RelativeCompletedComparison.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Relative comparison with the prescribed complementary action

The corner path below is constructed from the pointwise complementary identity, rather than inferred from ambient connectedness. It allows the completed-row comparison to keep the external corner fixed exactly.

lemma OAI.WeakPureInfiniteness.exists_projectionCorner_unitary_path line 19

lemma OAI.WeakPureInfiniteness.exists_relative_completed_row_comparison line 71

Source documentation

Both actual completion records are used in the same corner. The three-buffer row constructs the intermediate binary pair; the final ambient unitary fixes the complement exactly.

lemma exists_relative_completed_row_comparison {n : ℕ}
    (q : E) (hq : star q = q) (hqq : q * q = q) (hq0 : q ≠ 0)
    (b : Fin 2 → E)
    (hb : ∀ i j, star (b i) * b j = if i = j then q else 0)
    (hbs : (∑ i, b i * star (b i)) = q)
    (x y : Fin (n + 1) → E)
    (A : RelativeBinaryCompletion q b x) (B : RelativeBinaryCompletion q b y)
    (R : Fin 3 → E)
    (hRs : ∀ i, q * R i = R i ∧ R i * q = R i)
    (hR : ∀ i j, star (R i) * R j = if i = j then q else 0)
    (hAR : bergRowsCommute A.row R) (hBR : bergRowsCommute B.row R)
    (ε : ℝ) (hε : 0 < ε) :
…

Mentions: OAI.WeakPureInfiniteness.RelativeBinaryCompletion, OAI.WeakPureInfiniteness.bergRowsCommute