RowCompletionBase.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The actual base path of the common-corner shrink

Binary completions chosen with connected left cocycles have a connected base comparison. The proof identifies that base with compression of the literal cocycle product by one fixed isometry. No general claim about a corner stabilizer or about the ambient unitary group is used.

lemma OAI.WeakPureInfiniteness.coisometry_filler_cross line 22

Source documentation

The cross product of two fillers with the same initial projection is the standard compression of their middle unitary product.

lemma coisometry_filler_cross (A y : E) (hA : A * star A = 1)
    (hy : star y * y = 1) (hpy : (star A * A) * y = y) (u v : unitary E) :
    star (1 - star A * A + y * (star (v : E) * A)) *
        (1 - star A * A + y * (star (u : E) * A)) =
      (binaryCornerUnitary (star A) (by simpa only [star_star] using hA) (v * star u) : E) := by
…

Mentions: OAI.WeakPureInfiniteness.binaryCornerUnitary

lemma OAI.WeakPureInfiniteness.binaryShrinkValue_reference line 60
Source documentation
Factoring the reference row out of the finite transfer keeps the initial projection independent of the chosen completion cocycle.
```
lemma binaryShrinkValue_reference (r b : Fin 2 → E) (u : unitary E) :
    binaryShrinkValue r (fun i => star (u : E) * b i) 1 =
      1 - star (finiteCuntzTransfer r b 1) * finiteCuntzTransfer r b 1 +
        r 1 * (star (u : E) * finiteCuntzTransfer r b 1) := by
…
```
Mentions: OAI.WeakPureInfiniteness.binaryShrinkValue, OAI.WeakPureInfiniteness.finiteCuntzTransfer
lemma OAI.WeakPureInfiniteness.finiteCuntzTransfer_reference_coisometry line 80
Source documentation
The fixed isometry and the full reference row give the exact base identity used in the two common-corner comparisons.
```
lemma finiteCuntzTransfer_reference_coisometry (r b : Fin 2 → E)
    (hr : ∀ i j, star (r i) * r j = if i = j then 1 else 0)
    (hbs : (∑ i, b i * star (b i)) = 1) :
    finiteCuntzTransfer r b 1 * star (finiteCuntzTransfer r b 1) = 1 := by
…
```
Mentions: OAI.WeakPureInfiniteness.finiteCuntzTransfer
lemma OAI.WeakPureInfiniteness.binaryShrinkValue_reference_cross line 90

lemma OAI.WeakPureInfiniteness.binaryShrinkValue_reference_cross_joined line 121

Source documentation

The base product is connected because its two prescribed cocycles are connected. This is the concrete path, rather than an ambient K1 claim.

lemma binaryShrinkValue_reference_cross_joined (r b : 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)
    (u v : unitary E) (hu : Joined (1 : unitary E) u) (hv : Joined (1 : unitary E) v) :
    ∃ K : unitary E, Joined (1 : unitary E) K ∧
      (K : E) = star (binaryShrinkValue r (fun i => star (v : E) * b i) 1) *
        binaryShrinkValue r (fun i => star (u : E) * b i) 1 := by
…

Mentions: OAI.WeakPureInfiniteness.binaryShrinkValue