FiniteTreeGeometry.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Concrete tagged leaf states and subtree locality for the finite tree.

abbrev OAI.TreeEdit.BinaryLower.FiniteTree.Leaf line 12
Source documentation
The finite leaf set, represented by ordered paths of exactly k edges.
```
abbrev Leaf (m k : ℕ) := Word (Fin m) k
```
Mentions: OAI.TreeEdit.Word
abbrev OAI.TreeEdit.BinaryLower.FiniteTree.State line 15
Source documentation
The manuscript's product of cyclic leaf coordinates.
```
abbrev State {m k : ℕ} (Q : Leaf m k → ℕ) := ∀ l, ZMod (Q l)
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf
abbrev OAI.TreeEdit.BinaryLower.FiniteTree.Symbol line 18
Source documentation
A symbol retains both its leaf tag and its cyclic state.
```
abbrev Symbol {m k : ℕ} (Q : Leaf m k → ℕ) := Σ l, ZMod (Q l)
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf
def OAI.TreeEdit.BinaryLower.FiniteTree.leafDecoder line 22
Source documentation
Decode an actual leaf path. The fallback only totalizes this function on paths of the wrong length; the root construction never evaluates that branch.
```
def leafDecoder {m k : ℕ} (Q : Leaf m k → ℕ) (base : Leaf m k)
    (p : List (Fin m)) (x : State Q) : Symbol Q :=
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf, OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.Symbol
theorem OAI.TreeEdit.BinaryLower.FiniteTree.leafDecoder_of_length line 26
theorem OAI.TreeEdit.BinaryLower.FiniteTree.leafDecoder_eq_iff line 32
Source documentation
At a valid leaf, equality is exactly equality of that leaf's state.
```
theorem leafDecoder_eq_iff {m k : ℕ} (Q : Leaf m k → ℕ)
    (base : Leaf m k) (p : List (Fin m)) (hp : p.length = k) (x y : State Q) :
    leafDecoder Q base p x = leafDecoder Q base p y ↔
      x ⟨p, hp⟩ = y ⟨p, hp⟩ := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf, OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.leafDecoder
theorem OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord_state_congr line 40
Source documentation
The recursive word depends only on the coordinates below its prefix, even though ancestor shifts may offset all coordinates of the supplied state.
```
theorem nodeWord_state_congr {T m k : ℕ} (Q : Leaf m k → ℕ)
    (base : Leaf m k) (u : List (Fin m) → State Q)
    (h : ℕ) (p : List (Fin m)) (hlen : p.length + h = k)
    (x y : State Q) (hagree : ∀ l : Leaf m k, p <+: l.val → x l = y l) :
    nodeWord T (leafDecoder Q base) u h p x =
      nodeWord T (leafDecoder Q base) u h p y := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf, OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord, OAI.TreeEdit.BinaryLower.FiniteTree.leafDecoder
def OAI.TreeEdit.BinaryLower.FiniteTree.leafEquiv line 66
Source documentation
The list-path and function-path presentations of the same leaf set.
```
def leafEquiv (m k : ℕ) : Leaf m k ≃ (Fin k → Fin m) :=
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf
def OAI.TreeEdit.BinaryLower.FiniteTree.pullState line 72
Source documentation
Pull back a function-indexed cyclic state to the list-path presentation. This is just relabeling coordinates, used to connect the closed-form vectors to the list recursion.
```
def pullState {m k : ℕ} (Q : (Fin k → Fin m) → ℕ)
    (x : ∀ l, ZMod (Q l)) : State (fun l => Q (leafEquiv m k l)) :=
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.leafEquiv
theorem OAI.TreeEdit.BinaryLower.FiniteTree.pullState_add line 76
theorem OAI.TreeEdit.BinaryLower.FiniteTree.pullState_nsmul line 80
theorem OAI.TreeEdit.BinaryLower.FiniteTree.pullState_zsmul line 84

theorem OAI.TreeEdit.BinaryLower.FiniteTree.leafDecoder_ne_of_not_dvd line 89

Source documentation

A nonzero residue shift changes the tagged symbol at a leaf.

theorem leafDecoder_ne_of_not_dvd {m k : ℕ} (Q : Leaf m k → ℕ)
    (base : Leaf m k) (p : List (Fin m)) (hp : p.length = k)
    (x z : State Q) (hz : z ⟨p, hp⟩ = 1) (t : ℤ)
    (ht : ¬ (Q ⟨p, hp⟩ : ℤ) ∣ t) :
    leafDecoder Q base p (x + t • z) ≠ leafDecoder Q base p x := by
…

Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf, OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.leafDecoder

theorem OAI.TreeEdit.BinaryLower.FiniteTree.singleton_deficit_of_ne line 101
Source documentation
Two different singleton words have unit one-sided deficit.
```
theorem singleton_deficit_of_ne {Γ : Type*} (a b : Γ) (hab : a ≠ b) :
    deficit 1 [a] [b] = 1 := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.deficit
theorem OAI.TreeEdit.BinaryLower.FiniteTree.leaf_deficit_of_not_dvd line 121
Source documentation
The base case of finite separation, with the actual canonical deficit.
```
theorem leaf_deficit_of_not_dvd {m k : ℕ} (Q : Leaf m k → ℕ)
    (base : Leaf m k) (p : List (Fin m)) (hp : p.length = k)
    (x z : State Q) (hz : z ⟨p, hp⟩ = 1) (t : ℤ)
    (ht : ¬ (Q ⟨p, hp⟩ : ℤ) ∣ t) :
    deficit 1 [leafDecoder Q base p x] [leafDecoder Q base p (x + t • z)] = 1 := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf, OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.deficit, OAI.TreeEdit.BinaryLower.FiniteTree.leafDecoder
theorem OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord_shift_congr line 131
Source documentation
State shifts agreeing below one node produce exactly the same subtree word, giving support locality for the closed-form vectors.
```
theorem nodeWord_shift_congr {T m k : ℕ} (Q : Leaf m k → ℕ)
    (base : Leaf m k) (u : List (Fin m) → State Q)
    (h : ℕ) (p : List (Fin m)) (hlen : p.length + h = k)
    (x z w : State Q) (hagree : ∀ l : Leaf m k, p <+: l.val → z l = w l) :
    nodeWord T (leafDecoder Q base) u h p (x + z) =
      nodeWord T (leafDecoder Q base) u h p (x + w) := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf, OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord, OAI.TreeEdit.BinaryLower.FiniteTree.leafDecoder

theorem OAI.TreeEdit.BinaryLower.FiniteTree.child_relative_shift line 144

Source documentation

The relative input shift between source row a and target row b in a child is (b-a+tR) times its distinguished vector. The two support hypotheses are precisely the coordinate restrictions of the explicit subtree vectors.

theorem child_relative_shift {T m k : ℕ} (Q : Leaf m k → ℕ)
    (base : Leaf m k) (u : List (Fin m) → State Q)
    (h : ℕ) (p : List (Fin m)) (hlen : p.length + h = k)
    (x wp up wc : State Q) (R t : ℤ) (a b : ℕ)
    (hu : ∀ l : Leaf m k, p <+: l.val → up l = wc l)
    (hw : ∀ l : Leaf m k, p <+: l.val → wp l = R • wc l) :
    nodeWord T (leafDecoder Q base) u h p (x + t • wp + b • up) =
      nodeWord T (leafDecoder Q base) u h p
        (x + a • up + ((b : ℤ) - (a : ℤ) + t * R) • wc) := by
…

Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf, OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord, OAI.TreeEdit.BinaryLower.FiniteTree.leafDecoder