BinaryLeafRows.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The finite prefix rows used in the canonical vacuum split

The finite coisometric rows in the explicit split are prefix words in a relative binary pair. Binary conjugacy therefore controls them with a linear word-length loss. The ambient complementary corner remains fixed.

lemma OAI.WeakPureInfiniteness.zeroCornerRow_perturbation line 20
lemma OAI.WeakPureInfiniteness.zeroCornerRow_conjugate line 50

lemma OAI.WeakPureInfiniteness.exists_connected_binary_leaf_conjugacy line 70

Source documentation

The actual binary theorem controls every finite prefix row, not just the two generating isometries.

lemma exists_connected_binary_leaf_conjugacy [Nontrivial E]
    (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)
    (hcomm : bergRowsCommute s t) (n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧ ∀ i,
      ‖(u : E) * zeroCornerRow 1 (s 0) (s 1) n i * star (u : E) -
        zeroCornerRow 1 (t 0) (t 1) n i‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.WeakPureInfiniteness.zeroCornerRow

lemma OAI.WeakPureInfiniteness.projectionCornerUnitary_conjugate line 104
lemma OAI.WeakPureInfiniteness.projectionCorner_zeroCornerRow line 117

lemma OAI.WeakPureInfiniteness.exists_relative_binary_leaf_conjugacy line 133

Source documentation

Relative binary rows give finite prefix-row conjugacies inside their actual shared corner. The complementary identity is retained exactly.

lemma exists_relative_binary_leaf_conjugacy
    (q : E) (hq : star q = q) (hqq : q * q = q) (hq0 : 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)
    (hcomm : bergRowsCommute s t) (n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧
      (u : E) * (1 - q) = 1 - q ∧ (1 - q) * (u : E) = 1 - q ∧
      ∀ i, ‖(u : E) * zeroCornerRow q (s 0) (s 1) n i * star (u : E) -
        zeroCornerRow q (t 0) (t 1) n i‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.WeakPureInfiniteness.zeroCornerRow