ConnectedProperComparison.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Connected comparison using two forward shrinks

The two shrinks have the same final projection. Their literal base product is the compression of the prescribed connected completion cocycles. Thus the path used here never requires an ambient-to-relative connectedness inference, and its final unitary has no leftover complementary block.

lemma OAI.WeakPureInfiniteness.compressed_binary_word line 20
lemma OAI.WeakPureInfiniteness.compressed_binary_gram line 38
lemma OAI.WeakPureInfiniteness.compressed_binary_sum line 48
lemma OAI.WeakPureInfiniteness.unitary_commutes_projection_of_fixed_complement line 66
lemma OAI.WeakPureInfiniteness.unitary_inverse_comparison line 76

lemma OAI.WeakPureInfiniteness.exists_connected_forward_shrink_comparison line 94

Source documentation

This is the quantitative two-shrink assembly, with the base connectedness supplied by the actual completion formula. All coefficients at the endpoint are genuine unitaries; there is no polar correction or residual corner.

lemma exists_connected_forward_shrink_comparison [Nontrivial E]
    (r b a c d : Fin 2 → E)
    (hr : ∀ i j, star (r i) * r j = if i = j then 1 else 0)
    (hb : ∀ i j, star (b i) * b j = if i = j then 1 else 0)
    (hbs : (∑ i, b i * star (b i)) = 1)
    (ha : ∀ i j, star (a i) * a j = if i = j then 1 else 0)
    (has : (∑ i, a i * star (a i)) = 1)
    (hc : ∀ i j, star (c i) * c j = if i = j then 1 else 0)
    (hcs : (∑ i, c i * star (c i)) = 1)
    (har : bergRowsCommute a r) (hcr : bergRowsCommute c r)
    (u v : unitary E) (hu : Joined (1 : unitary E) u) (hv : Joined (1 : unitary E) v)
    (hua : ∀ j, (u : E) * a j = b j) (hvc : ∀ j, (v : E) * c j = b j)
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute