FiniteRecurrence

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

(e.J.bound.by.indyhyp) in its A.4 finite-corridor form

This module is a Provider helper and makes no source-node status claim.

What is carried here

Items (I-2) and (I-3) of the depgraph record for the node p.combine.corrected, the finite good-event Besov step:

• (I-2) the two substitutions into the proved Step-1 display exists_integral_cutoffResponseJ_le_initialJLBoundDisplay (InitialJLBound.lean): the printed mean gap by the proved Step-2 display coefficientCutoffLaw_sq_abs_annealedSigmaStarInvScalarAtScale_sub_le (CombineIntegerDownscale.lean), and the two variance blocks by the proved unconditional corridor bound exists_coefficientCutoff_finiteCorridor_starInverseVariance_withS_bound' (StarredFluctuationIntegrable.lean);
• (I-3) the resulting finite recurrence, delivered twice: at integer scales (exists_integral_cutoffResponseJ_le_finiteCorridorIndyhypDisplay) and in the A.4 reindexing t = n - L on ℕ (exists_finiteRecurrence_integral_cutoffResponseJ), the second in exactly the input shape of the proved weighted-mean iteration finiteCorridor_weightedDefect_iteration (FiniteCorridorIteration.lean), whose hrec binder it is.

The delivered displays

At delta_1 := 10^9 E^2 gamma the integer-scale public delivers

E[J(cu_m, sigmabar_L^{-1/2} e, sigmabar_L^{1/2} e; a_L)] <= A delta_1 (delta_1 + 3^{-(m-L)}) + C sum_{n=L}^m 3^{-(m-n)} (E[J(cu_n)] - E[J(cu_m)]),

which is the printed e.J.bound.by.indyhyp with the printed bi-infinite defect sum sum_{n=-infty}^m replaced by the printed finite corridor sum_{n=L}^m of e.initial.JL.bound. That replacement is exactly what A.4 prescribes: every scale used lies in [L, m], so the iteration never invokes a mean below the infrared cutoff, for which e.iter.init supplies no estimate.

The ℕ-reindexed public sets F t := E[J(cu_{L+t}, ...)] and delivers

F t <= A delta_1 (delta_1 + 3^{-t}) + C sum_{k=1}^{t} 3^{-k} (F (t-k) - F t), for every t > j_0,

which is the A.4 display verbatim. Both A and C and the separation j_0 are selected before the model, the cutoff L and the unit direction e, as A.4 requires.

Shape match against A.4, with every constant disclosed

Write C_1, C_bad for the two constants of the proved Step-1 display, C_var for the constant of the proved corridor variance bound (all three existential, all at least 1), and sigmabar_L for the running coarse-grained diffusivity.

1. The defect coefficient is C := C_1, the Step-1 display's own constant. The gate binder C 3^{-(3/4)(m-L)} <= 1/4 is therefore byte-identical to the proved one.
2. The forcing amplitude is A := 3 C_1 C_var + 7 C_1 + C_bad, assembled as:
   • 3 C_1 C_var from the two variance blocks. The proved corridor bound gives sigmabar_L^2 var[sigma_{L,*}^{-1}(cu_n)] + var[sigma_{L,*}^{-1}kappa_L(cu_n)] <= 2 C_var delta (delta + 3^{-d(n-L)}) at every corridor scale n, where delta is the lane's two-term amplitude (see 4 below). Summing against the printed weight 3^{-(m-n)} uses the two corridor sums sum_{n=L}^m 3^{-(m-n)} <= 3/2 and sum_{n=L}^m 3^{-(m-n)} 3^{-d(n-L)} <= (3/2) 3^{-(m-L)}. The second needs 2 <= d; that is M.shellPrefix.dimension, a field of the standing model, not an added hypothesis. The product of the two 3/2s with the 2 of the proved bound is the 3.
   • 6 C_1 from the mean gap. The proved Step-2 display gives |sigmabar_{L,*}^{-1}(cu_m) - sigmabar_{L,*}^{-1}(cu_n)|^2 <= 4 sigmabar_L^{-2} delta_1^2, so the display's sigmabar_L^2 weighting cancels the sigmabar_L^{-2} and leaves 4 delta_1^2 at every corridor scale; the corridor weight then contributes the 3/2, giving 6 delta_1^2.
   • C_1 + C_bad from the collapse of the Step-1 display's two amplitude terms C_1 delta_1^2 + C_bad (10^9 E^2 gamma)^2. Per A.3 and A.4, which both set delta_1 := 10^9 E^2 gamma, the delivered statements are instantiated at that value, so the two terms are terms in one amplitude. This is the adjudication recorded (I-1).
   • finally delta_1^2 <= delta_1 (delta_1 + 3^{-(m-L)}) absorbs the three pure-square blocks into the A.4 forcing shape.
