OAI/Dynamics/ThreeTorus/CyclicPrediction.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.ThreeTorus.ActualColoredBlocks line 17

   Source documentation

   A finite trace of actual centered blocks. A is exactly the sum of their estimators. This data retains each anchor and each physical passage.

   inductive ActualColoredBlocks {m : ℕ} (C : ColoredState (Fin m)) :
       ColoredState (Fin m) → ℕ → Equiv.Perm TripleTorus → (UnitAddCircle → ℂ) → Prop
     | nil : ActualColoredBlocks C C 0 (Equiv.refl _) (fun _ => 0)
     | snoc {E F : ColoredState (Fin m)} {k : ℕ} {α β : Equiv.Perm TripleTorus}
         {A D : UnitAddCircle → ℂ} (h : ActualColoredBlocks C E k α A)
         (hb : ActualColoredBlock E F β D) :
         ActualColoredBlocks C F (k+1) (α.trans β) (fun z => A z+D z)
   
   namespace ActualColoredBlocks
   variable {m : ℕ} {C E : ColoredState (Fin m)} {k : ℕ} {α : Equiv.Perm TripleTorus}
       {A : UnitAddCircle → ℂ} (h : ActualColoredBlocks C E k α A)
   include h

   Mentions: OAI.ThreeTorus.ColoredState, OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.ActualColoredBlock

2. lemma OAI.ThreeTorus.ActualColoredBlocks.continuous line 29
3. lemma OAI.ThreeTorus.ActualColoredBlocks.preserves line 33
4. lemma OAI.ThreeTorus.ActualColoredBlocks.physicalError_eq line 37
5. lemma OAI.ThreeTorus.ActualColoredBlocks.estimator_continuous line 44
6. lemma OAI.ThreeTorus.ActualColoredBlocks.estimator_smooth line 48
7. lemma OAI.ThreeTorus.ActualColoredBlocks.estimator_reflection line 53
8. lemma OAI.ThreeTorus.integral_blockPreviousError_eq line 59
9. lemma OAI.ThreeTorus.block_increment_budget line 68
10. theorem OAI.ThreeTorus.actual_repeated_blocks line 79

    Source documentation

    Source04's repeated blocks, with every new center formed from the actual current densities. Physical transport, not a spectral model, keeps the mass strictly below two. No future uniform strength bound is required.

    theorem actual_repeated_blocks {m : ℕ} (C : ColoredState (Fin m))
        (τR : Fin m → Fin m) (hτR : Involutive τR) (hrC : C.Reflection τR)
        (tags : Fin m → ℂ) (htags : ∀ r, ‖tags r‖ ≤ 1)
        (htrR : ∀ r, tags (τR r) = conj (tags r))
        {delta ε κ : ℝ} (hd : 0 < delta) (hd1 : delta ≤ 1/100) (hε : 0 < ε) (hκ : 0 < κ)
        (hmass : (∫ z, blockTotal C.density z ∂phaseHaar) < 2) (K : ℕ) :
        ∃ E : ColoredState (Fin m), ∃ α : Equiv.Perm TripleTorus, ∃ A : UnitAddCircle → ℂ,
          ActualColoredBlocks C E K α A ∧
          (∀ r, physicalError (C.vector r) (E.vector r ∘ α) < ε) ∧
          ((∫ z, Real.sqrt (blockTotal C.density z) ∂phaseHaar)-400*(K:ℝ)*delta^2 ≤
            ∫ z, Real.sqrt (blockTotal E.density z) ∂phaseHaar) ∧
          ((∫ z, blockPreviousError E.density tags A K z ∂phaseHaar) ≤ (K:ℝ)*(5/delta)) ∧
    …

    Mentions: OAI.ThreeTorus.ColoredState, OAI.ThreeTorus.blockTotal, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.ActualColoredBlocks, OAI.ThreeTorus.physicalError, OAI.ThreeTorus.blockPreviousError

11. lemma OAI.ThreeTorus.exists_prediction_budget line 144

    Source documentation

    δ and K are fixed before any block strengths or lengths, with the exact source choice K=ceil(10/(ε²δ)).

    lemma exists_prediction_budget {ε τ : ℝ} (hε : 0 < ε) (hτ : 0 < τ) :
        ∃ δ : ℝ, 0 < δ ∧ δ ≤ 1/100 ∧
          let K := ⌈10/(ε^2*δ)⌉₊
    …

