OAI/Analysis/OInfinity/NegativeBinary.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Binary encoding of each finite stabilized canonical row

Two consecutive explicit range completions define a shift from each prescribed generator to the next. Together with the first generator this is a coisometric binary pair. No general even-row comparison is used.

  1. def OAI.WeakPureInfiniteness.skipSecond line 20
  2. lemma OAI.WeakPureInfiniteness.skipSecond_injective line 23
  3. lemma OAI.WeakPureInfiniteness.skipSecond_ne_one line 39
  4. lemma OAI.WeakPureInfiniteness.successive_full_rows_binary line 50

    Source documentation

    Removing the second range of a full row leaves a shift isometry whose complement is exactly that second range.

    lemma successive_full_rows_binary (m : ℕ) (r : Fin (m + 1) → E) (R : Fin (m + 2) → E)
    (hr : ∀ i j, star (r i) * r j = if i = j then 1 else 0)
    (hR : ∀ i j, star (R i) * R j = if i = j then 1 else 0)
    (hrsum : (∑ i, r i * star (r i)) = 1)
    (hRsum : (∑ i, R i * star (R i)) = 1) :
    ∃ A B : E, star A * A = 1 ∧ star B * B = 1 ∧ star A * B = 0 ∧
      A * star A + B * star B = 1 ∧ B = R 1 ∧
      ∀ i : Fin m, A * r i.succ = R i.succ.succ := by
…
  5. lemma OAI.WeakPureInfiniteness.exists_canonicalNegative_binary_pair line 90

    Source documentation

    Every finite initial segment of the actual stabilized canonical row extends to a binary pair in its same corner. The empty transition sum at m=0 is included.

    lemma exists_canonicalNegative_binary_pair [Nontrivial E] (s : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0) (m : ℕ) :
    ∃ A B : E,
      star A * A = canonicalTailProjection s 1 ∧
      star B * B = canonicalTailProjection s 1 ∧ star A * B = 0 ∧
      A * star A + B * star B = canonicalTailProjection s 1 ∧
      B = canonicalNegativeRow s 0 ∧
      ∀ i : Fin m, A * canonicalNegativeRow s i = canonicalNegativeRow s (i + 1) := by
…

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

  6. lemma OAI.WeakPureInfiniteness.exists_canonicalNegative_binary_encoding line 132