PathInjectivity.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.matrixEntryPaths_nodup_local line 13
Source documentation
The recursive path enumeration never repeats a path.
```
private theorem matrixEntryPaths_nodup_local [Fintype ι] [DecidableEq ι]
    (labels : List σ) (i j : ι) : (matrixEntryPaths labels i j).Nodup := by
…
```
Mentions: OAI.Problem335.matrixEntryPaths

def OAI.Problem335.edgeListShift line 37

Source documentation

Differentiated coordinates have sign -1, multiplied coordinates sign +1.

def edgeListShift (side : σ → Bool) : List (σ × ι × ι) → ((σ × ι × ι) →₀ ℤ)
  | [] => 0
  | e :: p => Finsupp.single e (if side e.1 then -1 else 1) + edgeListShift side p

theorem OAI.Problem335.edgeListShift_nil line 41
theorem OAI.Problem335.edgeListShift_cons line 44

theorem OAI.Problem335.edgeListShift_apply_eq_zero line 50

Source documentation

A layer absent from a path has no coordinate shift.

theorem edgeListShift_apply_eq_zero (side : σ → Bool) (p : List (σ × ι × ι))
    (e : σ × ι × ι) (he : e.1 ∉ p.map Prod.fst) : edgeListShift side p e = 0 := by
…

Mentions: OAI.Problem335.edgeListShift

theorem OAI.Problem335.edgeListShift_apply_of_not_mem line 64
Source documentation
A coordinate absent from the edge list receives no shift.
```
theorem edgeListShift_apply_of_not_mem (side : σ → Bool) (p : List (σ × ι × ι))
    (e : σ × ι × ι) (he : e ∉ p) : edgeListShift side p e = 0 := by
…
```
Mentions: OAI.Problem335.edgeListShift

theorem OAI.Problem335.edgeListShift_injective_of_labels line 74

Source documentation

With a fixed nonrepeating layer list, the signed shift determines the whole path.

theorem edgeListShift_injective_of_labels (side : σ → Bool)
    (labels : List σ) (hlabels : labels.Nodup)
    (p q : List (σ × ι × ι)) (hp : p.map Prod.fst = labels)
    (hq : q.map Prod.fst = labels) (hshift : edgeListShift side p = edgeListShift side q) :
    p = q := by
…

Mentions: OAI.Problem335.edgeListShift

theorem OAI.Problem335.edgeListShift_apply_of_mem line 107

Source documentation

A selected coordinate occurs with its single creation/annihilation sign.

theorem edgeListShift_apply_of_mem (side : σ → Bool) (p : List (σ × ι × ι))
    (hlabels : (p.map Prod.fst).Nodup) (e : σ × ι × ι) (he : e ∈ p) :
    edgeListShift side p e = if side e.1 then -1 else 1 := by
…

Mentions: OAI.Problem335.edgeListShift

theorem OAI.Problem335.edgeListShift_apply line 126

Source documentation

With one edge per layer, coordinate shifts are precisely signed membership.

theorem edgeListShift_apply [DecidableEq σ] [DecidableEq ι] (side : σ → Bool) (p : List (σ × ι × ι))
    (hlabels : (p.map Prod.fst).Nodup) (e : σ × ι × ι) :
    edgeListShift side p e = if e ∈ p then (if side e.1 then -1 else 1) else 0 := by
…

Mentions: OAI.Problem335.edgeListShift

theorem OAI.Problem335.matrixEntryPaths_shift_injective line 137

Source documentation

Finite path indices are distinguished by their signed exponent shifts.

theorem matrixEntryPaths_shift_injective [Fintype ι] [DecidableEq ι]
    (side : σ → Bool) (labels : List σ) (hlabels : labels.Nodup) (i j : ι) :
    Function.Injective (fun p : Fin (matrixEntryPaths labels i j).length =>
      edgeListShift side ((matrixEntryPaths labels i j).get p)) := by
…

Mentions: OAI.Problem335.matrixEntryPaths, OAI.Problem335.edgeListShift

theorem OAI.Problem335.matrixEntryPaths_translated_shift_injective line 148

Source documentation

From any fixed input exponent, two distinct paths reach distinct output exponents.

theorem matrixEntryPaths_translated_shift_injective [Fintype ι] [DecidableEq ι]
    (side : σ → Bool) (labels : List σ) (hlabels : labels.Nodup) (i j : ι)
    (input : (σ × ι × ι) →₀ ℤ) :
    Function.Injective (fun p : Fin (matrixEntryPaths labels i j).length =>
      input + edgeListShift side ((matrixEntryPaths labels i j).get p)) := by
…

Mentions: OAI.Problem335.matrixEntryPaths, OAI.Problem335.edgeListShift

theorem OAI.Problem335.edgeListShift_eq_sum line 158

Source documentation

The signed list shift is the sum of the individual signed coordinates.

theorem edgeListShift_eq_sum (side : σ → Bool) (p : List (σ × ι × ι)) :
    edgeListShift side p =
      (p.map (fun e => Finsupp.single e (if side e.1 then (-1 : ℤ) else 1))).sum := by
…

Mentions: OAI.Problem335.edgeListShift

