PrincipalResponseTerminal

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

The principal-response comparison and its gates

The two halves of the Step-3 switch display are stated at different admissibility gates on the induction parameter E: the bad-event package asks for c⁻¹ (cstar M)⁻¹ ≤ E, the coarse-ellipticity envelope for max (exp (2 C)) (cstar M)⁻¹ ≤ E, and both for a fifth-root upper gate. The source premises available at this level are the two premises of l.approximate.recurrence.formula itself: a constant fixed before the model times (cstar M)⁻¹ below E, and gamma ≤ E⁻⁵. They are not contained in Algsuperdiff.Frozen.Section3.inductionState, which binds only 1 ≤ E, and they are not carried by the frozen induction command; at the frozen root the corresponding scale premise is the stronger gamma ≤ (E⁻¹)^10, from which the gamma ≤ E⁻⁵ read here is obtained in the root assembly.

This module supplies the arithmetic that turns those two source premises into every gate the two halves ask for, so that none of them has to be carried as a hypothesis by the comparison itself.

The admissibility reductions

• le_rpow_neg_fifth_of_gamma_le_zpow_neg_five' --- the integer-power gate gamma ≤ E⁻⁵ gives the real-power gate E ≤ gamma^(-1/5) that both packages consume.
• admissibility_of_enlarged_const_mul_cstarInv_le --- one enlarged constant, chosen after the two packages have fixed their own constants and depending only on them, dominates all the lower gates at once. The step that makes this work is the repository's own upper bound cstar M ≤ 3 / 2 (Provider.Disorder.cstar_le_three_halves), which gives (cstar M)⁻¹ ≥ 2 / 3 and so lets a 3 / 2 factor inside the enlarged constant pay for the (cstar M)⁻¹ that multiplies it. No lower bound on cstar M is assumed; none is available.

The scale gaps at the recurrence mesoscale

The two-sided exponent (n - Q.scale)_+ - 5 (Q.scale - n)_+ of the oscillation rate is read at the Step-3 orientation: the cube scale is the corrected buffer n := m - h - a ceil|log_3 gamma| and the field index is m - h. scaleGapPos_recurrenceMesoScale_to_field and scaleGapPos_field_to_recurrenceMesoScale evaluate the two positive parts there: the -5 branch vanishes and the surviving branch is the corrected gap itself.

The two rate gates

Both tails of the bad-event package have to clear gamma⁻¹ + log 2 before the two-lane fold can collapse them. The mechanism is the standard one: the constants are fixed once, before gamma, and the whole gain is read off the two source premises.

• add_log_two_le_mul_rpow_three_recurrenceGap --- the oscillation lane. With 2 / c ≤ Cterm, the premise Cterm (cstar M)⁻¹ ≤ E gives 2 ≤ c cstar E, and gamma ≤ E⁻⁵ gives E ≤ gamma⁻¹, so the prefactor reaches 2 ≤ c cstar gamma⁻¹. That alone is not the gate: the missing factor gamma⁻¹ is supplied by the gap factor, through 3^(a ceil|log_3 gamma|) ≥ gamma⁻¹. Both steps are load-bearing.
• add_log_two_le_exp_ellipticityRate --- the ellipticity lane, a genuine exp-beats-power step. The exponent x := c E⁻² gamma⁻¹ has x^2 / 4 = c^2 gamma⁻¹ gamma⁻¹ / (4 E^4); with 12 / c^2 ≤ Cterm and cstar M ≤ 3 / 2 the same premise gives 8 / c^2 ≤ E, which together with E^5 ≤ gamma⁻¹ puts x^2 / 4 above 2 gamma⁻¹, and sq_div_four_le_exp carries that to exp x.

The two gates of the recombination

The assembly step that turns the two legs into the comparison itself asks for a window gate and a rename gate. Both are discharged here, over abstract reals:

• inv_abs_log_mem_Icc --- the window |log gamma|⁻¹ ∈ [8 gamma, 1], on gamma ≤ 1 / 1089.
• This is what lets the comparison be displayed at the manuscript's own shape C E^2 |log cgamma|^2 cgamma with C absolute, rather than at a cgamma-dependent factor.
• Its only real content is a threshold on gamma by an absolute constant.