3. The rate. The lag weights are the printed 3^{-k} and the forcing decay is the printed 3^{-t}; both are the single parameter r = 1/3 of the proved iteration engine, which is the only admissible value there (its hr3 caps r at 1/3, and the printed lag weights force r >= 1/3).
4. The two-term amplitude, absorbed. The proved corridor variance bound carries the lane's delta = E^2 gamma + exp(-2 E^{-3} gamma^{-1}), strictly larger than the printed delta_1-scale amplitude; this is the caveat recorded on that display (B). It is absorbed here, unconditionally under the proposition's own regime gamma <= E^{-10} and 1 <= E, by twoTermAmplitude_le_amplitude below: exp(-2 E^{-3} gamma^{-1}) <= E^2 gamma, hence delta <= 2 E^2 gamma, hence delta <= 2 * 10^{-9} delta_1 <= delta_1. The elementary input is exp(-x) <= 4/x^2 for x > 0.
5. The delivered Chom is their maximum. Both places it is consumed are monotone in the right direction: the gate gamma <= Chom^{-1} E^{-2} epsilon is stronger for a larger Chom, and so is the corridor separation L <= m - Chom |log epsilon| since |log epsilon| >= 0. Nothing is weakened by the composition.

Source premises, standing data, typing data, and no conditional input

Every caller-supplied mathematical proposition of the two publics is a threaded premise of one of the three proved displays. There is no conditional A input: the module's conditional-A count is zero.

• hEfloor, hregime --- the A.3 induction regime, verbatim from the Step-1 display;
• hLower --- the frozen preceding-error clause, verbatim from the Step-1 display and from the corridor variance bound (the two carry byte-identical binders);
• hepsilon, hgate --- the printed smallness window and gate, at the composed Chom (see 5 above);
• hsep (L <= m - 2) --- inherited verbatim from the Step-1 display, whose own disclosure pins the single excluded cutoff L = m - 1 to (v);
• hsepvar (L <= m - Chom |log epsilon|) --- the corridor-separation premise of the proved corridor variance bound. In the ℕ-reindexed public this reads Chom |log epsilon| <= t, i.e. the recurrence is delivered above an epsilon-dependent depth. A.4 asks for a dimension-only j_0(d); the delivered j_0 is dimension-only, but the separation binder rides alongside it. This is a threaded premise of a proved display, not an addition, and it is the consumer's to discharge together with A.4's choice of k_1;
• hgateC --- the printed gate C 3^{-(1-s)(m-L)} <= 1/4 at the s = 1/4 endpoint, verbatim from the Step-1 display. In the ℕ-reindexed public it is discharged internally from j_0 < t;
• he --- e.pq.normed in the Step-1 display's form |e| = 1.

