LambdaGateChain

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

Provider: the lambda-gate chain, the wave bridge and the injection prefactor

ABK26: the good-event coefficient-switch chain of l.localization.mathcalE, and the injection display e.J.sensitivity.apppp.

1. The lambda-gate chain

The printed chain is

|s_{m,*}^{-1}(z+cu_l)| 1_Q <= lambda_{1/8,2}^{-1}(z+cu_l; a_m) 1_Q
                           <= 2 lambda_{1/8,2}^{-1}(z+cu_l; a_{l-h}) 1_Q
                           <= C shom_{l-h}^{-1} ,

with Q = Q(l,l-h,z) the good local event. This module produces the composed last two steps at an explicit dimension-only-times-Ccg level:

shom_{l-h} lambda_{1/8,2}^{-1}(z+cu_l; a_m) <= 48 Ccg ,   almost surely on Q .

Constant accounting, term by term (each factor is proved separately below):

• the middle step contributes 2 (inv_lambdaSq_le_two_mul_inv_lambdaSq_of_mem_goodLocalEvent_ae): the proved Multiscale.lambdaSq_inv_le_of_mem_goodLocalEvent_ae (Provider/Multiscale/LambdaSensitivityTwin.lean) already states the frozen lambda-sensitivity switch on the good event at the manuscript's own carrier lambda_{s,q}(z+cu_l; a_L), with the explicit leading factor 1 + C_lam ||grad(k_m - k_{l-h})||_{W1inf} lambda_{3/8,2}^{-1}; the good event's own sensitivity clause -- in the proved discharged form BadEvents.gradientW1Infinity_incrementUnitCube₂_le_lambdaGate_ae -- bounds that second summand by 1. So the printed 2 is exact, not an over-estimate. Only that collapse is new here; the carrier work is consumed, not redone;
• the good event's ellipticity clause contributes 2 Ccg (inv_lambdaSq_le_of_mem_goodLocalEvent_ae): goodLocalThreshold is (1/2) Ccg^{-1} 3^{-(1/2)(n-m)_+} shom_{n-1} and at n = l-h <= l = Q.scale the positive part vanishes, so the clause reads (1/2) Ccg^{-1} shom_{l-h-1} <= lambda_{1/8,2}(z+cu_l; a_{l-h});

2 * (2 Ccg) * 12 = 48 Ccg, which is dimension-only times the caller's Ccg. The gate is delivered at the lambda-carrier form lambda_gate_chain, which is exactly the hgate binder of Provider/Localization/SwitchNormalization.lean's _of_lambdaGate bridges, at s = 1/8, q = 2, sn = shom_{l-h}, Cev = 48 Ccg.

2. The wave bridge

three_zpow_mul_underlineW2Gauge_le_waveGaugeW2 proves

3^{2l} ||k_m - k_{l-h}||_{W-underline^{2,infinity}(z+cu_l)}
  <= waveGaugeW2 m h (z+cu_l) omega ,

i.e. 3 ^ (2 * Q.scale) * underlineW2Gauge Q (shellIncrement omega (Q.scale-h) m) <= MultiscaleEstimate.waveGaugeW2 m h Q omega, at the constant 1. Three apparent obstacles all dissolve at the carriers as proved:

