OAI/Analysis/OInfinity/CanonicalBufferAbsorption.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Absorbing a commuting canonical row into the actual vacuum split

The corner and its connected anchor come from the source row itself. The finite target completion is used only at the auxiliary index. The original source representation remains explicitly on the complementary corner.

  1. lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.exists_proper_vacuum_absorption line 21

    Source documentation

    A vacuum corner absorbs a proper target prefix. No commutation of the corner with the source row is required.

    lemma BufferAbsorptionCorner.exists_proper_vacuum_absorption
    (D : BufferAbsorptionCorner E) (s t : ℕ → 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)
    (n : ℕ) (hqz : D.q * s (n + 2) = 0)
    (hqt : ∀ i, Commute D.q (t i))
    (hat : ∀ i, Commute (star D.a) (t i))
    (hbt : ∀ i, Commute (star D.b) (t i))
    (ε : ℝ) (hε : 0 < ε) :
    ∃ U : unitary E, Joined D.anchor U ∧
      ∀ i : Fin n,
        ‖(U : E) * s i * star (U : E) -
…

    Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner

  2. lemma OAI.WeakPureInfiniteness.exists_connected_canonical_buffer_absorption line 119

    Source documentation

    All geometric, coefficient-commutation and connected-anchor hypotheses are supplied by the two commuting canonical rows. The independently chosen tolerance κ controls the source's actual finite vacuum split.

    lemma exists_connected_canonical_buffer_absorption
    (s t : ℕ → 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)
    (hst : bergRowsCommute s t) (n : ℕ)
    (κ ε : ℝ) (hκ : 0 < κ) (hε : 0 < ε) :
    ∃ D : BufferAbsorptionCorner E, ∃ U : unitary E,
      Joined (1 : unitary E) U ∧ D.q ≠ 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‖ < κ) ∧
      (∀ i, Commute D.q (t i) ∧ Commute D.w (t i) ∧
…

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