PrincipalResponseSwitchActualDisplay

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

Provider: the good-event energy display with a per-cube event, and its actual consumer

Source displays in ABK26:

• l.approximate.recurrence.formula (label), Step 3;
• the gauge-switch chain, closing;
• e.nablaw.in.L.eight (label), quoted as the ellipticity budget;
• the independence sentence;
• e.lower.bound.principal.one.pre (label; display);
• e.good.local.events (label), instantiated as cQ_z := cQ(n, m-h, z);
• e.recurrence.params (label; display).

What this module supplies

Two things.

1. The-generalized display. The manuscript's event cQ_z:= cQ(n, m-h, z) varies with the cube z + cu_n. A display whose good event is a single fixed set cannot consume the per-cube switch; descendantsAverage_integral_goodEventEnergy_le_annealedCube_family is the same composition with the event carried as a family Ebad: TriadicCube d -> Set Omega, and with the switch hypothesis taken almost surely rather than pointwise, which is the form in which the switch is actually available (see ApproximateRecurrence.PrincipalResponseSwitchActualPerCube).

2. A consumer with hswitch produced. descendantsAverage_integral_principalGoodEventEnergy_le_annealedCube is that display instantiated at the actual cutoff carrier -- CutoffSample d, (Cutoff.cutoffSampleLaw M).toMeasure, the per-cube bad event principalBadEvent M Ccg . lowScale, and the three terms switchCubeEnergy, switchCubeQuad, switchEllipLoad -- in which the switch hypothesis is not a binder: it is discharged inside the proof from switchCubeEnergy_indicator_le_ae. The cgamma^6 gate is likewise discharged, at the corrected recurrence gap and the manuscript's own standing range cgamma in (0, 1/4].

What the consumer still owes, and to whom

The consumer's remaining binders are exactly the substantive inputs the manuscript itself quotes from elsewhere, plus the two residuals recorded in PrincipalResponseSwitchActualPerCube:

• hlam0 -- strict positivity of lambda_{3/8,2}(z+cu_n; a_{m-h}) on the good event;
• hshell -- the centered-shell size (see that module's docstring);
• hellip -- the ellipticity budget, quoted by the manuscript from e.nablaw.in.L.eight;
• hindep -- the independence replacement;
• hbudget -- the numerical smallness in which "increasing M in e.cgamma.constraints if necessary" is made quantitative for the remainder;
• the three integrability families.

hswitch is gone.

The 3/2

The switch factor carried through is the honest 1 + (3/2) Delta rather than the printed 1 + Delta; see the module docstring of PrincipalResponseSwitchActualPerCube for exactly where the printed factor needs a constant margin that neither the manuscript nor this repository supplies.

Main results

• annealedCubeBlockQuadratic_nonneg_actual
• descendantsAverage_integral_goodEventEnergy_le_annealedCube_family
• gridSwitchDiscount_eq_rpow_recurrenceGap

Nonnegativity of the annealed cube form

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.annealedCubeBlockQuadratic_nonneg_actual {d : ℕ} [NeZero d] (M : ABKModel d) (L n : ℤ) (V : HCPolySupport.BlockVec d) : 0 ≤ HCPolySupport.blockVecDot V (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M L) n) V)

The annealed cube quadratic form is nonnegative. The proved Loewner plateau of ApproximateRecurrence.PrincipalResponseSwitchPlateau puts the infinite-volume bfAhom_L = diag(shom_L, shom_L^{-1}) below the finite-cube bfAhom_L(cu_n), and the former is a positive diagonal.

Unconditional: no caller-supplied proposition enters.

