PairChartSampling.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact normalized-pair identities for chart sampling

The action in this development is a left action obtained by inverting the manuscript's right-translation parameter. The identities below keep that inversion explicit.

def OAI.PolycyclicRecognition.chartOccupationPoint line 23
Source documentation
Normalization at the actual chart point, including the deterministic suffix between the two sampled factors.
```
def chartOccupationPoint (p : NormalizedPair G Λ) (x a k d : G) :
    NormalizedPair G Λ := normalizedTranslate (x * a * k * d) p
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.normalizedTranslate
theorem OAI.PolycyclicRecognition.chartOccupationPoint_right_factor line 28
Source documentation
A right move in the second factor changes only that factor.
```
theorem chartOccupationPoint_right_factor (p : NormalizedPair G Λ)
    (x a k d v : G) :
    v⁻¹ • chartOccupationPoint p x a k d =
      chartOccupationPoint p x a k (d * v) := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.chartOccupationPoint
theorem OAI.PolycyclicRecognition.chartOccupationPoint_normal_factor line 40
Source documentation
A right move in the normal factor changes the first sampled factor by the precise conjugate estimated by interior slack. No factorization uniqueness is needed.
```
theorem chartOccupationPoint_normal_factor (p : NormalizedPair G Λ)
    (x a k d u : G) :
    u⁻¹ • chartOccupationPoint p x a k d =
      chartOccupationPoint p x (a * (k * (d * u * d⁻¹) * k⁻¹)) k d := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.chartOccupationPoint
theorem OAI.PolycyclicRecognition.continuous_chartOccupationPoint line 49
Source documentation
Sampling is continuous in all four group coordinates.
```
theorem continuous_chartOccupationPoint (p : NormalizedPair G Λ) :
    Continuous (fun z : (G × G) × (G × G) =>
      chartOccupationPoint p z.1.1 z.1.2 z.2.1 z.2.2) := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.chartOccupationPoint