Manuscript-facing theorem for bundle v5

This module packages the explicit continuous-coordinate online process, its exact finite count marginals, the two natural-log cost bounds in the main theorem, the balanced-initial-law corollary, and the abstract resource guarantees.

noncomputable def FD1D.V5.universalConstant : ℝ

One universal constant sufficient for both parts of the main theorem.

Equations

• FD1D.V5.universalConstant = 72000 / Real.log 2

theorem FD1D.V5.universalConstant_pos : 0 < universalConstant

theorem FD1D.V5.limsup_trajectoryRMSCostFromState_le_log_succ {m : ℕ} (hm : 2 ≤ m) (s0 : SpatialState m) : Filter.limsup (ContinuousProcess.trajectoryRMSCostFromState m ⋯ s0) Filter.atTop ≤ universalConstant * Real.log ↑(m + 1) / ↑m

Natural-log form of manuscript part (i), from any fixed initial inventory.

theorem FD1D.V5.finite_horizon_expected_joinedTrajectoryCost_le_log_succ {m N : ℕ} (hm : 2 ≤ m) (hN : 2 * m ^ 2 ≤ N) (initial : RefreshSupply (treeDepth m) m) (demand : Fin m → ℝ) (hdemand : ∀ (j : Fin m), demand j ∈ Set.Icc 0 1) : ∫ (path : ℕ → ContinuousProcess.ProcessState m), ContinuousProcess.joinedTrajectoryAverageCost initial demand ↑(parameterA m) ⋯ N path ∂ContinuousProcess.trajectoryLaw (↑(parameterA m)) (SupplyConfiguration.canonicalFallback ⋯) ≤ universalConstant * Real.log ↑(m + 1) / ↑m

Natural-log form of manuscript part (ii). The scheduled replacement phase is joined pathwise to the same post-refresh trajectory.

structure FD1D.V5.FullFormalization (m : ℕ) (hm : 2 ≤ m) : Prop

All formal conclusions used by the v5 main theorem and balanced corollary. The countMarginal field identifies the explicit continuous process with the finite V5 count kernel at every time.

• countMarginal (s0 : SpatialState m) (t : ℕ) : MeasureTheory.Measure.map (fun (path : ℕ → ContinuousProcess.ProcessState m) => spatialCount (treeDepth m) (path t).1) (ContinuousProcess.trajectoryLawFromState s0 (↑(parameterA m)) (SupplyConfiguration.canonicalFallback ⋯)) = ((parameterizedKernel m ⋯).iterate t (FiniteLaw.dirac (spatialCount (treeDepth m) s0))).toMeasure
• arbitraryInitialRMS (s0 : SpatialState m) : Filter.limsup (ContinuousProcess.trajectoryRMSCostFromState m ⋯ s0) Filter.atTop ≤ universalConstant * Real.log ↑(m + 1) / ↑m
• initializedFiniteHorizon (N : ℕ) : 2 * m ^ 2 ≤ N → ∀ (initial : RefreshSupply (treeDepth m) m) (demand : Fin m → ℝ), (∀ (j : Fin m), demand j ∈ Set.Icc 0 1) → ∫ (path : ℕ → ContinuousProcess.ProcessState m), ContinuousProcess.joinedTrajectoryAverageCost initial demand ↑(parameterA m) ⋯ N path ∂ContinuousProcess.trajectoryLaw (↑(parameterA m)) (SupplyConfiguration.canonicalFallback ⋯) ≤ universalConstant * Real.log ↑(m + 1) / ↑m
• balancedEveryHorizon (T : ℕ) : 0 < T → √((∑ t ∈ Finset.range T, ((parameterizedKernel m ⋯).iterate t (Balanced.parameterizedLaw m)).expect (parameterizedSquaredCostEnvelope m)) / ↑T) ≤ (2 + √(501 / 12)) * ↑(parameterA m) / ↑m
• resources : HierarchicalResourceGuarantees

theorem FD1D.V5.full_formalization {m : ℕ} (hm : 2 ≤ m) : FullFormalization m hm

The explicit V5 online policy satisfies the complete packaged theorem.