BufferedRelativeWitness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

An actual relative witness after the second buffer

Both completion records and the common range row are constructed. The only hypotheses concern the given finite proper rows in the first row's commutant and their shared full binary reference corner.

def OAI.WeakPureInfiniteness.RelativeBinaryCompletion.map line 25

lemma OAI.WeakPureInfiniteness.exists_buffered_relative_witness line 66

Source documentation

The actual second-buffer construction removes the completion-record hypotheses from the relative comparison.

lemma exists_buffered_relative_witness [Nontrivial E]
    (U : Ultrafilter ℕ) [Fact ((U : Filter ℕ) ≤ atTop)]
    (R : ℕ → E) (hR : ∀ i j, star (R i) * R j = if i = j then 1 else 0)
    (q : StarSubalgebra.centralizer ℂ (Set.range R))
    (hq : star q = q) (hqq : q * q = q) (hq0 : q ≠ 0)
    (n : ℕ) (x y : Fin (n + 2) → StarSubalgebra.centralizer ℂ (Set.range R))
    (hxs : ∀ i, q * x i = x i ∧ x i * q = x i)
    (hys : ∀ i, q * y i = y i ∧ y i * q = y i)
    (hx : ∀ i j, star (x i) * x j = if i = j then q else 0)
    (hy : ∀ i j, star (y i) * y j = if i = j then q else 0)
    (b : Fin 2 → StarSubalgebra.centralizer ℂ (Set.range R))
    (hb : ∀ i j, star (b i) * b j = if i = j then q else 0)
…