12. lemma OAI.ThreeTorus.averaged_prediction_identity line 181
13. theorem OAI.ThreeTorus.actual_density_prediction line 209

    Source documentation

    The source prediction estimate, for actual reflected packet passages. The smooth-neighborhood requirement is not included here: it remains to be threaded through the passage selection before exporting Proposition 4.1.

    theorem actual_density_prediction {m : ℕ} (C : ColoredState (Fin m))
        (τR : Fin m → Fin m) (hτR : Involutive τR) (hrC : C.Reflection τR)
        (tags : Fin m → ℂ) (htags : ∀ r, ‖tags r‖ ≤ 1)
        (htrR : ∀ r, tags (τR r) = conj (tags r))
        {ε τ η κ : ℝ} (hε : 0 < ε) (hτ : 0 < τ) (hη : 0 < η) (hκ : 0 < κ)
        (hmass : (∫ z, blockTotal C.density z ∂phaseHaar) < 2) :
        ∃ E : ColoredState (Fin m), ∃ α : Equiv.Perm TripleTorus,
          ∃ Ψ : UnitAddCircle → ℂ, ∃ K : ℕ, ∃ A : UnitAddCircle → ℂ,
          0 < K ∧ ActualColoredBlocks C E K α A ∧ Ψ = (fun z => A z/(K:ℂ)) ∧
          (∀ r, physicalError (C.vector r) (E.vector r ∘ α) < η) ∧
          ((∫ z, Real.sqrt (blockTotal C.density z) ∂phaseHaar)-τ <
            ∫ z, Real.sqrt (blockTotal E.density z) ∂phaseHaar) ∧
    …

    Mentions: OAI.ThreeTorus.ColoredState, OAI.ThreeTorus.blockTotal, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.ActualColoredBlocks, OAI.ThreeTorus.physicalError

14. def OAI.ThreeTorus.ColoredState.weightedVector line 259

    Source documentation

    Literal packet spectral calculus, evaluated in the current coordinates.

    def weightedVector (a : C.Index → UnitAddCircle → ℂ) (x : TripleTorus) : ℂ :=
    …

    Mentions: OAI.ThreeTorus.TripleTorus

15. lemma OAI.ThreeTorus.ColoredState.weightedVector_continuous line 263
16. lemma OAI.ThreeTorus.ColoredState.weighted_packet_spectral line 272
17. lemma OAI.ThreeTorus.ColoredState.weightedVector_energy line 290
18. lemma OAI.ThreeTorus.ColoredState.weightedVector_sub line 328
19. lemma OAI.ThreeTorus.ColoredState.weightedVector_tags line 333
20. lemma OAI.ThreeTorus.ColoredState.weighted_density_colors line 343
21. lemma OAI.ThreeTorus.ColoredState.physical_prediction_energy line 368

    Source documentation

    The density prediction error is exactly the squared physical L² error for the literal packet multiplier; no cyclic-space calculus is assumed.

    lemma physical_prediction_energy (b : Fin m → ℂ) {Ψ : UnitAddCircle → ℂ}
        (hΨ : Continuous Ψ) :
        (∫ x, ‖C.weightedVector (fun _ => Ψ) x-∑ r, b r*C.vector r x‖^2 ∂tripleVolume) =
          ∑ r, ∫ z, C.density r z*‖Ψ z-b r‖^2 ∂phaseHaar := by
    …

    Mentions: OAI.ThreeTorus.tripleVolume, OAI.ThreeTorus.phaseHaar

22. def OAI.ThreeTorus.ColoredState.laurent line 393

    Source documentation

    A finite Laurent polynomial in the actual twist Koopman operator.

    def laurent (c : ℤ →₀ ℂ) (x : TripleTorus) : ℂ :=
    …

    Mentions: OAI.ThreeTorus.TripleTorus

23. lemma OAI.ThreeTorus.ColoredState.laurent_eq_multiplier line 397
24. lemma OAI.ThreeTorus.ColoredState.laurent_continuous line 410
25. lemma OAI.ThreeTorus.ColoredState.multiplier_error_bound line 417
26. lemma OAI.ThreeTorus.ColoredState.exists_laurent_approx line 444

    Source documentation

    Continuous spectral multiplication lies in the physical cyclic space, proved by actual finite Laurent approximants, with any squared L² tolerance.

    lemma exists_laurent_approx {Ψ : UnitAddCircle → ℂ} (hΨ : Continuous Ψ)
        {ε : ℝ} (he : 0 < ε) :
        ∃ c : ℤ →₀ ℂ, physicalError (C.weightedVector (fun _ => Ψ)) (C.laurent c) < ε := by
    …

    Mentions: OAI.ThreeTorus.physicalError

