Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Homogenization.IterateAssembly

IterateAssembly #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The finite-corridor iterate mean bound (e.iter.post.new) #

The single public below is exactly the proposition that the proved terminal theorem

exists_isCommonEventTwoTermBigOWith_cutoffResponseJ_of_iterateMeanBound (Provider/Homogenization/UnionCompletion.lean)

takes as its one conditional A obligation hIter. The statement below is a byte-level transcription of that binder type, so the terminal theorem is discharged by the bare application

exists_isCommonEventTwoTermBigOWith_cutoffResponseJ_of_iterateMeanBound _
  (exists_iterateMeanBound_integral_cutoffResponseJ _)

with no glue at all. This module is a Provider helper and makes no source-node status claim by itself.

What is assembled here, and from what #

Three proved publics are consumed and nothing they prove is re-proved.

  1. exists_finiteRecurrence_integral_cutoffResponseJ (FiniteRecurrence.lean) supplies the A.4 recurrence constants (Chom_R, A, C, j_0) and, at every corridor depth t with j_0 < t and Chom_R |log epsilon| <= t, the display F t <= A d_1 (d_1 + 3^{-t}) + C sum_{k=1}^t 3^{-k} (F(t-k) - F t) for F t := E[J(cu_{L+t}, sigmabar_L^{-1/2} e, sigmabar_L^{1/2} e; a_L)] and d_1 := 10^9 E^2 gamma. Its clause binder is carried at the observation scale L + t, so the proposition's own clause at m - 1 supplies it exactly when L + t <= m.
  2. integral_cutoffResponseJ_nonneg_and_le_amplitude (IterateInit.lean) supplies the engine's other two slots, hFnonneg and hcrude at K_0 = 1, with no horizon: 0 <= F t and F t <= d_1 for every t : ℕ.
  3. finiteCorridor_weightedDefect_iteration (FiniteCorridorIteration.lean) is the weighted-mean engine. The existential wrapper exists_finiteCorridor_weightedDefect_decay (ibid.:475) is not used: its K and rho are opaque witnesses, and the constant Citer produced below has to be built from them explicitly. The fixed-constant public gives finiteCorridorAmplitude A' (1/3) 0 and rho = finiteCorridorDecayRate C by name; the amplitude actually delivered by exists_shift_engine is K = max (finiteCorridorAmplitude A' (1/3) 0) 1, the max being what supplies the 1 <= K that the final arithmetic needs (disclosed again at the exists_shift_engine entry below). That is what makes Citer nameable before the model, the tolerance, the cutoff and the direction.

The construction, and the two audit adjudications it implements #

