BufferedTail.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact relocation of the whole buffered tail

An actual unit-isometry in the canonical vacuum corner exchanges its range with the full terminal range of w^(m+1). The swap commutes with the target family and has a uniform path. Its formula retains the residual source copy; relocation itself does not estimate that copy by zero.

lemma OAI.WeakPureInfiniteness.buffered_isometry_pow_gram line 20

lemma OAI.WeakPureInfiniteness.exists_controlled_isometry_swap line 33

Source documentation

Two orthogonal full isometries have a self-adjoint swap. Its commutant property is stated for both isometries and adjoints, not inferred from unstarred commutation alone.

lemma exists_controlled_isometry_swap [Nontrivial E] (r z : E)
    (hr : star r * r = 1) (hz : star z * z = 1) (hzr : star z * r = 0) :
    ∃ u : unitary E, (u : E) * r = z ∧ (u : E) * z = r ∧
      star (u : E) = (u : E) ∧
      (∀ x : E, Commute r x → Commute (star r) x →
        Commute z x → Commute (star z) x → Commute (u : E) x) ∧
      ∃ p : Path (1 : unitary E) u,
        ∀ a b, ‖(p a : E) - p b‖ ≤ (2 * Real.pi) * |(a : ℝ) - b| := by
…

lemma OAI.WeakPureInfiniteness.bufferedAbsorptionValue_relocate line 88

Source documentation

Conjugation by a target-commuting unitary relocates the whole source summand exactly.

lemma bufferedAbsorptionValue_relocate (w z t x : E) (m : ℕ) (u : unitary E)
    (hut : Commute (u : E) t) (hur : (u : E) * w ^ m = z) :
    (u : E) * bufferedAbsorptionValue w t x m * star (u : E) =
      t * (1 - z * star z) + z * x * star z := by
…

Mentions: OAI.WeakPureInfiniteness.bufferedAbsorptionValue

lemma OAI.WeakPureInfiniteness.exists_controlled_buffered_tail_swap line 107

Source documentation

A single target-commuting swap moves every tested generator's terminal copy to the same fixed internal range, with cost 2π, independently of depth.

lemma exists_controlled_buffered_tail_swap [Nontrivial E] {I : Type*}
    (w z : E) (hw : star w * w = 1) (hz : star z * z = 1)
    (hzw : star z * w = 0) (t : I → E)
    (htw : ∀ i, Commute w (t i)) (htsw : ∀ i, Commute (star w) (t i))
    (htz : ∀ i, Commute z (t i)) (htsz : ∀ i, Commute (star z) (t i))
    (m : ℕ) :
    ∃ u : unitary E,
      (∀ i x, (u : E) * bufferedAbsorptionValue w (t i) x (m + 1) * star (u : E) =
        t i * (1 - z * star z) + z * x * star z) ∧
      ∃ p : Path (1 : unitary E) u,
        ∀ a b, ‖(p a : E) - p b‖ ≤ (2 * Real.pi) * |(a : ℝ) - b| := by
…

Mentions: OAI.WeakPureInfiniteness.bufferedAbsorptionValue

lemma OAI.WeakPureInfiniteness.exists_canonical_controlled_tail_swaps line 133

Source documentation

All support and commutant conditions for the terminal swap come from the actual canonical vacuum split. The relocated source copy is explicit.

lemma exists_canonical_controlled_tail_swaps [Nontrivial E]
    (s t : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hst : bergRowsCommute s t) (n : ℕ) (κ : ℝ) (hκ : 0 < κ) :
    ∃ (D : BufferAbsorptionCorner E) (z : E),
      star z * z = 1 ∧ D.q * z = z ∧ 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‖ < κ) ∧
      ∀ m, ∃ u : unitary E,
        (∀ (i : ℕ) (x : E),
          (u : E) * bufferedAbsorptionValue D.w (t i) x (m + 1) * star (u : E) =
…

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