RelativeCocycle.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Actual binary row cocycles in a proper projection corner

The corner unitary is extended by the identity on the complementary projection. The complement is retained explicitly; this is not yet an ambient approximate intertwining statement for the canonical O∞ rows.

def OAI.WeakPureInfiniteness.projectionCornerElement line 20
Source documentation
A supported element, regarded as an element of the unital corner.
```
def projectionCornerElement (q : E) (hq : star q = q) (hqq : q * q = q)
    (x : E) (hx : q * x = x ∧ x * q = x) : ProjectionCorner q hq hqq := ⟨x, hx⟩
```
Mentions: OAI.WeakPureInfiniteness.ProjectionCorner
lemma OAI.WeakPureInfiniteness.projectionCornerElement_gram line 23
lemma OAI.WeakPureInfiniteness.projectionCornerElement_range_sum line 36
lemma OAI.WeakPureInfiniteness.projectionCornerInclusion_rowCocycle line 49
lemma OAI.WeakPureInfiniteness.projectionCornerInclusion_rowShift line 57
def OAI.WeakPureInfiniteness.relativeRowProduct line 66
Source documentation
The actual product cocycle, with the corner unit as its zeroth term.
```
def relativeRowProduct {I : Type*} [Fintype I] (q : E) (s t : I → E) : ℕ → E
  | 0 => q
  | n + 1 => finiteRowCocycle s t * finiteRowShift s (relativeRowProduct q s t n)
```
Mentions: OAI.WeakPureInfiniteness.finiteRowCocycle, OAI.WeakPureInfiniteness.finiteRowShift
lemma OAI.WeakPureInfiniteness.projectionCorner_rowProduct line 70
lemma OAI.WeakPureInfiniteness.projectionCornerUnitary_complement line 90

lemma OAI.WeakPureInfiniteness.exists_relative_binaryRowCocycle_path line 107

Source documentation

The uniform 192π contraction survives proper-corner transport. The constructed ambient unitary is exactly the product cocycle plus 1-q and fixes the complementary corner on both sides.

lemma exists_relative_binaryRowCocycle_path
    (q : E) (hq : star q = q) (hqq : q * q = q) (hqne : q ≠ 0)
    (s t : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then q else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then q else 0)
    (hsum : (∑ i, s i * star (s i)) = q)
    (htsum : (∑ i, t i * star (t i)) = q)
    (hc : ∀ i j, Commute (s i) (t j)) (n : ℕ) :
    ∃ u : unitary E, (u : E) = relativeRowProduct q s t n + (1 - q) ∧
      (u : E) * (1 - q) = 1 - q ∧ (1 - q) * (u : E) = 1 - q ∧
      ∃ p : Path u 1, ∀ a b, ‖(p a : E) - p b‖ ≤ (192 * Real.pi) * |(a : ℝ) - b| := by
…

Mentions: OAI.WeakPureInfiniteness.relativeRowProduct