All of the analytic statements are over abstract reals, away from any model or envelope, so that no definitional depth reaches the unifier.

The comparison itself

exists_const_descendantsAverage_integral_principalEnergy_le_annealedLimit puts the two halves of the Step-3 switch display together at one and the same witness and hands back the combined comparison of e.lower.bound.principal.one: one pair of correctors produced existentially with their e.def.w properties, one coarse-ellipticity constant, one per-cube bad-event family, and a single inequality between the grid average of the localized principal energy and the infinite-volume annealed form at the factor 1 + 3 principalResponseSwitchBudget M E 64 plus cgamma^6. Its two surviving analytic premises are the two source premises above; every gate listed in this header --- including the threshold on cgamma that the four sub-packages ask for, which is not a binder but a consequence of the enlarged Cterm --- and every measurability, integrability and MemLp proposition the two halves ask for, is discharged inside its proof.

References

• ABK26, l.approximate.recurrence.formula, Step 3.

The fifth-root upper gate

The lower admissibility gates, from one enlarged constant

The two scale gaps at the recurrence mesoscale

The two rate gates

The bad-event leg inside the half budget

The two gates of the recombination

The plumbing of the limit-side quadratic form

The principal-response comparison

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.exists_const_descendantsAverage_integral_principalEnergy_le_annealedLimit (d : ℕ) (hd : 2 ≤ d) : ∃ (Cterm : ℝ), 0 < Cterm ∧ ∀ (M : ABKModel d) (m Kc : ℤ) (hgap : ℕ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m - 1) E → 0 < hgap → Cterm * (Disorder.cstar M)⁻¹ ≤ ↑E → M.gamma ≤ ↑E ^ (-5) → ↑hgap ≤ 6 * Disorder.cstar M * M.gamma⁻¹ → 10 ^ 10 * M.gamma⁻¹ ≤ ↑Kc - ↑m → ∀ (e e' : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e ≤ 1 → HCPolySupport.Book.Ch02.vecNorm e' ≤ 1 → ∀ (j : ℕ), (HCPolySupport.originCube d Kc).scale - ↑j = recurrenceMesoScale recurrenceGapMultiplier M.gamma m ↑hgap → ∃ (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))), (∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc)) (wD omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑(Annealed.sigmaBar M (m - ↑hgap)))⁻¹ omega (m - ↑hgap) m e x) ∧ (∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc)) (wN omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑(Annealed.sigmaBar M (m - ↑hgap)))⁻¹ omega (m - ↑hgap) m e' x) ∧ (HCPolySupport.descendantsAverage (HCPolySupport.originCube d Kc) j fun (R : HCPolySupport.TriadicCube d) => ∫ (omega : Cutoff.CutoffSample d), switchCubeEnergy M m R (principalPz (Annealed.sigmaBar M (m - ↑hgap)) (↑omega) (m - ↑hgap) m e e' R (wD ↑omega) (wN ↑omega)) omega ∂↑(Cutoff.cutoffSampleLaw M)) ≤ ((1 + 3 * principalResponseSwitchBudget M E 64) * HCPolySupport.descendantsAverage (HCPolySupport.originCube d Kc) j fun (R : HCPolySupport.TriadicCube d) => ∫ (omega : Cutoff.CutoffSample d), HCPolySupport.blockVecDot (gaugedPrincipalLoadShell (Annealed.sigmaBar M (m - ↑hgap)) R (m - ↑hgap) m e e' wD wN ↑omega) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockDiag (↑(Annealed.sigmaBar M (m - ↑hgap)) • 1) ((↑(Annealed.sigmaBar M (m - ↑hgap)))⁻¹ • 1)) (gaugedPrincipalLoadShell (Annealed.sigmaBar M (m - ↑hgap)) R (m - ↑hgap) m e e' wD wN ↑omega)) ∂↑(Cutoff.cutoffSampleLaw M)) + M.gamma ^ 6

The principal-response comparison of l.approximate.recurrence.formula, Step 3, at one and the same witness.

