BufferedProperComparison.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual common-range binary row

Three orthogonal buffer isometries construct the full binary row in the range of both forward shrinks. Its commutation with the prescribed rows follows from the explicit zero-corner completion polynomial. This discharges the common-range row premise of the preceding comparison.

lemma OAI.WeakPureInfiniteness.exists_buffer_shrink_range_pair line 22
Source documentation
A proper three-row supplies the full binary row needed in the shrink range, including commutation with any prescribed finite family.
```
lemma exists_buffer_shrink_range_pair [Nontrivial E]
    (R : Fin 3 → E)
    (hR : ∀ i j, star (R i) * R j = if i = j then 1 else 0) :
    let p := 1 - R 0 * star (R 0)
…
```

lemma OAI.WeakPureInfiniteness.exists_connected_encoded_comparison_of_buffer line 85

Source documentation

The common-range row is now constructed from the buffer. The only completion input is the actual connected cocycle to one shared reference.

lemma exists_connected_encoded_comparison_of_buffer [Nontrivial E]
    (R : Fin 3 → E)
    (hR : ∀ i j, star (R i) * R j = if i = j then 1 else 0)
    (b a c : Fin 2 → E)
    (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)
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute