OAI/Geometry/HarmonicGrowth/GlobalControl.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicCounterexample.LinearODE.weighted_slope_gap_deriv line 13
2. lemma OAI.HarmonicCounterexample.LinearODE.riccati_quadratic_upper line 37
3. lemma OAI.HarmonicCounterexample.LinearODE.symmetric_norm_bound line 71
4. theorem OAI.HarmonicCounterexample.LinearODE.actual_slope_norm_bound line 100

   Source documentation

   The history-independent Riccati bound is proved for the actual center-regular PB solution. It is not an assumption on an arbitrary incoming solution.

   theorem actual_slope_norm_bound {A : ℝ → E →L[ℝ] E} {p : ℝ → ℝ}
       (hA : Continuous A) (hp : Continuous p) {MA Mp : ℝ}
       (hMA : 0 ≤ MA) (hMp : 0 ≤ Mp)
       (hAn : ∀ t,‖A t‖ ≤ MA) (hpn : ∀ t,|p t| ≤ Mp)
       (hAs : ∀ t x y,inner ℝ (A t x) y=inner ℝ x (A t y))
       (hAp : ∀ t x,0 ≤ inner ℝ x (A t x))
       {l B : ℝ} (hl : 0 < l) (hAc : ∀ t ≤ 0,∀ x,A t x=(l*(l+B)) • x)
       (hpc : ∀ t ≤ 0,p t=B) {t : ℝ} (ht : 0 ≤ t) :
       ‖slope A p l t‖ ≤ l+MA+Mp+1 := by
   …

   Mentions: OAI.HarmonicCounterexample.LinearODE.slope

5. theorem OAI.HarmonicCounterexample.LinearODE.uniform_round_reset line 155

   Source documentation

   A single late threshold resets EVERY positive symmetric bounded history. Only the actual preceding round interval is used.

   theorem uniform_round_reset (basis : OrthonormalBasis ι ℝ E)
       {α p : ℝ → ℝ} (hp : Continuous p) {β p₀ γ θ B l B₀ MA Mp : ℝ}
       (hαlim : Tendsto α atTop (𝓝 β)) (hplim : Tendsto p atTop (𝓝 p₀))
       (hγ : 0 < γ) (hθ : 0 < θ) (hpl : ∀ᶠ t in atTop,γ ≤ p t)
       (hroot : β*B-p₀*θ-θ^2=0) (hMA : 0 ≤ MA) (hMp : 0 ≤ Mp)
       (hpn : ∀ t,|p t| ≤ Mp) (hl : 0 < l) (hpc : ∀ t ≤ 0,p t=B₀)
       {ε : ℝ} (hε : 0 < ε) :
       ∃ J : ℕ,∀ j,J ≤ j → ∀ A : ℝ → E →L[ℝ] E,
         Continuous A → (∀ t,‖A t‖ ≤ MA) →
         (∀ t x y,inner ℝ (A t x) y=inner ℝ x (A t y)) →
         (∀ t x,0 ≤ inner ℝ x (A t x)) →
         (∀ t ≤ 0,∀ x,A t x=(l*(l+B₀)) • x) →
   …

6. structure OAI.HarmonicCounterexample.LinearODE.HistoryGeometry line 239

   Source documentation

   Primitive radial coefficients and fixed angular operators. All fields are scalar/asymptotic or pointwise geometric facts; no transmission/reset/growth conclusion is part of this data.

   structure HistoryGeometry (S : PulseSystem E ι κ) where
   …

   Mentions: OAI.HarmonicCounterexample.LinearODE.PulseSystem

7. def OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.coefficient line 268
8. def OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.bound line 271
9. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.bound_nonneg line 276
10. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.coefficient_smooth line 286
11. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.coefficient_bound line 291
12. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.coefficient_nonnegative line 300
13. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.coefficient_symmetric line 313
14. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.coefficient_center line 323
15. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.coefficient_round line 330
16. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.coefficient_rest line 336
17. theorem OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.uniform_incoming line 362

    Source documentation

    Uniform reset for the explicit smooth angular stream, including the first active period and arbitrary prior admissible control choices.

    theorem HistoryGeometry.uniform_incoming {ε : ℝ} (hε : 0 < ε) :
        ∃ J : ℕ,∀ j0 j,J ≤ j → ∀ s : ℕ → Fin n → ℝ,
          (∀ k,j0 ≤ k → ∀ t i,packetStretch (s k) (pulse k) t i ∈ Icc (1/2:ℝ) (3/2)) →
          ∀ b,‖orthogonalMatrix (S.basis b) (slope (G.coefficient slot s j0 b) G.drift (G.l b) (time j))-
            S.θ b • (1:Matrix (ι b) (ι b) ℝ)‖ ≤ ε := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix, OAI.HarmonicCounterexample.LinearODE.slope

18. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.uniform_radial_tail line 387
19. theorem OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.eventual_history_conditions line 406

    Source documentation

    All scalar and incoming thresholds simultaneously, chosen BEFORE the start index, entire control stream, and current history.

    theorem HistoryGeometry.eventual_history_conditions (T₀ : ℝ) {ρ : ℝ} (hρ : 0 < ρ) :
        ∃ J : ℕ,∀ j0 j,J ≤ j0 → j0 ≤ j →
          T₀ ≤ pulse j ∧ ρ/4+(pulse j)⁻¹+ρ/4 ≤ ρ ∧
          (∀ t,time j ≤ t → (∀ b,|G.α t-S.β b| ≤ ρ/4) ∧
            |G.drift t-S.p₀| ≤ ρ/4 ∧ S.γ ≤ G.drift t) ∧
          ∀ s : ℕ → Fin n → ℝ,
            (∀ k,j0 ≤ k → ∀ t i,packetStretch (s k) (pulse k) t i ∈ Icc (1/2:ℝ) (3/2)) →
            ∀ b,‖orthogonalMatrix (S.basis b) (slope (G.coefficient slot s j0 b) G.drift (G.l b) (time j))-
              S.θ b • (1:Matrix (ι b) (ι b) ℝ)‖ ≤ ρ/4 := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix, OAI.HarmonicCounterexample.LinearODE.slope

20. lemma OAI.HarmonicCounterexample.LinearODE.PhysicalWord.ideal_factor line 450
21. lemma OAI.HarmonicCounterexample.LinearODE.PhysicalWord.value_factor line 458
22. lemma OAI.HarmonicCounterexample.LinearODE.PhysicalWord.defect_factor line 467
23. theorem OAI.HarmonicCounterexample.LinearODE.word_physical_C1 line 475

    Source documentation

    Packaged uniform estimate with precisely the data that occur in a recursive center-regular geometric construction.

    theorem word_physical_C1 (S : PulseSystem E ι κ) (w : PhysicalWord κ) :
        ∃ T₀ ρ C : ℝ,1 ≤ T₀ ∧ 0 < ρ ∧ 1 ≤ C ∧
          ∀ H : PulseHistory S,T₀ ≤ H.T → H.δ+H.T⁻¹+H.ε ≤ ρ →
          ∀ x ∈ w.ball,
            DifferentiableAt ℝ (w.value S H) x ∧ DifferentiableAt ℝ (w.defect S H) x ∧
            max (max ‖w.value S H x-w.ideal S x‖ ‖fderiv ℝ (w.value S H) x-fderiv ℝ (w.ideal S) x‖)
              (max ‖w.defect S H x‖ ‖fderiv ℝ (w.defect S H) x‖) ≤ C*(H.δ+H.T⁻¹+H.ε) := by
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.PulseSystem, OAI.HarmonicCounterexample.LinearODE.PhysicalWord, OAI.HarmonicCounterexample.LinearODE.PulseHistory

24. theorem OAI.HarmonicCounterexample.LinearODE.local_physical_tuning line 534

    Source documentation

    The uniform local producer: the genuine simultaneous Lie packet admits exact physical whole-period tuning, with all thresholds chosen before histories and BEFORE the bounded complete diagonal-leg normalizers.

    theorem local_physical_tuning (S : PulseSystem E ι κ)
        (htrace : ∀ j b,(S.generator j b).trace=0)
        (hfull : ∀ X : MatrixProduct ι,(∀ b,(X b).trace=0) →
          X ∈ LieSubalgebra.lieSpan ℝ _ (Set.range S.generator))
        (target : ∀ b,Matrix.SpecialLinearGroup (ι b) ℝ)
        {K₀ : ℝ} (hK₀ : 0 ≤ K₀) :
        ∃ (w : PhysicalWord κ) (T₀ ρ : ℝ),1 ≤ T₀ ∧ 0 < ρ ∧
          ∀ H : PulseHistory S,T₀ ≤ H.T → H.δ+H.T⁻¹+H.ε ≤ ρ →
          ∀ K : MatrixProduct ι,‖K‖ ≤ K₀ →
          ∃ x ∈ w.ball,∀ b,∃ c : ℝ,c ∈ Ioo (1/2:ℝ) (3/2) ∧
            wholePeriod K (w.defect S H x) (w.value S H x) b=
              c • ((slProductToUnits target:MatrixProduct ι) b) := by
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.PulseSystem, OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.PhysicalWord, OAI.HarmonicCounterexample.LinearODE.PulseHistory

25. def OAI.HarmonicCounterexample.LinearODE.PhysicalWord.admissible line 585

    Source documentation

    Zero belongs to the admissible control space as a genuinely absent pulse, not as the generally nonzero word at parameter zero.

    def PhysicalWord.admissible : Set (Fin w.n → ℝ) :=
    …

26. lemma OAI.HarmonicCounterexample.LinearODE.PhysicalWord.zero_admissible line 588
27. lemma OAI.HarmonicCounterexample.LinearODE.PhysicalWord.amplitudes_admissible line 590
28. lemma OAI.HarmonicCounterexample.LinearODE.PhysicalWord.admissible_uniform_bound line 593
29. theorem OAI.HarmonicCounterexample.LinearODE.PhysicalWord.admissible_stretch_threshold line 608

    Source documentation

    The same compact parameter ball works in every later pulse, with a threshold independent of histories or later parameter choices.

    theorem PhysicalWord.admissible_stretch_threshold : ∃ J : ℕ,∀ j,J ≤ j →
        ∀ a ∈ w.admissible,∀ t i,packetStretch a (pulse j) t i ∈ Icc (1/2:ℝ) (3/2) := by
    …

    Mentions: OAI.HarmonicCounterexample.a

30. def OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.baseline line 634
31. def OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.packet line 638
32. def OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.defect line 643
33. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.coefficient_causal line 648
34. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.packet_causal line 655
35. def OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.pulseHistory line 700

    Source documentation

    This is a constructor from the actual stream. All nontrivial input facts are supplied by the single history-independent threshold theorem.

    def HistoryGeometry.pulseHistory : PulseHistory S where
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.PulseHistory

