AffineIntervals.lean`

56 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TorsionFreeZeroDivisors.AffineIntervals.boundary line 14
Source documentation
Boundary action of a signed interval isometry. On half-integer centers it agrees with the manuscript's letter-index affine action.
```
def boundary (r : Bool) (a x : ℤ) : ℤ := if r then a-x else x+a
```
def OAI.TorsionFreeZeroDivisors.AffineIntervals.compOffset line 16
lemma OAI.TorsionFreeZeroDivisors.AffineIntervals.affine_comp line 18
lemma OAI.TorsionFreeZeroDivisors.AffineIntervals.boundary_comp line 22
lemma OAI.TorsionFreeZeroDivisors.AffineIntervals.integer_positions line 26
lemma OAI.TorsionFreeZeroDivisors.AffineIntervals.nat_positions line 45
def OAI.TorsionFreeZeroDivisors.AffineIntervals.preLo line 50
Source documentation
Exact integer endpoints of the inverse image; reflection does not incur any rounding loss on the source half-integer convention.
```
def preLo (r : Bool) (a lo hi : ℤ) : ℤ := if r then a-hi else lo-a
```
def OAI.TorsionFreeZeroDivisors.AffineIntervals.preHi line 51
lemma OAI.TorsionFreeZeroDivisors.AffineIntervals.mem_preimage line 53
lemma OAI.TorsionFreeZeroDivisors.AffineIntervals.preimage_bounds line 57
def OAI.TorsionFreeZeroDivisors.AffineIntervals.anchor line 64
Source documentation
Empty comparison sides may be placed at the preimage of target boundary zero; this has no occurrences and satisfies the global range condition.
```
def anchor (r : Bool) (a : ℤ) : ℤ := if r then a else -a
```
lemma OAI.TorsionFreeZeroDivisors.AffineIntervals.anchor_bounds line 66
structure OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking line 79
Source documentation
A literal partition into signed integer chunks, not a count of formal pieces.
```
structure Chunking (lp : P → ℕ) (lt : T → ℕ) where
…
```
lemma OAI.TorsionFreeZeroDivisors.ChunkComparisons.position_ext line 87
def OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.pairing line 97
lemma OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.partner_image line 103
def OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.rev line 107
def OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.off line 110
lemma OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.new_affine line 114
lemma OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.new_affine_image line 121
lemma OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.partner_coordinate line 128

lemma OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.partner_chunk_iff line 141

Source documentation

The image of an old partner is in a given chunk precisely when the conjugate affine index is in that chunk.

lemma partner_chunk_iff {x : Position lt} {e : E} {u : T}
    (he : C.side (K.equiv x)=some e) (hu : K.path u=C.source (C.flip e)) :
    ((K.pairing C).partner x).1=u ↔
      affine (K.rev C e x.1 u) (K.off C e x.1 u) x.2.val ∈ positions 0 (lt u) := by
…

def OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.rawLo line 163
def OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.rawHi line 166
def OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.valid line 170
def OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.lower line 174
def OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.upper line 177
lemma OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.interval_iff line 184
lemma OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.range_bounds line 231
def OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.side line 243
lemma OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.side_iff line 246
def OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.comparisons line 253
Source documentation
Split every side at the boundaries of both chunks. Empty pieces carry no positions; their chosen endpoint maintains the exact range convention.
```
def comparisons : Comparisons (E := E×T×T) lt where
…
```
lemma OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.fixed_iff line 306
def OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.unpairedEquiv line 315

theorem OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.unpaired_card line 321

Source documentation

Splitting and orientation normalization neither deletes nor duplicates an unpaired occurrence.

theorem unpaired_card [Fintype P] [Fintype T] :
    Fintype.card {x : Position lt // (K.comparisons C lo hi hlo hhi).pairing.partner x=x} =
      Fintype.card {x : Position lp // C.pairing.partner x=x} :=
…

lemma OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.xor_labels line 326

theorem OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.compatible line 338

Source documentation

Every literal compatible labeling survives splitting with exactly the xor of the path comparison and the two chain orientations.

theorem compatible {A : Type*} (bar : A → A) (hb : Function.Involutive bar)
    (old : Position lp → A) (word : Position lt → A)
    (hn : ∀ x,old (K.equiv x)=if K.reverse x.1 then bar (word x) else word x)
    (hc : ∀ x e,C.side x=some e → old x = if C.reverse e then
      bar (old (C.pairing.partner x)) else old (C.pairing.partner x)) :
    ∀ x a, (K.comparisons C lo hi hlo hhi).side x=some a →
      word x=if (K.comparisons C lo hi hlo hhi).reverse a then
        bar (word ((K.comparisons C lo hi hlo hhi).pairing.partner x))
      else word ((K.comparisons C lo hi hlo hhi).pairing.partner x) := by
…

Mentions: OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.side

def OAI.TorsionFreeZeroDivisors.FiniteChunking.before line 367
def OAI.TorsionFreeZeroDivisors.FiniteChunking.start line 368
lemma OAI.TorsionFreeZeroDivisors.FiniteChunking.not_before line 370
lemma OAI.TorsionFreeZeroDivisors.FiniteChunking.start_next line 372
lemma OAI.TorsionFreeZeroDivisors.FiniteChunking.start_end line 382
def OAI.TorsionFreeZeroDivisors.FiniteChunking.localIndex line 386
lemma OAI.TorsionFreeZeroDivisors.FiniteChunking.local_bounds line 388
lemma OAI.TorsionFreeZeroDivisors.FiniteChunking.affine_offset line 393
lemma OAI.TorsionFreeZeroDivisors.FiniteChunking.positions_card line 397
lemma OAI.TorsionFreeZeroDivisors.FiniteChunking.position_card line 400
abbrev OAI.TorsionFreeZeroDivisors.FiniteChunking.Traversal line 407
abbrev OAI.TorsionFreeZeroDivisors.FiniteChunking.traversalLength line 408
def OAI.TorsionFreeZeroDivisors.FiniteChunking.pathLength line 409
def OAI.TorsionFreeZeroDivisors.FiniteChunking.offset line 411
def OAI.TorsionFreeZeroDivisors.FiniteChunking.image line 413
lemma OAI.TorsionFreeZeroDivisors.FiniteChunking.image_val line 424
lemma OAI.TorsionFreeZeroDivisors.FiniteChunking.image_injective line 430
def OAI.TorsionFreeZeroDivisors.FiniteChunking.equiv line 459
Source documentation
The prescribed offsets define an actual equivalence. In particular, this partition covers every old letter even when a path is empty.
```
def equiv : Position (traversalLength chunks len) ≃ Position (pathLength chunks len) :=
…
```
Mentions: OAI.TorsionFreeZeroDivisors.FiniteChunking.traversalLength, OAI.TorsionFreeZeroDivisors.FiniteChunking.pathLength
def OAI.TorsionFreeZeroDivisors.FiniteChunking.chunking line 464