CanonicalBuffer.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

A connected absorption corner from the canonical vacuum split

The finite Fock construction provides the corner, its complementary isometry, its binary row and the path of the absorption anchor together. All coefficients inherit commutation with the original source commutant.

lemma OAI.WeakPureInfiniteness.zeroCornerRow_map line 20
lemma OAI.WeakPureInfiniteness.zeroCornerRow_star_commutes line 33
lemma OAI.WeakPureInfiniteness.finiteRowIsometry_commutes line 46
lemma OAI.WeakPureInfiniteness.finiteRowIsometry_star_commutes line 60

lemma OAI.WeakPureInfiniteness.exists_canonical_connected_absorption_corner_with_commuting_isometry line 79

Source documentation

The genuine canonical split has an explicitly connected absorption anchor and retains its unused generator. Its binary coefficients commute with every element of the source commutant.

lemma exists_canonical_connected_absorption_corner_with_commuting_isometry [Nontrivial E]
    (s : ℕ → E) (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ D : BufferAbsorptionCorner E,
      Joined (1 : unitary E) D.anchor ∧ D.q ≠ 0 ∧
      D.q * s (n + 2) = 0 ∧
      (∀ i : Fin (n + 1), ‖s i * D.q - D.q * s i‖ < ε) ∧
      (∀ i : Fin (n + 1),
        ‖D.q * s i * D.q - zeroCornerRow D.q D.a D.b n i‖ < ε) ∧
      (∃ z : E, star z * z = 1 ∧ D.q * z = z ∧
        ∀ y : E, (∀ i, Commute (s i) y ∧ Commute (star (s i)) y) → Commute z y) ∧
      (∀ y : E, (∀ i, Commute (s i) y ∧ Commute (star (s i)) y) →
…

Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner, OAI.WeakPureInfiniteness.zeroCornerRow

lemma OAI.WeakPureInfiniteness.exists_canonical_connected_absorption_corner_with_isometry line 276

Source documentation

The actual internal unit-isometry, forgetting its commutant data.

lemma exists_canonical_connected_absorption_corner_with_isometry [Nontrivial E]
    (s : ℕ → E) (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ D : BufferAbsorptionCorner E,
      Joined (1 : unitary E) D.anchor ∧ D.q ≠ 0 ∧
      D.q * s (n + 2) = 0 ∧
      (∀ i : Fin (n + 1), ‖s i * D.q - D.q * s i‖ < ε) ∧
      (∀ i : Fin (n + 1),
        ‖D.q * s i * D.q - zeroCornerRow D.q D.a D.b n i‖ < ε) ∧
      (∃ z : E, star z * z = 1 ∧ D.q * z = z) ∧
      (∀ y : E, (∀ i, Commute (s i) y ∧ Commute (star (s i)) y) →
        Commute D.q y ∧ Commute D.w y ∧ Commute D.a y ∧ Commute D.b y) := by
…

Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner, OAI.WeakPureInfiniteness.zeroCornerRow

lemma OAI.WeakPureInfiniteness.exists_canonical_connected_absorption_corner line 293

Source documentation

The canonical absorption corner with its source commutant data.

lemma exists_canonical_connected_absorption_corner [Nontrivial E]
    (s : ℕ → E) (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ D : BufferAbsorptionCorner E,
      Joined (1 : unitary E) D.anchor ∧ D.q ≠ 0 ∧
      D.q * s (n + 2) = 0 ∧
      (∀ i : Fin (n + 1), ‖s i * D.q - D.q * s i‖ < ε) ∧
      (∀ i : Fin (n + 1),
        ‖D.q * s i * D.q - zeroCornerRow D.q D.a D.b n i‖ < ε) ∧
      (∀ y : E, (∀ i, Commute (s i) y ∧ Commute (star (s i)) y) →
        Commute D.q y ∧ Commute D.w y ∧ Commute D.a y ∧ Commute D.b y) := by
…

Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner, OAI.WeakPureInfiniteness.zeroCornerRow