27. lemma OAI.ThreeTorus.physicalError_symm line 485
28. lemma OAI.ThreeTorus.physicalError_const_mul line 489
29. lemma OAI.ThreeTorus.physicalError_tagged_sum line 495
30. theorem OAI.ThreeTorus.actual_cyclic_prediction line 517

    Source documentation

    Actual finite Laurent approximation to the OLD tagged packet sum after reflected signal blocks. Neither a cyclic-space oracle nor a formal spectral operator is used: the witness is a literal finite sum of twist iterates.

    theorem actual_cyclic_prediction {m : ℕ} (C : ColoredState (Fin m))
        (τR : Fin m → Fin m) (hτR : Involutive τR) (hrC : C.Reflection τR)
        (tags : Fin m → ℂ) (htags : ∀ r, ‖tags r‖ ≤ 1)
        (htrR : ∀ r, tags (τR r) = conj (tags r))
        {ε τ η κ : ℝ} (hε : 0 < ε) (hτ : 0 < τ) (hη : 0 < η) (hκ : 0 < κ)
        (hmass : (∫ z, blockTotal C.density z ∂phaseHaar) < 2) :
        ∃ E : ColoredState (Fin m), ∃ α : Equiv.Perm TripleTorus,
          ∃ c : ℤ →₀ ℂ, ∃ K : ℕ, ∃ A : UnitAddCircle → ℂ,
          0 < K ∧ ActualColoredBlocks C E K α A ∧
          (∀ r, physicalError (C.vector r) (E.vector r ∘ α) < η) ∧
          ((∫ z, Real.sqrt (blockTotal C.density z) ∂phaseHaar)-τ <
            ∫ z, Real.sqrt (blockTotal E.density z) ∂phaseHaar) ∧
    …

    Mentions: OAI.ThreeTorus.ColoredState, OAI.ThreeTorus.blockTotal, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.ActualColoredBlocks, OAI.ThreeTorus.physicalError

31. lemma OAI.ThreeTorus.physicalDist_const_mul line 577
32. lemma OAI.ThreeTorus.finite_weighted_dist_le line 582
33. theorem OAI.ThreeTorus.exists_colored_separation_small line 597

    Source documentation

    The TWO separating passages simultaneously approximate the total vector, its arbitrarily tagged test, and total density. Tags are fixed BEFORE choice.

    theorem exists_colored_separation_small {n : ℕ} (F : PassagePackets (Fin n))
        (hd : ∀ i j, i ≠ j → F.m i = F.m j → Disjoint (F.cylinderCore i) (F.cylinderCore j))
        (τ : Fin n → Fin n) (hτ : Involutive τ) (hr : F.Reflection τ)
        (b : Fin n → ℂ) (Q : PhysicalJetData) (frame : PhysicalFrame)
        {ε κ ζ : ℝ} (hε : 0 < ε) (hκ : 0 < κ) (hζ : 0 < ζ) :
        ∃ C : ColoredState (Fin n), ∃ α : Equiv.Perm TripleTorus, ∃ frame' : PhysicalFrame,
          Continuous α ∧ MeasurePreserving α tripleVolume tripleVolume ∧
          frame'.chart=frame.chart.trans α ∧ C.Reflection τ ∧
          (∃ δ : ℝ, 0 < δ ∧ δ < 1/8 ∧ δ < κ ∧ C.packets.GoodArc δ) ∧
          Q.Close ζ frame F.V frame' C.packets.V ∧
          physicalDist (finitePacketVector F.m F.A) (C.totalVector ∘ α) < ε ∧
          physicalDist (fun x => ∑ i, b i*packet (F.m i) (F.A i) x)
    …

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.PhysicalJetData, OAI.ThreeTorus.PhysicalFrame, OAI.ThreeTorus.ColoredState, OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.tripleVolume, OAI.ThreeTorus.physicalDist, OAI.ThreeTorus.finitePacketVector, OAI.ThreeTorus.packet

34. theorem OAI.ThreeTorus.exists_prediction_ready line 658

    Source documentation

    Full source05 preparation through BOTH support-separating passages. The same arbitrary tags, reality, physical errors and total density are retained.

    theorem exists_prediction_ready (F : MeasurablePackets)
        {τ : F.Index → F.Index} (hr : F.Reflection τ)
        {δ l u : ℝ} (hδ : 0 ≤ δ) (hd : δ < 1/2) (hdl : δ < l) (hud : u < 1-δ)
        (hsupp : F.Supported l u)
        (V : ℝ → ℝ) (hp : Periodic V 1) (hs : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
        (hv : ∀ x ∈ Ioo δ (1-δ), 0 < deriv V x)
        (hflat : F.spectrum (fun z => (hp.lift z:UnitAddCircle))=phaseHaar)
        {h : TripleTorus → ℂ} (hh : Continuous h) (hrh : ∀ x, conj (h x)=h x)
        (hch : ∫ x, h x ∂tripleVolume=0) (hbh : ∀ x, ‖h x‖ ≤ 1)
        (Q : PhysicalJetData) (frame : PhysicalFrame)
        {ε κ ζ : ℝ} (hε : 0 < ε) (hκ : 0 < κ) (hζ : 0 < ζ) :
        ∃ n : ℕ, ∃ C : ColoredState (Fin n), ∃ ρ : Fin n → Fin n,
    …

    Mentions: OAI.ThreeTorus.MeasurablePackets, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.tripleVolume, OAI.ThreeTorus.PhysicalJetData, OAI.ThreeTorus.PhysicalFrame, OAI.ThreeTorus.ColoredState