For a single constant Cterm fixed before the model --- the manuscript's own C(d) --- every model, every induction state S(m - 1, E), and every scale datum of e.recurrence.params carry one pair of solutions wD, wN of the two problems e.def.w (label), produced existentially together with those properties, for which the grid average of the localized principal energy obeys

  avsum_R E[ P_R . bfA_m(R) P_R ]
    <= (1 + 3 principalResponseSwitchBudget M E 64)
         avsum_R E[ W_R . bfAhom_{m-h} W_R ]
       + cgamma^6 ,

where principalResponseSwitchBudget M E 64 = C 3^128 E^2 (log cgamma)^2 cgamma carries an absolute constant; no factor of the conclusion depends on cgamma except through the printed |log cgamma|^2 cgamma. There is no separate smallness binder on cgamma: every threshold the proof needs is forced by Cterm (cstar M)^{-1} <= E, cstar M <= 3/2 and cgamma <= E^{-5}, which is exactly the manuscript's "increasing M in e.cgamma.constraints if necessary".

with W_R = G_{-(h)_R} P_R the gauged load and principalResponseSwitchBudget the named form of the printed factor C E^2 |log cgamma|^2 cgamma. This is the target display e.lower.bound.principal.one (label) at the localization data of this repository -- one combined comparison, not a pair of good/bad estimates and not a raw two-exponential tail.

The two surviving analytic premises

They are the two premises of l.approximate.recurrence.formula itself: one constant fixed before the model times (cstar M)^{-1} below E, and cgamma <= E^{-5}. Neither is contained in Algsuperdiff.Frozen.Section3.inductionState, which binds only 1 <= E, and neither is carried by the frozen induction command; at the frozen root the corresponding scale premise is the stronger cgamma <= (E^{-1})^{10}, from which the cgamma <= E^{-5} read here is obtained in the root assembly.

Everything else the two halves and the recombination ask for -- the two admissibility gates, the fifth-root gate, the window, the two rate gates, the tail domination, the moment envelope's smallness gate, the four sub-packages' own cgamma-thresholds, the rename gate, and every measurability, integrability and MemLp proposition -- is discharged inside the proof. None of them survives as a binder. In particular the terminal carries no hsmall, no hEexp/hEadm/hEgamma, no hwindow, no rate gate and no cgamma <= gamma0. What remains besides the two premises is standing or source-scale data: the induction state at m - 1, 0 < h, the buffer bound h <= 6 cstar cgamma^{-1}, the large-cube gate 10^10 cgamma^{-1} <= K - m, the two directions, the localization depth j and its mesoscale identity.

The parameters

• No multiplier binder and no range binder occurs; the printed buffer 16 of e.recurrence.params is not used.
• The good-event half is read at the honest switch factor 1 + (3/2) Delta; the extra half of Delta is paid inside the cgamma^6 budget at the corrected gap a = 32, not absorbed into the printed factor.
• The bad-event half is folded to the single tail exp(-cgamma^{-1}) and finished below cgamma^6 / 2 internally, at the tail power 3/8.
• The coarse-ellipticity gate of the good half is met at Ccg = 2 Cbase from the dimension floor (d : ℝ)^6 <= Cbase carried by the bad-event package and Provider.BadEvents.one_le_sensitivityConstMax. No event monotonicity is used or assumed.
• The window |log cgamma|^{-1} in [8 cgamma, 1] needs cgamma <= 1 / 1089. The standing cgamma <= 1 / 4 is insufficient for its lower end: at cgamma = 1 / 4, 8 cgamma |log cgamma| = 2 log 4 = 2.77... > 1. The bound is obtained here from the source premises, by enlarging Cterm past (3/2). 1089: then 1089 <= E <= cgamma^{-1}. The same mechanism supplies the four sub-packages' own thresholds, so no cgamma <= gamma0 binder occurs.
• The reading gauge shom_{m-1} of the fourth-moment display and the load gauge shom_{m-h} of e.Pz.def are bridged inside the proof by the public transports of PrincipalResponseMomentsFourth; no gauge identity is assumed.