VacuumBufferAbsorption.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Absorption with a canonical vacuum spare

A second unused source isometry is orthogonal to every word in the finite Fock sum. It therefore completes that sum to a connected ambient unitary without requiring the target corner to commute with the source row. The commutation requirements on the tested target entries remain explicit.

lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.exists_vacuum_absorption_on line 24

Source documentation

The second source spare replaces source-corner commutation in the connected Fock completion. Only the selected target entries must commute with the fixed binary coefficients.

lemma BufferAbsorptionCorner.exists_vacuum_absorption_on [Nontrivial E]
    (D : BufferAbsorptionCorner E) (s t : I → E) (r z : E) (P : I → Prop)
    (hrr : star r * r = 1) (hr : ∀ i, star r * s i = 0)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hzz : star z * z = 1) (hqz : D.q * z = 0)
    (hzr : star z * r = 0) (hzs : ∀ i, star z * s i = 0)
    (htq : ∀ i, t i * D.q = t i) (ht : ∑ i, t i * star (t i) = D.q)
    (htt : ∀ i j, star (t i) * t j = if i = j then D.q else 0)
    (hat : ∀ i, P i → Commute (star D.a) (t i))
    (hbt : ∀ i, P i → Commute (star D.b) (t i))
    (ε : ℝ) (hε : 0 < ε) :
    ∃ W : unitary E, Joined D.anchor W ∧
…

Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner

lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.exists_canonical_vacuum_absorption line 89

Source documentation

Canonical source rows supply both required spare isometries. The only geometric condition on the target corner is its annihilation of the second unused generator, as provided by the canonical vacuum split.

lemma BufferAbsorptionCorner.exists_canonical_vacuum_absorption [Nontrivial E]
    (D : BufferAbsorptionCorner E) (s : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (n : ℕ) (t : Fin n → E)
    (hqz : D.q * s (n + 1) = 0)
    (htq : ∀ i, t i * D.q = t i) (ht : ∑ i, t i * star (t i) = D.q)
    (htt : ∀ i j, star (t i) * t j = if i = j then D.q else 0)
    (hat : ∀ i, Commute (star D.a) (t i))
    (hbt : ∀ i, Commute (star D.b) (t i))
    (ε : ℝ) (hε : 0 < ε) :
    ∃ W : unitary E, Joined D.anchor W ∧
      ∀ i : Fin n,
…

Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner