CartanNeighborSamplingRow.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Original neighboring samples before their affine limit is identified

structure OAI.PolycyclicRecognition.CartanWordModel.NeighborSamplingRow line 38
Source documentation
Actual samples, root step and weak law, with no affine-limit premise.
```
structure NeighborSamplingRow where
…
```

def OAI.PolycyclicRecognition.CartanWordModel.NeighborSamplingRow.withAffinity line 86

Source documentation

Insert a proved common affine description into the exact original row. This changes neither its weak law nor either sampled profile.

def NeighborSamplingRow.withAffinity
    (A : templateSymmetryGroup (M.supportIn T hunimod eW)) (b₁ b₂ : W)
    (haffine : ∀ z, eW (heightProjection T.character
      ((WordBasisSelections.basis X (boundedBracketWords d) βD).equivFun.symm z :
        GroupLieAlgebra (𝓘(ℝ, EG)) G)) ∈ (fun w => (1 - c * δ) • w) '' interior cell →
      D.point.1.val z = A.val (eW (heightProjection T.character
        ((WordBasisSelections.basis X (boundedBracketWords d) βD).equivFun.symm z :
          GroupLieAlgebra (𝓘(ℝ, EG)) G))) + b₁ ∧
      D.point.2.val z = A.val (eW (heightProjection T.character
        ((WordBasisSelections.basis X (boundedBracketWords d) βD).equivFun.symm z :
          GroupLieAlgebra (𝓘(ℝ, EG)) G))) + b₂) :
    AffineNeighborRow T M F hunimod eW π bN cell β X βD
…

Mentions: OAI.PolycyclicRecognition.templateSymmetryGroup, OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.CartanWordModel.AffineNeighborRow