NegativeCompletion.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Finite leaf matching for the stabilized canonical row

The remaining projection of the negative-corner row is explicitly the orthogonal sum of two copies of its unit. Matching the finite leaves and using the concrete binary pair fills this projection without a projection-classification assumption.

def OAI.WeakPureInfiniteness.negativeLeafMatch line 21
Source documentation
Match the common tail and each of finitely many range leaves.
```
def negativeLeafMatch {I : Type*} [Fintype I]
    (e r : E) (x y : I → E) : E := r * e + ∑ i, x i * star (y i)
```
lemma OAI.WeakPureInfiniteness.negativeLeafMatch_gram line 24
lemma OAI.WeakPureInfiniteness.negativeLeafMatch_range line 55
lemma OAI.WeakPureInfiniteness.negativeLeafMatch_cross line 87
def OAI.WeakPureInfiniteness.negativeLeftLeaf line 110
Source documentation
The first half of the matched range leaves.
```
def negativeLeftLeaf (s : ℕ → E) (n : ℕ) : Fin (n + 1) → E :=
…
```
def OAI.WeakPureInfiniteness.negativeRightLeaf line 114
Source documentation
The second half of the matched range leaves.
```
def negativeRightLeaf (s : ℕ → E) (n : ℕ) : Fin (n + 1) → E :=
…
```
lemma OAI.WeakPureInfiniteness.twoLetter_gram line 117
lemma OAI.WeakPureInfiniteness.negativeLeftLeaf_gram line 126
lemma OAI.WeakPureInfiniteness.negativeRightLeaf_gram line 140
lemma OAI.WeakPureInfiniteness.negativeLeaf_cross line 154
lemma OAI.WeakPureInfiniteness.negativeLeaf_tail_support line 168
lemma OAI.WeakPureInfiniteness.negativeLeafMatch_pair line 200
Source documentation
The two finite leaf maps each have the required unit e₁, and their ranges are orthogonal.
```
lemma negativeLeafMatch_pair (s : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0) (n : ℕ) :
    let e := canonicalTailProjection s (n + 2)
…
```
Mentions: OAI.WeakPureInfiniteness.canonicalTailProjection
lemma OAI.WeakPureInfiniteness.negativeLeaf_residual line 234
lemma OAI.WeakPureInfiniteness.negativeLeafMatch_range_sum line 265

lemma OAI.WeakPureInfiniteness.negativeMatchedPair_completion line 290

Source documentation

Combine the two matched copies with the explicit coisometric pair.

lemma negativeMatchedPair_completion (q a b u v : E)
    (hq : star q = q) (hqq : q * q = q)
    (haa : star a * a = q) (hbb : star b * b = q) (hab : star a * b = 0)
    (huu : star u * u = q) (hvv : star v * v = q) (huv : star u * v = 0)
    (huvs : u * star u + v * star v = q) :
    star (a * star u + b * star v) * (a * star u + b * star v) = q ∧
      (a * star u + b * star v) * star (a * star u + b * star v) =
        a * star a + b * star b := by
…

lemma OAI.WeakPureInfiniteness.exists_canonicalNegative_completion line 318

Source documentation

An actual relative isometry fills the full finite residual of the stabilized canonical row, with no classification premise.

lemma exists_canonicalNegative_completion [Nontrivial E] (s : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0) (n : ℕ) :
    ∃ c : E, star c * c = canonicalTailProjection s 1 ∧
      c * star c = canonicalTailProjection s 1 -
        ∑ i : Fin n, canonicalNegativeRow s i * star (canonicalNegativeRow s i) := by
…

Mentions: OAI.WeakPureInfiniteness.canonicalTailProjection, OAI.WeakPureInfiniteness.canonicalNegativeRow

lemma OAI.WeakPureInfiniteness.exists_canonicalNegative_full_row line 346

Source documentation

Append one explicit range filler while retaining every prescribed finite stabilized generator exactly.

lemma exists_canonicalNegative_full_row [Nontrivial E] (s : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0) (n : ℕ) :
    ∃ r : Fin (n + 1) → E,
      (∀ i : Fin n, r i.succ = canonicalNegativeRow s i) ∧
      (∀ i j, star (r i) * r j = if i = j then canonicalTailProjection s 1 else 0) ∧
      (∑ i, r i * star (r i)) = canonicalTailProjection s 1 := by
…

Mentions: OAI.WeakPureInfiniteness.canonicalNegativeRow, OAI.WeakPureInfiniteness.canonicalTailProjection