OAI/Analysis/FactorGeneration/ResidualMoments.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Valid residual-corner identities in the actual quotient. Compression centering requires two exact moments; global centering alone is insufficient.

  1. theorem OAI.Generator.Tracial.quotient_partial_residual_annihilation line 19
  2. theorem OAI.Generator.Tracial.quotient_residual_compression_trace line 34
  3. theorem OAI.Generator.Tracial.quotient_residual_centered line 49
  4. theorem OAI.Generator.Tracial.algebraPatchingWord_append line 55
  5. theorem OAI.Generator.Tracial.quotient_residual_word_centered line 62
  6. theorem OAI.Generator.Tracial.quotient_residual_signed_annihilation line 81
  7. theorem OAI.Generator.Tracial.quotient_residual_word_unit_left line 89
  8. theorem OAI.Generator.Tracial.quotient_residual_word_unit_right line 98
  9. theorem OAI.Generator.Tracial.quotient_residual_all_words_centered line 105
  10. theorem OAI.Generator.Tracial.quotient_residual_coefficient_centered line 130
  11. abbrev OAI.Generator.Tracial.ResidualWordIndex line 150
  12. def OAI.Generator.Tracial.residualWordValue line 152
  13. def OAI.Generator.Tracial.residualWordFamily line 157
  14. theorem OAI.Generator.Tracial.residualWordFamily_encode line 162
  15. theorem OAI.Generator.Tracial.residualWordFamily_contains_coefficient line 166
  16. theorem OAI.Generator.Tracial.residualWordFamily_contains_word line 170
  17. theorem OAI.Generator.Tracial.residualWordFamily_compression_centered line 177
  18. theorem OAI.Generator.Tracial.residualWordFamily_contains_run line 199
  19. theorem OAI.Generator.Tracial.residualWordFamily_contains_outer_run line 209
  20. def OAI.Generator.Tracial.algebraMixedTail line 224
  21. theorem OAI.Generator.Tracial.algebraMixedTail_normalize line 232

    Source documentation

    Every actual ordered mixed term is either the original word or an ordered increment word with enumerated internal blocks and an explicit old prefix.

    theorem algebraMixedTail_normalize (v w : Q τ ω) (x : ℕ → Q τ ω)
    (last : Option ℕ) (b s : Bool) (xs : List (Bool × Bool × ℕ)) :
    algebraMixedTail v w x last b s xs =
      algebraPatchingWord v (xs.map (fun a => (a.2.1,x a.2.2)) ++
        [(s,optionalCoefficient x last)]) ∨
    ∃ pre : List (Bool × ℕ), ∃ ys : List (Bool × ℕ), ∃ t : Bool, ∃ last' : Option ℕ,
      algebraMixedTail v w x last b s xs =
        algebraPatchingWord v (pre.map (fun a => (a.1,x a.2))) *
        algebraPatchingWord w (ys.map (fun a => (a.1,residualWordFamily τ ω v x a.2)) ++
          [(t,optionalCoefficient (residualWordFamily τ ω v x) last')]) := by
…

    Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.algebraMixedTail, OAI.Generator.Tracial.algebraPatchingWord, OAI.Generator.Tracial.optionalCoefficient, OAI.Generator.Tracial.residualWordFamily

  22. def OAI.Generator.Tracial.algebraWordCore line 283
  23. theorem OAI.Generator.Tracial.algebraWordCore_endpoints line 288
  24. theorem OAI.Generator.Tracial.algebraWordCore_map line 296
  25. theorem OAI.Generator.Tracial.algebraWordCore_support line 304
  26. theorem OAI.Generator.Tracial.algebraWordCore_compress line 317
  27. def OAI.Generator.Tracial.ExactOrderedMoments line 334
  28. theorem OAI.Generator.Tracial.exactOrderedMoments_core line 339
  29. theorem OAI.Generator.Tracial.trace_supported_cyclic_compression line 346
  30. theorem OAI.Generator.Tracial.exact_moment_of_cyclic_family line 356

    Source documentation

    Transfer exact moments from compressed internal coefficients and centered cyclic endpoint products. The scalar correction uses the moment with both endpoints equal to the unit.

    theorem exact_moment_of_cyclic_family (w f : Q τ ω)
    (hw : ∀ s,f*algebraSignedLetter w s=algebraSignedLetter w s ∧
      algebraSignedLetter w s*f=algebraSignedLetter w s)
    (y z : ℕ → Q τ ω) (k : ℕ → ℕ) (hk : ∀ i,f*y i*f=z (k i))
    (hc : ∀ a b : Option ℕ,∃ j : ℕ,∃ c : ℂ,
      f*(optionalCoefficient y b*optionalCoefficient y a)*f=z j+c • f)
    (hm : ExactOrderedMoments τ ω w z)
    (a b : Option ℕ) (xs : List (Bool × ℕ)) (s : Bool) :
    quotientTrace τ ω (optionalCoefficient y a*algebraPatchingWord w
      (xs.map (fun t => (t.1,y t.2)) ++ [(s,optionalCoefficient y b)]))=0 := by
…

    Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.algebraSignedLetter, OAI.Generator.Tracial.optionalCoefficient, OAI.Generator.Tracial.ExactOrderedMoments, OAI.Generator.Tracial.algebraPatchingWord

  31. def OAI.Generator.Tracial.quotientCornerCenter line 395
  32. theorem OAI.Generator.Tracial.quotientCornerCenter_supported line 398
  33. theorem OAI.Generator.Tracial.quotientCornerCenter_trace line 405
  34. theorem OAI.Generator.Tracial.quotientCornerCenter_decompose line 414
  35. abbrev OAI.Generator.Tracial.CyclicFamilyIndex line 420
  36. def OAI.Generator.Tracial.cyclicFamilyValue line 422
  37. def OAI.Generator.Tracial.cyclicResidualFamily line 426
  38. theorem OAI.Generator.Tracial.cyclicResidualFamily_encode line 431
  39. theorem OAI.Generator.Tracial.cyclicResidualFamily_supported line 435
  40. theorem OAI.Generator.Tracial.cyclicResidualFamily_centered line 449
  41. theorem OAI.Generator.Tracial.cyclicResidualFamily_internal line 463
  42. theorem OAI.Generator.Tracial.cyclicResidualFamily_outer line 468
  43. theorem OAI.Generator.Tracial.algebraSignedLetter_add' line 486
  44. theorem OAI.Generator.Tracial.ordered_sum_zero_of_all_mixed line 493

    Source documentation

    Distribute every signed letter while preserving the full multiplication order. The premise is checked for actual mixed terms, not scalar estimates.

    theorem ordered_sum_zero_of_all_mixed (v w : Q τ ω) (x : ℕ → Q τ ω)
    (last : Option ℕ) (s : Bool) (xs : List (Bool × ℕ)) (a : Q τ ω)
    (h : ∀ cs : List (Bool × Bool × ℕ),∀ b : Bool,
      quotientTrace τ ω (a*algebraMixedTail v w x last b s cs)=0) :
    quotientTrace τ ω (a*algebraPatchingWord (v+w)
      (xs.map (fun t => (t.1,x t.2)) ++ [(s,optionalCoefficient x last)]))=0 := by
…

    Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.algebraMixedTail, OAI.Generator.Tracial.algebraPatchingWord, OAI.Generator.Tracial.optionalCoefficient

  45. theorem OAI.Generator.Tracial.exactOrderedMoments_add_of_cyclic line 521