MidpointCut.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Force the trace midpoint boundary by charging one extra imperfect position.

theorem OAI.TwoPointCorrelations.imperfectColumnCount_eq_card_compl line 11
theorem OAI.TwoPointCorrelations.imperfectColumnCount_erase_le line 26
theorem OAI.TwoPointCorrelations.perfect_block_avoids_cut line 43
Source documentation
A block containing only retained perfect positions cannot cross the erased midpoint. The erased step is still encoded by its ordinary imperfect-position reference.
```
theorem perfect_block_avoids_cut {n : ℕ} (perfect : Finset (Fin n)) (cut : Fin n)
    (start len : ℕ) (_hend : start + len ≤ n)
    (hperfect : ∀ t ∈ intervalPositions (start, len),
      columnNatPerfect (perfect.erase cut) t = true) :
    start + len ≤ cut.val ∨ cut.val < start := by
…
```
Mentions: OAI.TwoPointCorrelations.intervalPositions, OAI.TwoPointCorrelations.columnNatPerfect
theorem OAI.TwoPointCorrelations.isChain_slice_of_two_halves line 57

theorem OAI.TwoPointCorrelations.trace_perfect_block_chain line 70

Source documentation

The two actual nonbacktracking halves suffice for every retained perfect block; no relation between the two midpoint tuples is needed.

theorem trace_perfect_block_chain {n : ℕ} (perfect : Finset (Fin n)) (cut : Fin n)
    (w : List SignedStep)
    (hleft : (w.take cut.val).IsChain (fun a b => a.tuple ≠ b.tuple))
    (hright : (w.drop cut.val).IsChain (fun a b => a.tuple ≠ b.tuple))
    (start len : ℕ) (hend : start + len ≤ n)
    (hperfect : ∀ t ∈ intervalPositions (start, len),
      columnNatPerfect (perfect.erase cut) t = true) :
    (wordSlice w start (start + len)).IsChain (fun a b => a.tuple ≠ b.tuple) := by
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.intervalPositions, OAI.TwoPointCorrelations.columnNatPerfect, OAI.TwoPointCorrelations.wordSlice

theorem OAI.TwoPointCorrelations.eventually_imperfect_with_cut_bound line 85

Source documentation

The one additional midpoint reference fits inside the same imperfect budget once the singleton and unlit exceptional classes have been removed.

theorem eventually_imperfect_with_cut_bound :
    ∀ᶠ L : ℝ in Filter.atTop, ∀ singletons unlit imperfect : ℕ,
      imperfect ≤ singletons + unlit + 1 →
      (singletons : ℝ) ≤ L ^ (1 / 4 : ℝ) →
      (unlit : ℝ) ≤ L ^ (1 / 50 : ℝ) →
      (imperfect : ℝ) ≤ 2 * L ^ (1 / 4 : ℝ) := by
…