The-generalized display

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.descendantsAverage_integral_goodEventEnergy_le_annealedCube_family {d : ℕ} {Omega : Type u_1} {mOmega : MeasurableSpace Omega} {mu : MeasureTheory.Measure Omega} [NeZero d] (M : ABKModel d) (L n : ℤ) (Q : HCPolySupport.TriadicCube d) (j : ℕ) (energy cubeQuad ellipLoad : HCPolySupport.TriadicCube d → Omega → ℝ) (W : HCPolySupport.TriadicCube d → Omega → HCPolySupport.BlockVec d) (Ebad : HCPolySupport.TriadicCube d → Set Omega) {delta Cs Cell : ℝ} (hdelta0 : 0 ≤ delta) (hCs0 : 0 ≤ Cs) (hswitch : ∀ R ∈ HCPolySupport.descendantsAtDepth Q j, ∀ᵐ (omega : Omega) ∂mu, energy R omega * (Ebad R)ᶜ.indicator (fun (x : Omega) => 1) omega ≤ (1 + delta) * cubeQuad R omega + Cs * delta * ellipLoad R omega) (hgoodInt : ∀ R ∈ HCPolySupport.descendantsAtDepth Q j, MeasureTheory.Integrable (fun (omega : Omega) => energy R omega * (Ebad R)ᶜ.indicator (fun (x : Omega) => 1) omega) mu) (hcubeInt : ∀ R ∈ HCPolySupport.descendantsAtDepth Q j, MeasureTheory.Integrable (cubeQuad R) mu) (hellipInt : ∀ R ∈ HCPolySupport.descendantsAtDepth Q j, MeasureTheory.Integrable (ellipLoad R) mu) (hindep : ∀ R ∈ HCPolySupport.descendantsAtDepth Q j, ∫ (omega : Omega), cubeQuad R omega ∂mu = ∫ (omega : Omega), HCPolySupport.blockVecDot (W R omega) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M L) n) (W R omega)) ∂mu) (hellip : (HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => ∫ (omega : Omega), ellipLoad R omega ∂mu) ≤ Cell) (hdeltaGate : delta ≤ M.gamma ^ 6) (hbudget : Cs * delta * Cell ≤ M.gamma ^ 6 / 2) : (HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => ∫ (omega : Omega), energy R omega * (Ebad R)ᶜ.indicator (fun (x : Omega) => 1) omega ∂mu) ≤ ((1 + M.gamma ^ 6) * HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => ∫ (omega : Omega), HCPolySupport.blockVecDot (W R omega) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M L) n) (W R omega)) ∂mu) + M.gamma ^ 6 / 2

e.lower.bound.principal.one.pre with the manuscript's own per-cube event.

ABK26's cQ_z := cQ(n, m-h, z) depends on the cube z + cu_n, so the good event enters the display as a family Ebad : TriadicCube d -> Set Omega, and no union over the grid is formed. The switch hypothesis is taken almost surely, which is the form in which it is available at the cutoff carrier.

At the field index L (the manuscript's m - h), the cube scale n, the localization cube Q and the depth j:

  avsum_R E[ energy_R 1_{cQ_R} ]
    <= (1 + cgamma^6) avsum_R E[ W_R . bfAhom_L(cu_n) W_R ] + (1/2) cgamma^6 .

The nonnegativity of the annealed grid average is not assumed: it is annealedCubeBlockQuadratic_nonneg_actual, hence the proved Loewner plateau.

: this statement holds only under the propositions supplied by its binders -- hdelta0, hCs0, hswitch, hgoodInt, hcubeInt, hellipInt, hindep, hellip, hdeltaGate, hbudget, whose provenance is listed in the module docstring. It is a provider A, not a source-facing frozen declaration.

The manuscript's own gap, and the cgamma^6 gate on the display

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gridSwitchDiscount_eq_rpow_recurrenceGap {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j a : ℕ) (gamma : ℝ) (m h : ℤ) (hscale : Q.scale - ↑j = recurrenceMesoScale a gamma m h) : gridSwitchDiscount Q j (m - h) = 3 ^ (-(↑(recurrenceGap a gamma) / 4))

At the manuscript's own mesoscale n = m - h - a ceil|log_3 gamma| (e.recurrence.params, label, at the free multiplier) the grid switch discount is exactly 3^{-(m-h-n)/4} = 3^{-(recurrenceGap a gamma)/4}.

: this statement holds only under the proposition supplied by its binder hscale, the identification of the grid scale with the manuscript's mesoscale. It is a provider A, not a source-facing frozen declaration.