36. theorem OAI.HarmonicCounterexample.LinearODE.global_physical_tuning line 756

    Source documentation

    One smooth infinite stream simultaneously tunes every whole-period packet. All thresholds precede EVERY history. The bounded normalizers may be any predetermined actual complete diagonal legs; they do not supply transmissions.

    theorem global_physical_tuning (S : PulseSystem E ι κ) (G : HistoryGeometry S)
        (htrace : ∀ j b,(S.generator j b).trace=0)
        (hfull : ∀ X : MatrixProduct ι,(∀ b,(X b).trace=0) →
          X ∈ LieSubalgebra.lieSpan ℝ _ (Set.range S.generator))
        (target : ∀ b,Matrix.SpecialLinearGroup (ι b) ℝ)
        {K₀ : ℝ} (hK₀ : 0 ≤ K₀) :
        ∃ w : PhysicalWord κ,∃ J : ℕ,∀ j0,J ≤ j0 →
          ∀ K : ℕ → MatrixProduct ι,(∀ j,j0 ≤ j → ‖K j‖ ≤ K₀) →
          ∃ s : ℕ → Fin w.n → ℝ,
            (∀ j,s j ∈ w.admissible) ∧ (∀ j,j<j0 → s j=0) ∧
            (∀ j,j0 ≤ j → ∀ t i,packetStretch (s j) (pulse j) t i ∈ Icc (1/2:ℝ) (3/2)) ∧
            ∀ j,j0 ≤ j → ∀ b,∃ c : ℝ,c ∈ Ioo (1/2:ℝ) (3/2) ∧
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.PulseSystem, OAI.HarmonicCounterexample.LinearODE.HistoryGeometry, OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.PhysicalWord

37. lemma OAI.HarmonicCounterexample.Transmission.blockwise_whole_period_exact_leg line 850

    Source documentation

    Block-dependent Riccati roots are kept in the complete-leg identity.

    lemma blockwise_whole_period_exact_leg
        {U V P B : ∀ b,Matrix (ι b) (ι b) ℝ} (θ : β → ℝ)
        (D M : ∀ b,(Matrix (ι b) (ι b) ℝ)ˣ)
        (hD : ∀ b,(D b:Matrix (ι b) (ι b) ℝ)=U b+θ b • V b)
        (hatt : ∀ b,∃ c : ℝ,c ∈ Ioo (1/2:ℝ) (3/2) ∧
          wholePeriod ((↑(D b)⁻¹:Matrix (ι b) (ι b) ℝ)*V b) (P b-θ b • 1) (B b)=
            c • (M b:Matrix (ι b) (ι b) ℝ)) :
        ∀ b,∃ c : ℝ,c ∈ Ioo (1/2:ℝ) (3/2) ∧
          (U b+V b*P b)*B b=c • ((D b:Matrix (ι b) (ι b) ℝ)*(M b:Matrix (ι b) (ι b) ℝ)) := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.Transmission.wholePeriod

38. lemma OAI.HarmonicCounterexample.Transmission.unnormalize_whole_leg line 873

    Source documentation

    Undo ONLY the harmless scalar pulse normalization. The scalar logarithmic cost is separated from the genuine diagonal factor of the entire leg.

    lemma unnormalize_whole_leg {Fa Fc Fd U V P D M : R} {I c : ℝ}
        (hvalue : Fd=(U+V*P)*Fc)
        (htune : (U+V*P)*(Real.exp (-I) • (Fc*Fa))=c • (D*M)) :
        Fd*Fa=(Real.exp I*c) • (D*M) := by
    …

39. lemma OAI.HarmonicCounterexample.LinearODE.zero_stretch line 910
40. def OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.baseCoefficient line 915

    Source documentation

    Background diagonal coefficient, independent of all control choices.

    def HistoryGeometry.baseCoefficient (j0 : ℕ) (b : ξ) (t : ℝ) : E b →L[ℝ] E b :=
    …

    Mentions: OAI.HarmonicCounterexample.b

41. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.baseCoefficient_eq line 919
42. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.baseCoefficient_diagonal line 933
43. def OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.legLambda line 947

    Source documentation

    The genuine fixed diagonal scalar coefficient.

    def HistoryGeometry.legLambda (d₀ : ∀ b,ι b → ℝ) (j0 : ℕ) (b : ξ) (i : ι b) (t : ℝ) : ℝ :=
    …

    Mentions: OAI.HarmonicCounterexample.b

44. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.legLambda_properties line 952
45. def OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.legU line 987

    Source documentation

    ACTUAL complete-leg columns with the physical schedule.

    def HistoryGeometry.legU (d₀ : ∀ b,ι b → ℝ) (j0 j : ℕ) (b : ξ) : Matrix (ι b) (ι b) ℝ :=
    …

    Mentions: OAI.HarmonicCounterexample.b

46. def OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.legV line 990
47. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.leg_normalizer line 995
48. def OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.transmission line 1029

    Source documentation

    Actual center-regular value transmission, including the complete diagonal leg and with no pulse scalar normalization.

    def HistoryGeometry.transmission (s : ℕ → Fin n → ℝ) (j0 j : ℕ) (b : ξ) : Matrix (ι b) (ι b) ℝ :=
    …

    Mentions: OAI.HarmonicCounterexample.b

49. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.actual_leg_restart line 1035
50. theorem OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.exact_period line 1072

    Source documentation

    Attainment in normalized pulse coordinates gives the actual WHOLE period, with its scalar exactly separated.

    theorem HistoryGeometry.exact_period (d₀ : ∀ b,ι b → ℝ)
        (hd₀ : ∀ b,orthogonalMatrix (S.basis b) (G.D₀ b)=Matrix.diagonal (d₀ b))
        (s : ℕ → Fin n → ℝ) (j0 j : ℕ)
        (hpos : ∀ k,j0 ≤ k → ∀ t i,packetStretch (s k) (pulse k) t i ∈ Icc (1/2:ℝ) (3/2))
        (hj : j0 ≤ j) (b : ξ) (D : (Matrix (ι b) (ι b) ℝ)ˣ)
        (hD : (D:Matrix (ι b) (ι b) ℝ)=G.legU d₀ j0 j b+S.θ b • G.legV d₀ j0 j b)
        (M : Matrix (ι b) (ι b) ℝ) {c : ℝ}
        (htune : wholePeriod ((↑D⁻¹:Matrix (ι b) (ι b) ℝ)*G.legV d₀ j0 j b)
          (G.defect slot s j0 j b) (G.packet slot s j0 j b)=c • M) :
        G.transmission slot s j0 j b=
          (Real.exp (∫ t in time j..time j+pulse j,G.baseline j b t)*c) • ((D:Matrix (ι b) (ι b) ℝ)*M) := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix

51. theorem OAI.HarmonicCounterexample.LinearODE.global_actual_transmission line 1123

    Source documentation

    One actual infinite center-regular equation realizes ALL the requested complete-period transmissions. Its normalizers are the true second-order post-pulse columns U,V, not supplied targets or asymptotic substitutes.

    theorem global_actual_transmission (S : PulseSystem E ι κ) (G : HistoryGeometry S)
        (d₀ : ∀ b,ι b → ℝ)
        (hd₀ : ∀ b,orthogonalMatrix (S.basis b) (G.D₀ b)=Matrix.diagonal (d₀ b))
        (htrace : ∀ j b,(S.generator j b).trace=0)
        (hfull : ∀ X : MatrixProduct ι,(∀ b,(X b).trace=0) →
          X ∈ LieSubalgebra.lieSpan ℝ _ (Set.range S.generator))
        (target : ∀ b,Matrix.SpecialLinearGroup (ι b) ℝ) :
        ∃ w : PhysicalWord κ,∃ J : ℕ,∀ j0,J ≤ j0 →
          ∃ s : ℕ → Fin w.n → ℝ,
            (∀ j,s j ∈ w.admissible) ∧ (∀ j,j<j0 → s j=0) ∧
            (∀ j,j0 ≤ j → ∀ t i,packetStretch (s j) (pulse j) t i ∈ Icc (1/2:ℝ) (3/2)) ∧
            ∀ j,j0 ≤ j → ∀ b,∃ D : (Matrix (ι b) (ι b) ℝ)ˣ,
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.PulseSystem, OAI.HarmonicCounterexample.LinearODE.HistoryGeometry, OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix, OAI.HarmonicCounterexample.LinearODE.PhysicalWord