BlockGrid.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

Exact half-integer alignment, including the reflection endpoint conventions. Uniform deficit bounds converge to zero relative to s when |a/s-ν| does; no rounding of the prescribed real grid s is needed.

def OAI.TorsionFreeZeroDivisors.BlockGrid.cell line 10
Source documentation
Partition the unit interval into N half-open equal cells.
```
def cell (N : ℕ) (hN : 0 < N) (x : ℝ) : Fin N :=
…
```
theorem OAI.TorsionFreeZeroDivisors.BlockGrid.same_cell line 15

theorem OAI.TorsionFreeZeroDivisors.BlockGrid.simultaneous line 36

Source documentation

Simultaneous approximation in all d coordinates, with the exact denominator bound N^d, by the pigeonhole principle.

theorem simultaneous {d N : ℕ} (hN : 0 < N) (a : Fin d → ℝ) :
    ∃ u : ℕ, 1 ≤ u ∧ u ≤ N ^ d ∧
      ∃ z : Fin d → ℤ, ∀ i, |(u : ℝ) * a i - (z i : ℝ)| < 1 / (N : ℝ) := by
…

theorem OAI.TorsionFreeZeroDivisors.BlockGrid.scale_approximation line 63

Source documentation

Scaling the simultaneous approximation gives the common block scale s=L/(uR), with error at most R/N for every prescribed offset.

theorem scale_approximation {d N : ℕ} (hN : 0 < N)
    (L R : ℝ) (hL : 0 < L) (hR : 0 < R) (offset : Fin d → ℝ) :
    ∃ u : ℕ, 1 ≤ u ∧ u ≤ N^d ∧
      ∃ z : Fin d → ℤ,
        let s := L / ((u : ℝ)*R)
…

def OAI.TorsionFreeZeroDivisors.BlockAlignment.positions line 98
Source documentation
Integer edge indices whose half-integer centers belong to a real interval.
```
def positions (lo hi : ℝ) : Finset ℤ := Finset.Ico ⌈lo-1/2⌉ ⌈hi-1/2⌉
```
theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.mem_positions line 100
theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.card_lower line 106
Source documentation
Works even for a reversed/empty real interval.
```
theorem card_lower (lo hi : ℝ) : hi-lo-1 ≤ ((positions lo hi).card : ℝ) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.BlockAlignment.positions
theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.card_upper line 116
def OAI.TorsionFreeZeroDivisors.BlockAlignment.block line 127
def OAI.TorsionFreeZeroDivisors.BlockAlignment.affine line 129
def OAI.TorsionFreeZeroDivisors.BlockAlignment.partnerIndex line 131
def OAI.TorsionFreeZeroDivisors.BlockAlignment.overlap line 133
theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.core_subset line 138
Source documentation
A central interval survives both translation and reflection. Using one extra unit of margin removes the open/closed endpoint distinction.
```
theorem core_subset (s : ℝ) (reverse : Bool) (a k ν : ℤ) :
    positions ((k : ℝ)*s+(|a-(ν : ℝ)*s|+1))
      (((k : ℝ)+1)*s-(|a-(ν : ℝ)*s|+1)) ⊆ overlap s reverse a k ν := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.BlockAlignment.positions, OAI.TorsionFreeZeroDivisors.BlockAlignment.overlap
theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.overlap_deficit line 154
Source documentation
An explicit o(s) deficit for the exact grid and signed isometry.
```
theorem overlap_deficit (s : ℝ) (hs : 0 ≤ s) (reverse : Bool) (a k ν : ℤ) :
    (((block s k).card - (overlap s reverse a k ν).card : ℕ) : ℝ) ≤
      2*|a-(ν : ℝ)*s|+4 := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.BlockAlignment.block, OAI.TorsionFreeZeroDivisors.BlockAlignment.overlap

theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.dominant_unique line 170

Source documentation

An overlap larger than half of its block dominates every disjoint one.

theorem dominant_unique {B D E : Finset ℤ} (hD : D ⊆ B) (hE : E ⊆ B)
    (hdis : Disjoint D E) (hd : B.card < 2*D.card) (he : B.card < 2*E.card) : False := by
…

def OAI.TorsionFreeZeroDivisors.BlockAlignment.inverseOffset line 181
theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.affine_inverse line 183
theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.affine_injective line 187
theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.partner_inverse line 190
def OAI.TorsionFreeZeroDivisors.BlockAlignment.overlapEquiv line 195
Source documentation
The overlap on the partner block is exactly the image of the first overlap.
```
def overlapEquiv (s : ℝ) (reverse : Bool) (a k ν : ℤ) :
    overlap s reverse a k ν ≃
      overlap s reverse (inverseOffset reverse a) (partnerIndex reverse ν k) (inverseOffset reverse ν) where
