FiniteCoordinates.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Cyclic leaf coordinates

The obstruction averages over the coordinate cyclic groups of the concrete finite parameter space. Coordinate homomorphisms have exact generators and a natural-multiple representation.

def OAI.TreeEdit.BinaryLower.FiniteVectors.leafCoordinate line 20
Source documentation
Insertion into one factor of the manuscript's product of cyclic groups.
```
def leafCoordinate (p : Fin k → Fin m → ℕ) (a : Leaf m k) :
    ZMod (leafPeriod p a) →+ State p where
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.leafPeriod, OAI.TreeEdit.BinaryLower.FiniteVectors.State
theorem OAI.TreeEdit.BinaryLower.FiniteVectors.leafCoordinate_apply_self line 26
theorem OAI.TreeEdit.BinaryLower.FiniteVectors.leafCoordinate_apply_ne line 31
theorem OAI.TreeEdit.BinaryLower.FiniteVectors.leafCoordinate_injective line 37
Source documentation
Each cyclic coordinate is genuinely embedded in the parameter group.
```
theorem leafCoordinate_injective (p : Fin k → Fin m → ℕ) (a : Leaf m k) :
    Function.Injective (leafCoordinate p a) := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.leafCoordinate
theorem OAI.TreeEdit.BinaryLower.FiniteVectors.leafCoordinate_one line 44
Source documentation
The coordinate generator is exactly the already constructed leaf vector.
```
@[simp] theorem leafCoordinate_one (p : Fin k → Fin m → ℕ) (a : Leaf m k) :
    leafCoordinate p a 1 = w p k a := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.leafCoordinate, OAI.TreeEdit.BinaryLower.FiniteVectors.w
theorem OAI.TreeEdit.BinaryLower.FiniteVectors.leafCoordinate_eq_val_nsmul line 56
Source documentation
Every residue shift is among the natural multiples of the leaf vector. This transports the manuscript's pointwise leaf-cost bound to the whole cyclic-coordinate average used in the spectral estimate.
```
theorem leafCoordinate_eq_val_nsmul (p : Fin k → Fin m → ℕ) (a : Leaf m k)
    [NeZero (leafPeriod p a)] (z : ZMod (leafPeriod p a)) :
    leafCoordinate p a z = z.val • w p k a := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.leafPeriod, OAI.TreeEdit.BinaryLower.FiniteVectors.leafCoordinate, OAI.TreeEdit.BinaryLower.FiniteVectors.w
theorem OAI.TreeEdit.BinaryLower.FiniteVectors.leafCoordinate_eq_val_zsmul line 68
Source documentation
Equivalent integer-multiple formulation, matching the source's allowed integer leaf translations.
```
theorem leafCoordinate_eq_val_zsmul (p : Fin k → Fin m → ℕ) (a : Leaf m k)
    [NeZero (leafPeriod p a)] (z : ZMod (leafPeriod p a)) :
    leafCoordinate p a z = (z.val : ℤ) • w p k a := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.leafPeriod, OAI.TreeEdit.BinaryLower.FiniteVectors.leafCoordinate, OAI.TreeEdit.BinaryLower.FiniteVectors.w