The amplitude-bridge conclusion (A.3's X_R step) --- the shape 10^9 E^2 gamma in Ioc 0 (1/2) together with the diagonal fourth-moment bound at every cutoff <= m - 1 --- is not a binder of either public. Its producer, item (I-1), is the proved AmplitudeBridge.lean's amplitude_mem_Ioc_and_lintegral_pow_four_le; that module is imported above and the conclusion is consumed, by the bare application amplitude_mem_Ioc_and_lintegral_pow_four_le M hChom10 hEfloor hregime hLower hepsilon hgate hs, every premise of which is either a binder of the publics below or the internal 10^9 <= Chom and hs. The regularity index hs: 0 < 1/4, which selects the exponent s = 1/4, is likewise not a binder: it is proof-irrelevant typing data and is produced internally by norm_num. Nothing beyond the bullets above is caller-supplied.

Standing data: M : ABKModel d (whence 2 <= d and 0 < gamma). Typing data: d, [NeZero d], m, L, t, e, E, epsilon.

The horizon and the epsilon-dependent depth, adjudicated

The recurrence is delivered at one observation scale at a time, with the preceding-error clause taken at that observation scale, exactly as the proved Step-1 display requires and exactly as A.3 prescribes ("fix M, assume S(M-1,E)"). Two consequences, both adjudicated and both costless:

1. The horizon. The proved iteration engine's hrec binder ranges over all t : ℕ, while a consumer holding the clause at one top scale m gets the recurrence only for L + t <= m. This costs nothing: the zero-truncation G t := if t <= T then F t else 0 satisfies all three engine binders, since beyond T the recurrence degenerates to 0 <= nonneg. Every downstream consumption (; the cutoff-union completion) lies inside that horizon.
2. The epsilon-dependent depth carried by hsepvar/hsept is absorbed consumer-side, by a shift performed with the sharp geometric prefix sum_{k > j} r^k <= (3/2) r^{j+1} and the engine applied at j_0 = 0, with A' := A + (3/2) r; then K = finiteCorridorAmplitude A' r 0 = 2 (A' + 2 K_0) is dimension-only, and the budget k_1 <= C(d) |log epsilon| survives. Do NOT instead pass j_0' := max j_0 ceil(Chom |log epsilon|) to the engine. finiteCorridorAmplitude A r j_0 = 2 (A + 2 K_0 + j_0 r) is linear in j_0, so that route makes K ~ |log epsilon| and hence demands gamma <~ epsilon / (|log epsilon| E^2), contradicting A.4's manuscript smallness condition gamma <= C(d)^{-1} E^{-2} epsilon.

The engine's other two binders, hFnonneg and the crude initialization hcrude (e.iter.init), are separate producers and are not supplied here.

References

• ABK26, Section 3.5: p.combine.under.S, its Step 5, and the proof of p.homogenization.step.

The corridor geometric quintet, factored through one reindex

The two-term amplitude absorption

The two assembly steps, as abstract real arithmetic

(e.J.bound.by.indyhyp) at integer scales

theorem Algsuperdiff.Section3.Provider.Homogenization.exists_integral_cutoffResponseJ_le_finiteCorridorIndyhypDisplay (d : ℕ) [NeZero d] : ∃ (Chom : ℝ) (A : ℝ) (C : ℝ), 10 ^ 9 ≤ Chom ∧ 64 ≤ Chom ∧ 0 ≤ A ∧ 1 ≤ C ∧ ∀ (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 ≤ Chom⁻¹ * (↑E)⁻¹ ^ 2 * epsilon → ∀ L ≤ m - 2, ↑L ≤ ↑m - Chom * |Real.log epsilon| → C * 3 ^ (-(3 / 4) * ↑(m - L)) ≤ 1 / 4 → ∀ (e : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e = 1 → ∫ (omega : Cutoff.CutoffSample d), Observable.cutoffResponseJ M m L e omega ∂↑(Cutoff.cutoffSampleLaw M) ≤ A * (10 ^ 9 * ↑E ^ 2 * M.gamma) * (10 ^ 9 * ↑E ^ 2 * M.gamma + 3 ^ (-↑(m - L))) + C * ∑ n ∈ Finset.Icc L m, 3 ^ (-↑(m - n)) * (∫ (omega : Cutoff.CutoffSample d), Observable.cutoffResponseJ M n L e omega ∂↑(Cutoff.cutoffSampleLaw M) - ∫ (omega : Cutoff.CutoffSample d), Observable.cutoffResponseJ M m L e omega ∂↑(Cutoff.cutoffSampleLaw M))

At delta_1 := 10^9 E^2 gamma the delivered display is

E[J(cu_m, sigmabar_L^{-1/2} e, sigmabar_L^{1/2} e; a_L)] <= A delta_1 (delta_1 + 3^{-(m-L)}) + C sum_{n=L}^m 3^{-(m-n)} (E[J(cu_n)] - E[J(cu_m)]),

i.e. the printed display with its bi-infinite defect sum replaced by the finite corridor of e.initial.JL.bound. A and C are selected before the model, the cutoff and the direction. Every constant is disclosed in the module docstring; there is no conditional A input, the amplitude bridge being imported and consumed rather than assumed.

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

(e.J.bound.by.indyhyp) in the A.4 reindexing t = n - L

theorem Algsuperdiff.Section3.Provider.Homogenization.exists_finiteRecurrence_integral_cutoffResponseJ (d : ℕ) [NeZero d] : ∃ (Chom : ℝ) (A : ℝ) (C : ℝ) (j₀ : ℕ), 10 ^ 9 ≤ Chom ∧ 64 ≤ Chom ∧ 0 ≤ A ∧ 0 ≤ C ∧ ∀ (M : ABKModel d) (E : { E : ℝ // 1 ≤ E }), 15 * (Disorder.cstar M)⁻¹ ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → ∀ epsilon ∈ Set.Ioc 0 (1 / 2), M.gamma ≤ Chom⁻¹ * (↑E)⁻¹ ^ 2 * epsilon → ∀ (L : ℤ) (e : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e = 1 → ∀ (t : ℕ), j₀ < t → Chom * |Real.log epsilon| ≤ ↑t → (∀ k ≤ L + ↑t - 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⁻¹)))) → ∫ (omega : Cutoff.CutoffSample d), Observable.cutoffResponseJ M (L + ↑t) L e omega ∂↑(Cutoff.cutoffSampleLaw M) ≤ A * (10 ^ 9 * ↑E ^ 2 * M.gamma) * (10 ^ 9 * ↑E ^ 2 * M.gamma + (1 / 3) ^ t) + C * ∑ k ∈ Finset.Icc 1 t, (1 / 3) ^ k * (∫ (omega : Cutoff.CutoffSample d), Observable.cutoffResponseJ M (L + ↑(t - k)) L e omega ∂↑(Cutoff.cutoffSampleLaw M) - ∫ (omega : Cutoff.CutoffSample d), Observable.cutoffResponseJ M (L + ↑t) L e omega ∂↑(Cutoff.cutoffSampleLaw M))

With F t := E[J(cu_{L+t}, sigmabar_L^{-1/2} e, sigmabar_L^{1/2} e; a_L)] and delta_1 := 10^9 E^2 gamma,

F t <= A delta_1 (delta_1 + 3^{-t}) + C sum_{k=1}^{t} 3^{-k} (F (t-k) - F t)

for every t > j_0, with A, C and the dimension-only separation j_0 selected before the model, the cutoff L and the unit direction e. Every predecessor t - k lies in [0, t], so no scale below the infrared cutoff is used: that is exactly what A.4 prescribes.

This is the input shape of exists_finiteCorridor_weightedDefect_decay at r = 1/3. The engine's hFnonneg and hcrude binders are separate producers and are not supplied here; so is the clause at every observation scale, which the hLower binder below is taken at, and which bounds the reach of the delivered recurrence by the induction state's top scale. The module docstring adjudicates both that horizon and the epsilon-dependent depth: the first is free by zero-truncation, the second is absorbed by a consumer-side shift with the engine applied at j_0 = 0 --- and not by enlarging the engine's own j_0.

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