CocycleCancellation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Cancellation transport for the actual binary cocycle

The joint cyclic partitions supply all transport premises for the length-two versus length-one cancellation in binary fragmentation. The partition is chosen after the cocycle length and requested error. This remains a theorem about two commuting coisometric binary rows.

def OAI.WeakPureInfiniteness.cancellationTowerModel line 22
Source documentation
The three transported components, keeping both shifted indices.
```
def cancellationTowerModel {N : ℕ} (e : ZMod N → E) (a b u : E)
    (da db : ZMod N) (θ : ℝ) (k : ZMod N) : E :=
…
```
lemma OAI.WeakPureInfiniteness.cocycle_row_norm line 29

lemma OAI.WeakPureInfiniteness.cyclic_row_generator_transport line 40

Source documentation

A cyclic shift estimate for the row endomorphism gives the actual one-generator transport estimate.

lemma cyclic_row_generator_transport {N : ℕ} (s : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (e : ZMod N → E) (η : ℝ)
    (hshift : ∀ k, ‖finiteRowShift s (e k) - e (k + 1)‖ ≤ η)
    (i : Fin 2) (k : ZMod N) :
    ‖s i * e k - e (k + 1) * s i‖ ≤ η := by
…

Mentions: OAI.WeakPureInfiniteness.finiteRowShift

lemma OAI.WeakPureInfiniteness.cyclic_row_two_letter_transport line 53

lemma OAI.WeakPureInfiniteness.exists_cocycle_cancellation_partition line 79

Source documentation

All the length-two/length-one quarter cancellations have an actual joint cyclic partition, and their three-band transport error is arbitrarily small uniformly in angle and tower cell.

lemma exists_cocycle_cancellation_partition (s t : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (hsum : (∑ i, s i * star (s i)) = 1)
    (htsum : (∑ i, t i * star (t i)) = 1)
    (hc : bergRowsCommute s t) (m ℓ : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ e : ZMod (2 ^ m) → E,
      (∀ k, IsStarProjection (e k)) ∧ (∑ k, e k) = 1 ∧
      (∀ k l, k ≠ l → e k * e l = 0) ∧
      (∀ k, ‖finiteRowShift s (e k) - e (k + 1)‖ < ε) ∧
      (∀ k, ‖finiteRowShift t (e k) - e (k + 1)‖ < ε) ∧
      (∀ (i r l : Fin 2), i ≠ l → ∀ (θ : ℝ) (k : ZMod (2 ^ m)),
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.WeakPureInfiniteness.finiteRowShift