ConeProbeEndpoints.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The three actual endpoints used in the cone offset comparison

def OAI.PolycyclicRecognition.coneProbeFirst line 16
Source documentation
The endpoint carrying both the ideal probe and its quotient section.
```
def coneProbeFirst (S : MulAut N) (n i s : N) : N := n * S (i * s)
```
def OAI.PolycyclicRecognition.coneProbeSecond line 19
Source documentation
The neighboring endpoint carrying the same ideal probe.
```
def coneProbeSecond (S : MulAut N) (n i k : N) : N := n * S i * S k
```
theorem OAI.PolycyclicRecognition.coneProbe_bridge line 22
Source documentation
The bridge is independent of the ideal probe.
```
theorem coneProbe_bridge (S : MulAut N) (n i s k : N) :
    (coneProbeFirst S n i s)⁻¹ * coneProbeSecond S n i k = S (s⁻¹ * k) := by
…
```
Mentions: OAI.PolycyclicRecognition.coneProbeFirst, OAI.PolycyclicRecognition.coneProbeSecond
theorem OAI.PolycyclicRecognition.coneProbe_anchor_increment line 28
Source documentation
The path from the neighboring sheet to a tile anchor is the reverse conjugate of that anchor.
```
theorem coneProbe_anchor_increment (S : MulAut N) (n a k : N) :
    (n * S k)⁻¹ * coneProbeSecond S n a k = S (k⁻¹ * a * k) := by
…
```
Mentions: OAI.PolycyclicRecognition.coneProbeSecond
theorem OAI.PolycyclicRecognition.coneProbe_tile_increment line 34
Source documentation
Within one tile the second-sheet increment is exactly its conjugated ideal coordinate.
```
theorem coneProbe_tile_increment (S : MulAut N) (n a i k : N) :
    (coneProbeSecond S n a k)⁻¹ * coneProbeSecond S n i k =
      S (k⁻¹ * a⁻¹ * i * k) := by
…
```
Mentions: OAI.PolycyclicRecognition.coneProbeSecond
theorem OAI.PolycyclicRecognition.coneProbe_tile_increment_mem line 41
Source documentation
The covering inclusion gives the required small ideal increment without a condition on the quotient-section coordinate.
```
theorem coneProbe_tile_increment_mem (S : MulAut N) (n a i k : N) (B : Set N)
    (hi : i ∈ (fun z => a * k * z * k⁻¹) '' B) :
    (coneProbeSecond S n a k)⁻¹ * coneProbeSecond S n i k ∈ S '' B := by
…
```
Mentions: OAI.PolycyclicRecognition.coneProbeSecond