OAI/Analysis/OInfinity/EvenModeCAR.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Disjoint modes for the finite even-row shift

Twisting each geometric mode by the same disjoint reference symmetry removes the shift parity and preserves its CAR relations. These are actual elements of the given even-row corner, with the quantitative shift estimate inherited from the finite geometric sums.

  1. lemma OAI.WeakPureInfiniteness.mode_cross_mul line 20
  2. lemma OAI.WeakPureInfiniteness.mode_cross_anticommute line 32
  3. lemma OAI.WeakPureInfiniteness.carReferenceTwist_mul line 49

    Source documentation

    The product identity responsible for preserving CAR under a common odd symmetry.

    lemma carReferenceTwist_mul (q u c d : E) (huu : u * u = q)
    (hdq : d * q = d) (hud : u * d + d * u = 0) :
    (c * u) * (d * u) = -(c * d) := by
…
  4. lemma OAI.WeakPureInfiniteness.carReferenceTwist_star_mul line 58
  5. lemma OAI.WeakPureInfiniteness.evenGeometricMode_anticommute line 80
  6. lemma OAI.WeakPureInfiniteness.evenGeometricMode_disjoint_star_anticommute line 88
  7. lemma OAI.WeakPureInfiniteness.evenModeSymmetry_star line 104
  8. lemma OAI.WeakPureInfiniteness.evenModeSymmetry_sq line 109
  9. lemma OAI.WeakPureInfiniteness.evenModeSymmetry_anticommute line 119
  10. lemma OAI.WeakPureInfiniteness.evenEigenMode_anticommute line 136
  11. lemma OAI.WeakPureInfiniteness.evenEigenMode_star_anticommute line 152
  12. lemma OAI.WeakPureInfiniteness.evenEigenMode_gram line 179
  13. lemma OAI.WeakPureInfiniteness.evenEigenMode_support line 201
  14. def OAI.WeakPureInfiniteness.evenBlockMode line 217

    Source documentation

    Consecutive disjoint geometric blocks, with block zero reserved for the reference.

    def evenBlockMode {m : ℕ} (r : Fin 2 × Fin n → E) (L : ℕ)
    (ζ : Fin m → ℂ) (i : Fin m) : E :=
…
  15. lemma OAI.WeakPureInfiniteness.block_separate line 221
  16. lemma OAI.WeakPureInfiniteness.evenBlockMode_CAR line 232
  17. lemma OAI.WeakPureInfiniteness.evenBlockMode_support line 256
  18. lemma OAI.WeakPureInfiniteness.evenBlockMode_shift_error line 262