• SUM versus MAX: waveGaugeW2 is cubeSupBound + waveGauge, and waveGauge is itself a SUM over the missing layers of 3^l ||grad j_k|| + 3^{2l} ||grad^2 j_k||, so each of the three max-entries of 3^{2l} underlineW2Gauge is dominated by the corresponding part of the sum, the other part being nonnegative;
• pointwise-versus-suprema: NOT needed. waveGauge's summands are already at the suprema (Stream.localCubeDerivNorm, Stream.localCubeSecondDerivNorm are the exact L-infinity norms), so a pointwise fidelity statement is not the route; the route is layer subadditivity, Stream.localCube(Second)DerivNorm_sum_le, applied to shellIncrement = ShellField.sum (Ioc (l-h) m);
• the base points cubeBasePoint Q, cubeCenter Q, triadicCubeShift Q are the same function by rfl (all three identifications are already proved as BadEvents.cubeBasePoint_eq_triadicCubeShift and the wave lane's own private cubeCenter_eq_triadicCubeShift).

The zeroth-order entry goes through the proved exact-L-infinity identity Stream.streamIncrementLinftyNorm_eq_localCubeControl and the wave lane's streamIncrementLinftyNorm_le_waveGaugeW2.

3. The injection prefactor (justified)

inv_sq_sigmaBar_mul_three_zpow_le_prefactor is the step the manuscript performs "using e.shom.h.bounds from the induction hypothesis and h cgamma <= 1":

shom_{l-h-1}^{-2} 3^{4l} <= 324 cstar^{-1} cgamma 3^{4l - 2 cgamma l} .

The printed exponent arithmetic is used verbatim: the lower branch of e.shom.h.bounds (inductionState's first conjunct) at the index j = l-h-1 gives shom_j^2 >= (1/4) cstar cgamma^{-1} 3^{2 cgamma j}, hence shom_j^{-2} <= 4 cstar^{-1} cgamma 3^{-2 cgamma j} and 3^{-2 cgamma j} = 3^{-2 cgamma l} 3^{2 cgamma h} 3^{2 cgamma} <= 81. 3^{-2 cgamma l} under cgamma h <= 1 and cgamma <= 1. The manuscript performs the identical inversion in-source (shom_n^{-2} <= 4 cstar^{-1} cgamma 3^{-2 cgamma n}). The constant 4 . 81 = 324 is the honest one; the manuscript writes C.

The scale gate on m0

The landmark premise carried by every statement below is mStarStar M < m0, not the printed m0 in (mstar, infty) cap Z. Nothing else moved: the premise is forwarded verbatim to Provider.Localization.shom_continuity, no proof step here consumes it, and no frozen statement changes -- Algsuperdiff.Frozen.Section3.diffusivity_asymptotics keeps the printed mStar M < m0 and reaches the weaker-gated chain a fortiori through Provider.Scales.mStarStar_le_mStar.

Related statements elsewhere

SwitchNormalization.sigmaStarInv_gate_of_lambdaGate is the one-cube ordering step (through CoarseGraining's Ch02.oneCube_sigmaStarInv_le_lambdaSq_finite_inv) that converts this file's gate into the matrix-norm gate the switch consumes; it takes that gate as a hypothesis, so there is no cycle and it is not invoked here.

Multiscale.SharpGlobalFrame.sigmaBar_inv_le_growth_branch is the one-scale inversion of the lower branch of e.shom.h.bounds, on the identical premise list (inductionState M m0 E, j <= m0), concluding shom_j^{-1} <= 2 sqrt(cstar^{-1} cgamma) 3^{-cgamma j} -- whose square is exactly the hinv0 step of inv_sq_sigmaBar_mul_three_zpow_le_prefactor, and it is consumed there rather than re-proved.

MultiscaleEstimate.WaveSizesZeroth.streamIncrementLinftyNorm_le_waveGaugeW2, the wave lane's own zeroth-order fidelity statement against the same three-order object, is consumed below.

References

• ABK26, l.localization.mathcalE and its lambda-gate; e.J.sensitivity.apppp; e.shom.h.bounds inside d.mathcalS.def; the manuscript's own in-source twin of the prefactor inversion; e.good.local.events; l.shom.continuity.

1. The middle step: the coefficient switch a_m -> a_{l-h}

On the good event Q(l,l-h,z) the frozen Section 2.4 lambda-sensitivity engine moves the coefficient at a cost of exactly the printed factor 2.

theorem Algsuperdiff.Section3.Provider.Localization.inv_lambdaSq_le_two_mul_inv_lambdaSq_of_mem_goodLocalEvent_ae {d : ℕ} (M : ABKModel d) (Ccg : ℝ) (Q : HCPolySupport.TriadicCube d) {n L : ℤ} (hnL : n ≤ L) {s : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hs : 0 < s) (hs2 : s ≤ 1 / 2) (hq : q.IsAdmissible) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), omega ∈ BadEvents.goodLocalEvent M Ccg Q n → (HCPolySupport.Book.Ch02.lambdaSq Q s q (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega))⁻¹ ≤ 2 * (HCPolySupport.Book.Ch02.lambdaSq Q s q (Cutoff.coefficientCutoffTriadicCoeffFamily M n omega))⁻¹

The middle step of the printed lambda-gate chain.

Almost surely on the good local event Q(l,n,z), for every admissible exponent pair in the frozen engine's own window 0 < s <= 1/2,

lambda_{s,q}^{-1}(z+cu_l; a_L) 1_Q <= 2 lambda_{s,q}^{-1}(z+cu_l; a_n) 1_Q .

The printed constant 2 is exact: the engine's leading factor is 1 + C_lam ||grad(k_L-k_n)||_{W1inf} lambda_{3/8,2}^{-1}(z+cu_l;a_n) and the good event's sensitivity clause -- discharged, at the frozen 3/8 carrier, by BadEvents.gradientW1Infinity_incrementUnitCube₂_le_lambdaGate_ae -- caps the second summand by 1.

A: the conclusion holds under the caller-supplied membership omega ∈ goodLocalEvent M Ccg Q n, which is the manuscript's own indicator 1_{Q(l,l-h,z)}.

2. The last step: the good event's coarse-ellipticity clause

The gate opens through e.good.local.events.

theorem Algsuperdiff.Section3.Provider.Localization.scaleGapPos_eq_zero_of_le {m n : ℤ} (h : n ≤ m) : BadEvents.scaleGapPos m n = 0

At or below the cube's own scale the printed positive part (n-m)_+ vanishes. (The proved BadEvents.scaleGapPos_of_lt covers only the strict branch; the boundary n = Q.scale is inside the localization regime and is needed here.)

theorem Algsuperdiff.Section3.Provider.Localization.inv_lambdaSq_le_of_mem_goodLocalEvent_ae {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 0 < Ccg) (Q : HCPolySupport.TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), omega ∈ BadEvents.goodLocalEvent M Ccg Q n → (HCPolySupport.Book.Ch02.lambdaSq Q (1 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Cutoff.coefficientCutoffTriadicCoeffFamily M n omega))⁻¹ ≤ 2 * Ccg * (↑(Annealed.sigmaBar M (n - 1)))⁻¹

The last step of the printed lambda-gate chain.

Almost surely on the good local event Q(l,n,z) with n <= l = Q.scale, the coarse-ellipticity clause of e.good.local.events clamps the inverse multiscale ellipticity of a_n at the event's own comparator shom_{n-1}:

lambda_{1/8,2}^{-1}(z+cu_l; a_n) 1_Q <= 2 Ccg shom_{n-1}^{-1} .

The 3^{-(1/4)(n-m)_+} weight of the event and the 3^{-(1/2)(n-m)_+} weight of goodLocalThreshold both collapse to 1 in this regime, so the level is exactly the reciprocal of the threshold's own (1/2) Ccg^{-1}.

A: on the caller-supplied omega ∈ goodLocalEvent M Ccg Q n and 0 < Ccg.

3. The composed gate, in both consumer spellings

The chain, end to end. The premise list is l.shom.continuity's own, which is where the shom_{n-1} -> shom_n passage comes from.

theorem Algsuperdiff.Section3.Provider.Localization.lambda_gate_chain (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ABKModel d) (m0 : ℤ) (E : { E : ℝ // 1 ≤ E }), mStarStar M < m0 → Frozen.Section3.inductionState M (m0 - 1) E → C * (Disorder.cstar M)⁻¹ ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → ∀ (Ccg : ℝ), 0 < Ccg → ∀ (Q : HCPolySupport.TriadicCube d) (n L : ℤ), n ≤ L → n ≤ Q.scale → n ≤ m0 → ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), omega ∈ BadEvents.goodLocalEvent M Ccg Q n → ↑(Annealed.sigmaBar M n) * (HCPolySupport.Book.Ch02.lambdaSq Q (1 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega))⁻¹ ≤ 48 * Ccg

The composed lambda-gate, at the printed carrier lambda_{1/8,2}(z+cu_l; a_L) and the deep comparator shom_n (n = l-h at the intended instance).

On the l.shom.continuity premise list, for every coarse-ellipticity constant Ccg > 0, every localization cube Q of scale l, every cutoff pair n <= L with n <= l and n <= m0, almost surely on Q(l,n,z):

shom_n lambda_{1/8,2}^{-1}(z+cu_l; a_L) <= 48 Ccg .

The level 48 Ccg is dimension-only times the caller's Ccg; the three factors are 2 (the middle step), 2 Ccg (the event's ellipticity clause at shom_{n-1}) and 12 (shom_continuity's fourth conjunct at the adjacent pair, whose side condition cgamma <= 1 comes from the root's own cgamma <= (E^{-1})^{10}).

This is exactly the hgate binder of Provider/Localization/SwitchNormalization.lean's _of_lambdaGate bridges, at s = 1/8, q = 2, sn = shom_n, Cev = 48 Ccg.

A on omega ∈ goodLocalEvent M Ccg Q n and 0 < Ccg; a proved local Provider theorem, no node status.

4. The wave bridge

theorem Algsuperdiff.Section3.Provider.Localization.three_zpow_mul_underlineW2Gauge_le_waveGaugeW2 {d : ℕ} (Q : HCPolySupport.TriadicCube d) (m : ℤ) (h : ℕ) (omega : Cutoff.ShellSeq d) : 3 ^ (2 * Q.scale) * underlineW2Gauge Q (Stream.shellIncrement omega (Q.scale - ↑h) m) ≤ MultiscaleEstimate.waveGaugeW2 m h Q omega

At the localization cube Q of scale l and the missing-layer range (l-h, m],

3^{2l} ||k_m - k_{l-h}||_{W-underline^{2,infinity}(z+cu_l)}
  <= waveGaugeW2 m h (z+cu_l) omega ,

at the honest constant 1 -- no dimension factor is needed.

The three legs, in the order they appear in underlineW2Gauge's max: 3^{2l} ||grad^2|| and 3^l ||grad|| are dominated by the corresponding halves of waveGauge's per-layer sum after layer subadditivity of the exact L-infinity gauges (Stream.localCubeSecondDerivNorm_sum_le, Stream.localCubeDerivNorm_sum_le, applied to shellIncrement = ShellField.sum (Ioc (l-h) m)), the other half of each summand being nonnegative; the zeroth-order leg ||.||_{L-infinity} is the proved exact identity Stream.streamIncrementLinftyNorm_eq_localCubeControl composed with the wave lane's own streamIncrementLinftyNorm_le_waveGaugeW2. The base points cubeBasePoint Q and cubeCenter Q are the same function by rfl.

theorem Algsuperdiff.Section3.Provider.Localization.three_zpow_mul_underlineW2Gauge_sq_le_waveGaugeW2_sq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (m : ℤ) (h : ℕ) (omega : Cutoff.ShellSeq d) : 3 ^ (4 * Q.scale) * underlineW2Gauge Q (Stream.shellIncrement omega (Q.scale - ↑h) m) ^ 2 ≤ MultiscaleEstimate.waveGaugeW2 m h Q omega ^ 2

The wave bridge, squared -- the form the injection remainder meets, since the frozen sensitivity engine's remainder carries the squares of the two gate quantities (the 3^{4l} fingerprint).

5. The injection prefactor

Justified by e.shom.h.bounds and h cgamma <= 1.

theorem Algsuperdiff.Section3.Provider.Localization.inv_sq_sigmaBar_mul_three_zpow_le_prefactor {d : ℕ} (M : ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hstate : Frozen.Section3.inductionState M m0 E) (l : ℤ) (h : ℕ) (hj : l - ↑h - 1 ≤ m0) (hgamma1 : M.gamma ≤ 1) (hgh : M.gamma * ↑h ≤ 1) : (↑(Annealed.sigmaBar M (l - ↑h - 1)))⁻¹ ^ 2 * 3 ^ (4 * l) ≤ 324 * (Disorder.cstar M)⁻¹ * M.gamma * 3 ^ (4 * ↑l - 2 * M.gamma * ↑l)

The injection prefactor.

From the lower branch of e.shom.h.bounds (the first conjunct of inductionState) at the index j = l-h-1, together with cgamma h <= 1 and cgamma <= 1:

shom_{l-h-1}^{-2} 3^{4l} <= 324 cstar^{-1} cgamma 3^{4l - 2 cgamma l} .

Exponent arithmetic, verbatim: shom_j^2 >= (1/4) cstar cgamma^{-1} 3^{2 cgamma j} gives shom_j^{-2} <= 4 cstar^{-1} cgamma 3^{-2 cgamma j}, and -2 cgamma j = -2 cgamma l + 2 cgamma h + 2 cgamma with 3^{2 cgamma h} 3^{2 cgamma} <= 3^2. 3^2 = 81. The manuscript performs the identical inversion in-source. The honest constant is 4 . 81 = 324; the manuscript writes C.

Only the exponent split -2 cgamma j = -2 cgamma l + 2 cgamma h + 2 cgamma is new here.

The manuscript's loading identities

theorem Algsuperdiff.Section3.Provider.Localization.vecNormSq_inverseSqrtLoad_eq {d : ℕ} (sigma : Observable.PositiveScalar) (v : HCPolySupport.Vec d) : HCPolySupport.vecNormSq (Observable.inverseSqrtLoad sigma v) = (↑sigma)⁻¹ * HCPolySupport.vecNormSq v

|shom^{-1/2} v|^2 = shom^{-1} |v|^2.

theorem Algsuperdiff.Section3.Provider.Localization.vecDot_inverseSqrtLoad_sqrtLoad {d : ℕ} (sigma : Observable.PositiveScalar) (v : HCPolySupport.Vec d) : HCPolySupport.vecDot (Observable.inverseSqrtLoad sigma v) (Observable.sqrtLoad sigma v) = HCPolySupport.vecNormSq v

shom^{-1/2} v . shom^{1/2} v = |v|^2: the manuscript's paired loading is normalized.

theorem Algsuperdiff.Section3.Provider.Localization.injection_remainder_bound {Cresp Ccg S G W Lam A B P : ℝ} (hCresp : 0 ≤ Cresp) (hCcg : 0 ≤ Ccg) (hS : 0 ≤ S) (hG : 0 ≤ G) (hLam0 : 0 ≤ Lam) (hLamS : Lam ≤ 2 * Ccg * S) (hA : A ≤ 8 * S) (hB : B ≤ 2) (hP : S ^ 2 * G ≤ P) : Cresp * (A * (G * W ^ 2) * Lam + B * (G * W ^ 2) * Lam ^ 2) ≤ Cresp * ((16 * Ccg + 8 * Ccg ^ 2) * P * W ^ 2)

The abstract-real core of the injection pricing: the two remainder terms of the frozen delta = 1 endpoint, gated at Lam <= 2 Ccg S with the loading data A <= 8 S, B <= 2, and the prefactor substitution S^2 G <= P.