…
```
Mentions: OAI.TorsionFreeZeroDivisors.BlockAlignment.overlap, OAI.TorsionFreeZeroDivisors.BlockAlignment.inverseOffset, OAI.TorsionFreeZeroDivisors.BlockAlignment.partnerIndex
theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.block_disjoint line 216
def OAI.TorsionFreeZeroDivisors.BlockAlignment.blockCount line 228
def OAI.TorsionFreeZeroDivisors.BlockAlignment.tail line 230
theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.count_bound line 232
theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.tail_bound line 240
theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.full_or_tail line 248
Source documentation
Literal partition into full blocks and the end fragment.
```
theorem full_or_tail (s : ℝ) (hs : 0 < s) (ell : ℕ) {q : ℤ}
    (hq : q ∈ positions 0 ell) :
    (∃ k : Fin (blockCount s ell), q ∈ block s k.val) ∨ q ∈ tail s ell := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.BlockAlignment.positions, OAI.TorsionFreeZeroDivisors.BlockAlignment.blockCount, OAI.TorsionFreeZeroDivisors.BlockAlignment.block, OAI.TorsionFreeZeroDivisors.BlockAlignment.tail
theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.full_subset line 267
Source documentation
A full block is entirely within its marked chain.
```
theorem full_subset (s : ℝ) (hs : 0 < s) (ell : ℕ) (k : Fin (blockCount s ell)) :
    block s k.val ⊆ positions 0 ell := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.BlockAlignment.blockCount, OAI.TorsionFreeZeroDivisors.BlockAlignment.block, OAI.TorsionFreeZeroDivisors.BlockAlignment.positions

theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.partner_full line 282

Source documentation

A grid block situated inside a comparison with one-block margins has a full indicated target block. This includes negative offsets and reflections.

theorem partner_full (s : ℝ) (hs : 0 < s) (reverse : Bool) (a k ν : ℤ)
    (lo hi ell : ℝ) (herr : |(a : ℝ)-(ν : ℝ)*s| ≤ s)
    (hlo : lo ≤ (k : ℝ)*s-s) (hhi : ((k : ℝ)+1)*s+s ≤ hi)
    (htarget : if reverse then 0 ≤ (a : ℝ)-hi ∧ (a : ℝ)-lo ≤ ell
      else 0 ≤ lo+(a : ℝ) ∧ hi+(a : ℝ) ≤ ell) :
    0 ≤ partnerIndex reverse ν k ∧ ((partnerIndex reverse ν k : ℤ)+1 : ℝ)*s ≤ ell := by
…

Mentions: OAI.TorsionFreeZeroDivisors.BlockAlignment.partnerIndex

theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.inverse_error line 303
def OAI.TorsionFreeZeroDivisors.BlockAlignment.nearCut line 313
Source documentation
Uniformly bounded exceptional grid indices near one real cut.
```
def nearCut (s t : ℝ) : Finset ℤ := Finset.Icc ⌈t/s-5⌉ ⌊t/s+5⌋
```
theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.mem_nearCut line 315
theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.nearCut_card line 320
theorem OAI.TorsionFreeZeroDivisors.BlockAlignment.margin_of_not_near line 331
Source documentation
A block containing a compared position and avoiding both endpoint neighborhoods is deep inside that exact comparison interval.
```
theorem margin_of_not_near (s : ℝ) (hs : 0 < s) (lo hi : ℝ) (k q : ℤ)
    (hq : q ∈ block s k) (hdom : q ∈ positions lo hi)
    (hnlo : k ∉ nearCut s lo) (hnhi : k ∉ nearCut s hi) :
    lo ≤ (k : ℝ)*s-s ∧ ((k : ℝ)+1)*s+s ≤ hi := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.BlockAlignment.block, OAI.TorsionFreeZeroDivisors.BlockAlignment.positions, OAI.TorsionFreeZeroDivisors.BlockAlignment.nearCut