CartanNeighborRowOffsetsEqual.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The finite polar tests determine both affine offsets

theorem OAI.PolycyclicRecognition.CartanWordModel.AffineNeighborRow.offsets_eq_of_cone_bounds line 50

Source documentation

Apply each fixed quotient trace to the original row and to its actual reversal. The ray and two-ray tests then force the offsets to agree.

theorem AffineNeighborRow.offsets_eq_of_cone_bounds
    (hExp : IsGroupExponential ExpG)
    (dynkinN : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
    (hcell : IsCompact cell) (hne : cell.Nonempty)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW cell) βcell.val)
    (hδ : 0 ≤ δ) (hs : ∀ n, 0 ≤ D.scale n)
    (hlabels : D.label₂ = D.label₁)
    (hnz : ∀ i, (M.supportIn T hunimod eW).weight i ≠ 0)
    (coeff : rootOffsetConeIndex (M.supportIn T hunimod eW) D.mode →
      Fin M.letterCount → ℕ)
    (hout : ∀ s j, ((M.supportIn T hunimod eW).weight j).toContinuousLinearMap ∉
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.rootOffsetConeIndex

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_neighbor_offset_threshold line 88

Source documentation

Finitely many cone and label thresholds give a single positive threshold for all original neighboring rows. Cofinal restriction supplies positive scales before reversal.

theorem exists_uniform_neighbor_offset_threshold
    [Nonempty (Fin M.letterCount)]
    (hExp : IsGroupExponential ExpG)
    (dynkinN : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
    (hcell : IsCompact cell) (hne : cell.Nonempty)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW cell) βcell.val)
    (hnz : ∀ i, (M.supportIn T hunimod eW).weight i ≠ 0)
    (hcone : ∀ (i : Fin M.letterCount)
      (A : templateSymmetryGroup (M.supportIn T hunimod eW))
      (s : rootOffsetConeIndex (M.supportIn T hunimod eW) i),
      ∃ coeff : Fin M.letterCount → ℕ,
…