That is exactly what truncated_shift_decay below does: with T:= (m - L).toNat it forms G t:= if t <= T then F t else 0, feeds G the unbounded nonnegativity and crude bound of both branches, and establishes only the recurrence by cases --- for t <= T it is the proved recurrence verbatim (the clause binder at `L

The certified replacement, followed here, is a consumer-side shift with the sharp geometric prefix sum_{k > j} r^k <= (3/2) r^{j+1} at r = 1/3, absorbed into A' := A + (3/2) r = A + C/2 (geom_third_Icc_shift_le, shifted_third_recurrence), after which the engine is run at j_0 = 0, where finiteCorridorAmplitude A' (1/3) 0 = 2 (A' + 2) is dimension-only and the delivered amplitude is K = max (finiteCorridorAmplitude A' (1/3) 0) 1. The engine's own shift (its private earlyPrefix_sum_le, which pays a cardinality factor j_0) is not bypassed: it is still invoked inside the engine (FiniteCorridorIteration.lean), at j_0 = 0, where its cardinality factor is 0, so it is paid at zero cost. The proved engine is not modified in any way.

The two separations. With u := |log epsilon|,

t_0    := max (j_0 + 1) ceil(Chom_R u)        (the recurrence's own two binders)
j*     := ceil((log(4 * 10^9 * K) + u) * lam^{-1}),   lam := -log rho > 0
k_1    := t_0 + j*  .

j* is the least depth with rho^{j*} (4 * 10^9 K) <= epsilon; it is obtained by taking logarithms (Real.log_pow, Real.exp_log) rather than through rpow. The budget k_1 <= Citer u is shift_budget_le, whose only analytic input is 1 <= 2 u, i.e. |log epsilon| >= log 2 > 1/2, which is where epsilon <= 1/2 is used.

The constant.

Citer := max 1 (max Chom_R (max (4 K 10^18)
           (2 (j_0 + 3) + Chom_R + (2 log(4 * 10^9 K) + 1) lam^{-1}))) .

All four branches are dimension-only: they are built from (Chom_R, A, C, j_0) and from K, rho, all selected before M, E, epsilon, L, n, e. The gate gamma <= Citer^{-1} E^{-2} epsilon implies the consumed gate gamma <= Chom_R^{-1} E^{-2} epsilon because Citer >= Chom_R (monotone in the right direction), and that one gate feeds both the recurrence and the initialization, the latter at Chom := Chom_R >= 10^9, which is the floor the amplitude bridge's gate route requires.

The final arithmetic. At any n with L + k_1 <= n <= m, writing t := (n - L).toNat in [k_1, T] and j := t - t_0 >= j*,

F t <= K d_1 (d_1 + rho^j) <= K d_1 (d_1 + rho^{j*})
    <= (1/4) epsilon E^2 gamma + (1/4) epsilon E^2 gamma
     = 2^{-1} epsilon E^2 gamma ,

the first quarter from K d_1^2 <= (1/4) epsilon E^2 gamma, which needs only Citer >= 4 K 10^18, and the second from the defining property of j* (final_absorption).

d = 0 #

The transcribed proposition quantifies over an arbitrary d : ℕ, exactly as the terminal theorem and the frozen statement do, while both proved inputs carry [NeZero d]. The degenerate case is discharged from the standing model itself: M.shellPrefix.dimension : 2 <= d is contradictory at d = 0, so the whole inner forall is vacuous there and the witness Citer := 1 serves. For 0 < d the instance NeZero d is produced and the construction above runs. No [NeZero d] binder is added to the statement, which is what makes the bare application to the terminal theorem type-check.

References #

Pure real arithmetic #

Every step of the assembly that is not an instantiation of a proved public is isolated here as a statement about abstract reals and abstract sequences: no model, no measure, no observable occurs below until the final theorem.

The iterate mean bound #

source
theorem Algsuperdiff.Section3.Provider.Homogenization.exists_iterateMeanBound_integral_cutoffResponseJ (d : ℕ) :
∃ (Citer : ℝ), 1 ≤ Citer ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), 15 * (Disorder.cstar M)⁻¹ ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → (∀ k ≤ m - 1, ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1), Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Observable.cutoffHomogenizationError M k ⟨s, ⋯⟩) (↑E * s⁻¹ * √M.gamma) (s⁻¹ ^ 2 * Real.exp (-((↑E)⁻¹ ^ 3 * M.gamma⁻¹)))) → ∀ epsilon ∈ Set.Ioc 0 (1 / 2), M.gamma ≤ Citer⁻¹ * (↑E)⁻¹ ^ 2 * epsilon → ∃ (k1 : ℕ), ↑k1 ≤ Citer * |Real.log epsilon| ∧ ∀ (n L : ℤ), L ≤ m - 1 → L + ↑k1 ≤ n → n ≤ m → ∀ (e : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e = 1 → ∫ (omega : Cutoff.CutoffSample d), Observable.cutoffResponseJ M n L e omega ∂↑(Cutoff.cutoffSampleLaw M) ≤ 2⁻¹ * epsilon * ↑E ^ 2 * M.gamma

One dimension-only constant Citer ≥ 1 is selected before the model, the scale, the tolerance, the cutoff and the direction. Under the frozen regime binders 15 c_star^{-1} ≤ E and gamma ≤ E^{-10}, the preceding-error clause at every scale k ≤ m - 1, the printed tolerance range epsilon ∈ (0, 1/2] and the smallness gate gamma ≤ Citer^{-1} E^{-2} epsilon, a single separation k₁ of logarithmic size k₁ ≤ Citer |log epsilon| is fixed --- before any cutoff L and any unit direction e --- such that

E[J(cu_n, sigmabar_L^{-1/2} e, sigmabar_L^{1/2} e; a_L)] ≤ (1/2) epsilon E^2 gamma

at every cutoff L ≤ m - 1, every unit direction and every observation scale L + k₁ ≤ n ≤ m.

This proposition is byte-identical to the hIter binder of the proved exists_isCommonEventTwoTermBigOWith_cutoffResponseJ_of_iterateMeanBound (UnionCompletion.lean, its), which it discharges by bare application.

This is a local Provider theorem and makes no source-node status claim.