LocalizationAssemblyCore

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

Provider: the per-(l,z) core of the localization assembly

It carries the two scalar inputs named (i) and the per-(l,z) composed switch endpoints they close; the l-sum, the z-average and the five-term display live in the sibling Provider/Localization/LocalizationAssembly.lean.

What is here

1. The loading ball of the breakdown legs (§1). The proved Breakdown.breakdownLegA_le_of_paired_bound says that a bound on J(R, σ^{-1/2}v, σ^{1/2}v; a) over the ball |v|² ≤ 2 bounds the leg. The converse is what the assembly needs — the leg is an admissible majorant of every paired loading in that ball — and it holds because the primal frame map e ↦ e₁ - e₂ maps the doubled unit sphere ONTO the ball (exists_frameLegAVec_eq). This is the exact statement that lets the deep-response comparator of the printed first two terms be the SAME carrier breakdownLegA / breakdownLegB that the printed left-hand side uses, at (a_{l-h}, σ_{l-h}) instead of (a_m, σ_m).

2. The scalar input (§2) (i):

3. For one grid cube R of the printed tiling, on one probability-one event and uniformly in the cube,

   legA(R; a_m, σ_m)
     ≤ 24 · legA(R; a_{l-h}, σ_{l-h})
       + 8·Cinj(Ccg) · c⋆⁻¹ γ · waveSizeW2(m,h,R)²
       + Cs·48Ccg · switchRemainder γ E h j
   

   with l = R.scale = m - j. The three summands are the printed first, third and fifth terms of e.localization.mathcalE.estimate before the z-average and the l-sum.

Fidelity and constants

• The deep comparator of the printed display is max_{|e|=1} J(z + □_l, ·, ·; a_{l-h}); the carrier here is breakdownLegA R (a_{l-h}) (isotropic σ_{l-h}), which is twice that maximum by quadratic homogeneity — exactly the convention the proved e.mathcal.E.breakdown already uses on the printed left-hand side. In the per-(l,z) display of §3 the same doubling does sit on both sides; in the sibling module's display it does NOT, because there the left-hand side is 𝓔², which carries no doubling, and legScaleAverage is degree-one homogeneous. Its provenance is 8 (the proved SwitchNormalization.breakdownLeg{A,B}_le_of_shom_switch at the ρ = 4 window) times 3 (the printed injection factor). Nothing downstream is sharp in it (e.what.homogenization.gives absorbs it into its own C).
• No min/3^{2γΔ} reshaping happens here: the remainder is emitted through the proved cross-file seam AggregationRemainder.switchRemainder_eq_of_int_gap ((iii)), never re-derived.

The scale gate on m0 (-bin statement change)

The landmark premise carried by every declaration below is mStarStar M < m0, not the printed m0 in (mstar, infty) cap Z. Nothing else moved: the premise is forwarded verbatim to the proved producers consumed here, no proof step here consumes it, and no frozen statement changes.

1. The loading ball of the breakdown legs

Breakdown.frameLegAVec e = e₁ - e₂ and Breakdown.frameLegBVec e = e₁ + e₂ send the doubled unit sphere |e| = 1 into the loading ball |v|² ≤ 2 (the proved vecNormSq_frameLeg{A,B}Vec_le). They are also ONTO it: given v with |v|² ≤ 2, the pair (v/2 + u, ∓ v/2 + u) with |u|² = (2-|v|²)/4 is a doubled unit direction with the prescribed image, by the parallelogram identity. A single coordinate spike supplies u, which is where [NeZero d] enters.

theorem Algsuperdiff.Section3.Provider.Localization.exists_frameLegAVec_eq {d : ℕ} [NeZero d] {v : HCPolySupport.Vec d} (hv : HCPolySupport.vecNormSq v ≤ 2) : ∃ (e : HCPolySupport.FullBlockVec d), HCPolySupport.Book.Ch02.fullBlockVecNormSq e = 1 ∧ frameLegAVec e = v

The primal frame map is onto the loading ball. Every v of squared length at most 2 is the primal frame combination e₁ - e₂ of a doubled unit direction.