theorem OAI.Problem335.edgeList_length line 166

Source documentation

A list containing all layer labels in order has the expected length.

theorem edgeList_length {n : ℕ} (p : List (Fin n × ι × ι))
    (hp : p.map Prod.fst = List.finRange n) : p.length = n := by
…

def OAI.Problem335.edgeProfile line 171

Source documentation

Convert an edge list ordered by layer into its finite coordinate profile.

def edgeProfile {n : ℕ} (p : List (Fin n × ι × ι))
    (hp : p.map Prod.fst = List.finRange n) (t : Fin n) : ι × ι :=
…

theorem OAI.Problem335.edgeProfile_label line 176

Source documentation

In an ordered edge list, the edge in position t is labelled by t.

theorem edgeProfile_label {n : ℕ} (p : List (Fin n × ι × ι))
    (hp : p.map Prod.fst = List.finRange n) (t : Fin n) :
    (p[t.val]'(by rw [edgeList_length p hp]; exact t.isLt)).1 = t := by
…

Mentions: OAI.Problem335.edgeList_length

theorem OAI.Problem335.edgeList_eq_ofFn_profile line 186

Source documentation

Rebuilding the ordered edge list from its profile changes nothing.

theorem edgeList_eq_ofFn_profile {n : ℕ} (p : List (Fin n × ι × ι))
    (hp : p.map Prod.fst = List.finRange n) :
    p = List.ofFn (fun t : Fin n => (t, edgeProfile p hp t)) := by
…

Mentions: OAI.Problem335.edgeProfile

theorem OAI.Problem335.edgeListShift_eq_sum_profile line 196

Source documentation

The list shift agrees with the layerwise finite sum used by profile operators.

theorem edgeListShift_eq_sum_profile {n : ℕ} (side : Fin n → Bool)
    (p : List (Fin n × ι × ι)) (hp : p.map Prod.fst = List.finRange n) :
    edgeListShift side p = ∑ t : Fin n,
      Finsupp.single (t, edgeProfile p hp t) (if side t then (-1 : ℤ) else 1) := by
…

Mentions: OAI.Problem335.edgeListShift, OAI.Problem335.edgeProfile

theorem OAI.Problem335.matrixEntryPaths_profile_injective line 205

Source documentation

Ordered edge-list indices have distinct layer profiles.

theorem matrixEntryPaths_profile_injective [Fintype ι] [DecidableEq ι]
    (n : ℕ) (i j : ι) :
    Function.Injective (fun p : Fin (matrixEntryPaths (List.finRange n) i j).length =>
      edgeProfile ((matrixEntryPaths (List.finRange n) i j).get p)
        (matrixEntryPaths_get_labels (List.finRange n) i j p)) := by
…

Mentions: OAI.Problem335.matrixEntryPaths, OAI.Problem335.edgeProfile, OAI.Problem335.matrixEntryPaths_get_labels

theorem OAI.Problem335.edgeListShift_nonnegative_iff line 218

Source documentation

The signed output is nonnegative exactly when every requested derivative is available.

theorem edgeListShift_nonnegative_iff [DecidableEq σ] [DecidableEq ι]
    (side : σ → Bool) (p : List (σ × ι × ι))
    (hlabels : (p.map Prod.fst).Nodup) (input : (σ × ι × ι) → ℕ) :
    (∀ e, 0 ≤ (input e : ℤ) + edgeListShift side p e) ↔
      ∀ e ∈ p, side e.1 = true → 1 ≤ input e := by
…

Mentions: OAI.Problem335.edgeListShift

theorem OAI.Problem335.edgeListShift_apply_profile line 242

Source documentation

Read a signed edge-list shift using its unique coordinate profile in one layer.

theorem edgeListShift_apply_profile [DecidableEq ι] {n : ℕ}
    (side : Fin n → Bool) (p : List (Fin n × ι × ι))
    (hp : p.map Prod.fst = List.finRange n) (t : Fin n) (a b : ι) :
    edgeListShift side p (t, a, b) =
      if edgeProfile p hp t = (a, b) then (if side t then -1 else 1) else 0 := by
…

Mentions: OAI.Problem335.edgeListShift, OAI.Problem335.edgeProfile

theorem OAI.Problem335.edgeListShift_sub_eq_iff line 257

Source documentation

Four ordered edge lists have compatible global shifts exactly when their coordinate differences agree separately in every layer.

theorem edgeListShift_sub_eq_iff {n : ℕ} (side : Fin n → Bool)
    (p q r s : List (Fin n × ι × ι))
    (hp : p.map Prod.fst = List.finRange n)
    (hq : q.map Prod.fst = List.finRange n)
    (hr : r.map Prod.fst = List.finRange n)
    (hs : s.map Prod.fst = List.finRange n) :
    edgeListShift side p - edgeListShift side q =
      edgeListShift side r - edgeListShift side s ↔
      ∀ t : Fin n,
        Finsupp.single (edgeProfile p hp t) (1 : ℤ) -
          Finsupp.single (edgeProfile q hq t) 1 =
        Finsupp.single (edgeProfile r hr t) 1 -
…

Mentions: OAI.Problem335.edgeListShift, OAI.Problem335.edgeProfile