ConeProbeIntrinsicTiles.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic ideal increments of the three actual probe sheets

theorem OAI.PolycyclicRecognition.intrinsic_probe_inverse_flow line 16

Source documentation

The intrinsic inverse flow is precisely conjugation back by the normalized neighbor step.

theorem intrinsic_probe_inverse_flow (ι : I →* N) (φ : MulAut I) (k : N)
    (hφ : ∀ z, ι (φ z) = k * ι z * k⁻¹) (i : I) :
    k⁻¹ * ι i * k = ι (φ.symm i) := by
…

theorem OAI.PolycyclicRecognition.intrinsic_probe_tile_mem line 26
Source documentation
The tile covering gives an actual small ideal coordinate, without choosing a second preimage of a point under the ambient inclusion.
```
theorem intrinsic_probe_tile_mem (φ : MulAut I) (a i : I) (B : Set I)
    (hi : i ∈ a • (φ '' B)) : φ.symm (a⁻¹ * i) ∈ B := by
…
```
theorem OAI.PolycyclicRecognition.coneProbe_intrinsic_anchor_increment line 35
Source documentation
The anchor chain starts at the second original sheet and uses the reverse-flow anchor controlled by the larger template.
```
theorem coneProbe_intrinsic_anchor_increment
    (ι : I →* N) (φ : MulAut I) (k : N)
    (hφ : ∀ z, ι (φ z) = k * ι z * k⁻¹)
    (S : MulAut N) (n : N) (a : I) :
    (n * S k)⁻¹ * coneProbeSecond S n (ι a) k = S (ι (φ.symm a)) := by
…
```
Mentions: OAI.PolycyclicRecognition.coneProbeSecond

theorem OAI.PolycyclicRecognition.coneProbe_intrinsic_tile_increment line 44

Source documentation

The within-tile chain has the intrinsic ideal coordinate supplied by that same tile; it keeps the actual endpoint being counted.

theorem coneProbe_intrinsic_tile_increment
    (ι : I →* N) (φ : MulAut I) (k : N)
    (hφ : ∀ z, ι (φ z) = k * ι z * k⁻¹)
    (S : MulAut N) (n : N) (a i : I) :
    (coneProbeSecond S n (ι a) k)⁻¹ * coneProbeSecond S n (ι i) k =
      S (ι (φ.symm (a⁻¹ * i))) := by
…

Mentions: OAI.PolycyclicRecognition.coneProbeSecond