theorem Algsuperdiff.Section3.Provider.Localization.exists_frameLegBVec_eq {d : ℕ} [NeZero d] {v : HCPolySupport.Vec d} (hv : HCPolySupport.vecNormSq v ≤ 2) : ∃ (e : HCPolySupport.FullBlockVec d), HCPolySupport.Book.Ch02.fullBlockVecNormSq e = 1 ∧ frameLegBVec e = v

The adjoint frame map is onto the loading ball.

theorem Algsuperdiff.Section3.Provider.Localization.responseJ_paired_le_breakdownLegA {d : ℕ} [NeZero d] {Q R : HCPolySupport.TriadicCube d} {k : ℤ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (sigma : Observable.PositiveScalar) (hR : R ∈ HCPolySupport.descendantsAtScale Q k) {v : HCPolySupport.Vec d} (hv : HCPolySupport.vecNormSq v ≤ 2) : HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (a.coeffOn R) (Observable.inverseSqrtLoad sigma v) (Observable.sqrtLoad sigma v) ≤ breakdownLegA R a (Observable.isotropicComparatorMatrix sigma)

The primal leg majorizes every paired loading of the ball. The exact converse of the proved Breakdown.breakdownLegA_le_of_paired_bound: on a descendant cube the leg at the isotropic comparator is an upper bound for J(R, σ^{-1/2}v, σ^{1/2}v; a) at every v with |v|² ≤ 2.

theorem Algsuperdiff.Section3.Provider.Localization.responseJ_paired_le_breakdownLegB {d : ℕ} [NeZero d] {Q R : HCPolySupport.TriadicCube d} {k : ℤ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (sigma : Observable.PositiveScalar) (hR : R ∈ HCPolySupport.descendantsAtScale Q k) {v : HCPolySupport.Vec d} (hv : HCPolySupport.vecNormSq v ≤ 2) : HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (a.coeffOn R).transpose (Observable.inverseSqrtLoad sigma v) (Observable.sqrtLoad sigma v) ≤ breakdownLegB R a (Observable.isotropicComparatorMatrix sigma)

The adjoint leg majorizes every paired loading of the ball.

theorem Algsuperdiff.Section3.Provider.Localization.injection_waveLeg_le_waveSizeW2_sq {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 0 ≤ Ccg) (R : HCPolySupport.TriadicCube d) (h : ℕ) (L : ℤ) (omega : Cutoff.ShellSeq d) : 324 * BadEvents.responseSensitivityConst d * (16 * Ccg + 8 * Ccg ^ 2) * ((Disorder.cstar M)⁻¹ * M.gamma * 3 ^ (4 * ↑R.scale - 2 * M.gamma * ↑R.scale)) * underlineW2Gauge R (Stream.shellIncrement omega (R.scale - ↑h) L) ^ 2 ≤ 324 * BadEvents.responseSensitivityConst d * (16 * Ccg + 8 * Ccg ^ 2) * ((Disorder.cstar M)⁻¹ * M.gamma) * MultiscaleEstimate.waveSizeW2 M L h R omega ^ 2

The wave-gauge bound at the fixed sample ((i), second item).

The priced wave remainder of the J-injection display carries 3^{4l - 2γl} · underlineW2Gauge(R, k_L - k_{l-h})².

Deterministic, sample by sample; no measure and no Orlicz datum occurs.

3. The per-(l,z) composed switch endpoints

All three ingredients are made first (one null set for every triadic cube, gap and coefficient scale), because the z-aggregation fixes the sample and then ranges over the grid.

theorem Algsuperdiff.Section3.Provider.Localization.breakdownLegA_le_deep_wave_remainder_ae (d : ℕ) [NeZero d] : ∃ (Cs : ℝ) (Cg : ℝ) (Ci : ℝ), 0 < Cs ∧ 0 < Cg ∧ 0 < Ci ∧ ∀ (M : ABKModel d) (m0 : ℤ) (E : { E : ℝ // 1 ≤ E }), mStarStar M < m0 → Frozen.Section3.inductionState M (m0 - 1) E → Cs * (Disorder.cstar M)⁻¹ ≤ ↑E → Cg * (Disorder.cstar M)⁻¹ ≤ ↑E → Ci * (Disorder.cstar M)⁻¹ ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → ∀ (Ccg : ℝ), 0 < Ccg → ∀ m ≤ m0, ∀ (hgap : ℕ), M.gamma * ↑hgap ≤ 1 → ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (j : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - ↑j), omega ∈ BadEvents.goodLocalEvent M Ccg R (R.scale - ↑hgap) → breakdownLegA R (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) (Observable.isotropicComparatorMatrix (Annealed.sigmaBar M m)) ≤ 24 * breakdownLegA R (Cutoff.coefficientCutoffTriadicCoeffFamily M (R.scale - ↑hgap) omega) (Observable.isotropicComparatorMatrix (Annealed.sigmaBar M (R.scale - ↑hgap))) + 8 * (324 * BadEvents.responseSensitivityConst d * (16 * Ccg + 8 * Ccg ^ 2) * ((Disorder.cstar M)⁻¹ * M.gamma)) * MultiscaleEstimate.waveSizeW2 M m hgap R ↑omega ^ 2 + Cs * (48 * Ccg) * switchRemainder M.gamma (↑E) hgap j

The composed primal per-(l,z) endpoint.

For the multiscale root's own regime, one gap h with γ h ≤ 1 and one working scale m ≤ m0: on ONE probability-one event, simultaneously for every depth j and every grid cube R of the printed tiling at scale l = m - j, on the manuscript's own good event 𝒬(l, l-h, z),

legA(R; a_m, σ_m) ≤ 24 · legA(R; a_{l-h}, σ_{l-h})
                    + 8·Cinj(Ccg)·c⋆⁻¹γ · waveSizeW2(m,h,R)²
                    + Cs·48Ccg · switchRemainder γ E h j .

The three summands are, before the z-average and the l-sum, the printed first, third and fifth terms of e.localization.mathcalE.estimate. The 24 is 8 (the proved switch endpoint at the ρ = 4 window) times 3 (the printed injection factor); measured at the printed max_{|e|=1} carrier this is a factor-4 loss against the printed 6 in a dimension-free numeral, chartered by [C]'s own text and disclosed in the module header.

A, inherited: 0 < Ccg and the good-event membership.

theorem Algsuperdiff.Section3.Provider.Localization.breakdownLegB_le_deep_wave_remainder_ae (d : ℕ) [NeZero d] : ∃ (Cs : ℝ) (Cg : ℝ) (Ci : ℝ), 0 < Cs ∧ 0 < Cg ∧ 0 < Ci ∧ ∀ (M : ABKModel d) (m0 : ℤ) (E : { E : ℝ // 1 ≤ E }), mStarStar M < m0 → Frozen.Section3.inductionState M (m0 - 1) E → Cs * (Disorder.cstar M)⁻¹ ≤ ↑E → Cg * (Disorder.cstar M)⁻¹ ≤ ↑E → Ci * (Disorder.cstar M)⁻¹ ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → ∀ (Ccg : ℝ), 0 < Ccg → ∀ m ≤ m0, ∀ (hgap : ℕ), M.gamma * ↑hgap ≤ 1 → ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (j : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - ↑j), omega ∈ BadEvents.goodLocalEvent M Ccg R (R.scale - ↑hgap) → breakdownLegB R (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) (Observable.isotropicComparatorMatrix (Annealed.sigmaBar M m)) ≤ 24 * breakdownLegB R (Cutoff.coefficientCutoffTriadicCoeffFamily M (R.scale - ↑hgap) omega) (Observable.isotropicComparatorMatrix (Annealed.sigmaBar M (R.scale - ↑hgap))) + 8 * (324 * BadEvents.responseSensitivityConst d * (16 * Ccg + 8 * Ccg ^ 2) * ((Disorder.cstar M)⁻¹ * M.gamma)) * MultiscaleEstimate.waveSizeW2 M m hgap R ↑omega ^ 2 + Cs * (48 * Ccg) * switchRemainder M.gamma (↑E) hgap j

The composed adjoint per-(l,z) endpoint. The (J3) mirror of breakdownLegA_le_deep_wave_remainder_ae: same regime list, same gap window, same constants 24 / 8·Cinj / Cs·48Ccg, every carrier transposed. The gate is the SAME printed lambda-gate (SwitchNormalization.sigmaStarInv_transpose_gate_of_lambdaGate is an adjoint invariance, not a second estimate), and the deep and wave terms come from the transposed injection endpoint of AdjointInjection.