LayerUniform

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

The a.e.-uniform layer lift, and the collar leg of Step 3

LayerMass.toReal_tsum_simplexPartition_le_payload reduces Step 3 of p.bfA.multiscalebound (ABK26) to the single hypothesis

hlayer : ∀ n : ℕ, ∑ □ ∈ 𝒲(□_m,n), ∑ 𝔰 ∈ S(□), f 𝔰
           ≤ ENNReal.ofReal (layerContrib b γ hs k₀ Ktot Ccol Mass Bad n) ,

a statement about one sample ω, quantified over all layers, all Whitney cubes and all cells at once. Step3Seams proves the three simplex legs of Step 1 (e.good.simplex.consequence at the manuscript's own simplex carrier) only per cube: each of them is an ∀ᵐ ω statement whose null set depends on the cube Q and on the two scales k, i. This module supplies the two things that stand between those legs and hlayer.

What is proved

1. The a.e.-uniform lift (items (1) of the #conclusion remainder). TriadicCube d is countable (Homogenization.instCountableTriadicCube) and so is ℤ, so MeasureTheory.ae_all_iff -- applied three times, once per quantifier, which is what makes the iterated form over TriadicCube d × ℤ × ℤ legitimate -- turns the per-cube family into a single null set. The two non-random ordering hypotheses Q.scale ≤ i and i ≤ m0 are carried inside the a.e. statement as implications; guarding them is ae_imp_of_imp_ae, a two-line case split, and no measurability is used. The three lifts are responseJ_simplexDomain_normalized_flux_le_ae_uniform, responseJ_simplexDomain_normalized_slope_le_ae_uniform and blockVecDot_coarseBlockMatrix_simplexDomain_normalized_le_ae_uniform; the third is specialized to the Whitney layer in blockVecDot_coarseBlockMatrix_whitneySimplexCells_le_ae, which is the exact per-cell datum Step3Seams.sum_sum_ofReal_cellWeight_le_ofReal_mul consumes on the good leg. Note the binder economy of the lift: the proved legs carry hm: Q.scale ≤ m0 and hji: Q.scale ≤ i and hi: i ≤ m0; the first is implied by the other two, so the uniform statements carry only two.

2. From the layer-envelope reading of the collar gradient estimate -- |∇ℓ̂_p(𝔰) - p| ≤ Cgrad |p| 3^{b(k+h_k)} on the cells of a layer-k collar cube, which is what leaves standing of the printed component-local display -- the normalized display

   |(∇·D̂_q)(𝔰)|²/|q|² + |∇ℓ̂_p(𝔰)|²/|p|² ≤ 8 Cgrad² 3^{2 b (k + h_k)}
   

   is bounds_on_slopes_when_bad. The 8 is's own 2 × (2 + 2): the per-leg step |∇ℓ̂_p|² ≤ 2(1 + ratio²)|p|² ≤ 4 Cgrad² 3^{2b(k+h_k)} |p|² (vecNormSq_le_four_mul_of_slope_error, which uses 1 ≤ Cgrad and 1 ≤ 3^{b(k+h_k)} exactly as records) summed over the two legs.

3. The collar leg made dischargeable. The per-cell term of the second sum of Multiscale.sum_of_a_decomp (SubadditiveDecomposition.lean) is the 𝐀_L(𝔰) quadratic form loaded at the competitor's cell constants (Fc 𝔰, Gc 𝔰). Since e.good.simplex.consequence is proved for an arbitrary load, it applies at that load verbatim, and item 2 then trades the competitor's slopes for the original ones: blockVecDot_coarseBlockMatrix_collar_whitneySimplexCells_le_ae bounds the collar cell term by 4 Cgrad² 3^{2b(k+h_k)} times the good-leg majorant at (p,q). That is a uniform per-cell constant on each cube. The declarations in this file still accept the layer-uniform majorants as interface data. Later conclusion providers, including ConclusionKtotEnvelope.lean and ConclusionAssemblyFinal.lean, produce and consume the concrete layer envelopes; that downstream discharge is not credited to this abstract file.

4. The two legs assembled in the hlayer shape. sum_sum_ofReal_two_leg_le_ofReal_layerContrib runs sum_sum_ofReal_cellWeight_le_ofReal_mul once per leg at the two constants Ktot 3^{γ(k+h_k)} and Ccol 3^{2b(k+h_k)} of ConclusionAssembly.layerContrib and adds them, and toReal_tsum_simplexPartition_two_leg_le_payload composes the result with LayerMass.toReal_tsum_simplexPartition_le_payload to reach the Step-3 payload. Its cell functional is f 𝔰 = ofReal(|𝔰|/|□_m| . g_good 𝔰) + ofReal(|𝔰|/|□_m| . g_col 𝔰), the [0,∞] reading of the right-hand side of e.sum-of-a-decomp.

What is not proved in this file, and what its A carries

• This file does not construct the affine approximation l.piecewise.affine.approx. Its collar gradient conclusion enters only as the two hypotheses vecNormSq (Fv - p) ≤ Cgrad² 3^{2b(k+h_k)} vecNormSq p (and the q-twin) of item 2/3, in the source-shaped A style of Multiscale.sum_of_a_decomp (SubadditiveDecomposition.lean)'s hbadF/hbadG/hoffF/hoffG (which carry clauses 1 and 3 of e.hat.linear.properties; this module carries the layer-envelope reading of clause 2, the one clause SubadditiveDecomposition.lean explicitly does not use). Accordingly hF, hG, and Cgrad are explicit A obligations of the declarations here. The later affine providers SuperposedPotentialClosure.lean, SuperposedDivergencePotential.lean, and SuperposedEnvelope.lean establish the concrete potential, solenoidal, and envelope legs used downstream; those theorems do not retroactively turn this abstract interface into a source-node export.
• At bad cells (hbadF/hbadG) the competitor constants vanish, so the collar term is 0 there --- the block pairing of a zero load is zero --- and the A antecedent is vacuous. The collar leg's live cells are the good cells of 𝒩(ℐ), which is where the antecedent is read.
• The declarations here do not prove the mass comparison between the collar family (𝒩(ℐ) ∩ 𝒲(□_m,k)) ∖ ℐ and the bad family ℐ_k; they take hmasscol : ∑_{□ ∈ S_col} |□|/|□_m| ≤ Bad n as an explicit A obligation. CollarMass.lean now proves the concrete collar-vs-bad comparison used later.
• The declarations here also leave the cell functionals g_good, g_col, the subfamilies, and their pointwise bounds as abstract A data. ConclusionCompetitor.lean supplies the concrete coefficient-family and competitor instantiation. This file therefore remains a conditional layer-pricing interface even though later providers discharge its inputs.

Main results

• blockVecDot_coarseBlockMatrix_simplexDomain_normalized_le_ae_uniform: e.good.simplex.consequence at the simplex carrier, on ONE null set for all cubes, all cell scales and all frame scales.
• blockVecDot_coarseBlockMatrix_whitneySimplexCells_le_ae: the same, read on a Whitney layer.
• vecNormSq_le_four_mul_of_slope_error, quadratic_form_le_of_slope_bounds: the two arithmetic steps behind e.bounds.on.slopes.when.bad --- a slope within Cgrad 3^{b(k+h_k)} of the load has square at most 4 Cgrad² 3^{2b(k+h_k)} times the load's, and that trade passes to the cell's quadratic form.
• blockVecDot_coarseBlockMatrix_collar_whitneySimplexCells_le_ae: the collar leg's per-cell bound.
• sum_sum_ofReal_two_leg_le_ofReal_layerContrib: the hlayer shape, one Whitney layer priced by layerContrib.

References

• ABK26, e.sum-of-a-decomp, e.good.simplex.consequence, Step 1, Step 3, e.bounds.on.slopes.when.bad, l.piecewise.affine.approx, r.gradient.bound.simplified, e.SW.def.

Two countability primitives

The three simplex legs of Step 1, a.e.-uniformly

theorem Algsuperdiff.Section3.Provider.Multiscale.blockVecDot_coarseBlockMatrix_simplexDomain_normalized_le_ae_uniform {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (Q : HCPolySupport.TriadicCube d) (k i : ℤ), Q.scale ≤ i → i ≤ m0 → omega ∉ BadEvents.badOsc M Q → omega ∉ BadEvents.badLoc M Q → ∀ (L : ℤ), Q.scale ≤ L → ∀ (T : Whitney.KuhnCell d), T.supportCube ∈ HCPolySupport.descendantsAtScale Q k → ∀ (p q : HCPolySupport.Vec d), HCPolySupport.blockVecDot ((√↑(Annealed.sigmaBar M i))⁻¹ • p, √↑(Annealed.sigmaBar M i) • q) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix (simplexDomain T) (simplexCoeffOn (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) T)) ((√↑(Annealed.sigmaBar M i))⁻¹ • p, √↑(Annealed.sigmaBar M i) • q)) ≤ 640 * simplexCrudeConst d (1 / 4) * HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q k (1 / 4) * (1 + 8 * BadEvents.bigLambdaSensitivityConst d * (Disorder.cstar M)⁻¹ * M.gamma * 3 ^ (-(2 * M.gamma * ↑Q.scale)) * (BadEvents.incrementUnitCube₂ Q Q.scale L omega).w1Infinity ^ 2) * HCPolySupport.vecNormSq p + 320 * simplexCrudeConst d (1 / 4) * HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q k (1 / 4) * 3 ^ (M.gamma * (↑i - ↑Q.scale)) * HCPolySupport.vecNormSq q

e.good.simplex.consequence at the manuscript's own carrier, a.e.-uniformly (ABK26, assembled). One null set serves every triadic cube Q, every cell scale k and every frame scale i simultaneously -- which is what a layer of e.sum-of-a-decomp needs, since a layer contains many cubes and Step 3 sums over all layers.

The uniform statement, read on one Whitney layer

theorem Algsuperdiff.Section3.Provider.Multiscale.blockVecDot_coarseBlockMatrix_whitneySimplexCells_le_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) (m : ℤ) (hn : ℕ → ℕ) {i : ℤ} (hmi : m - 1 ≤ i) (hi : i ≤ m0) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (n : ℕ), ∀ Q ∈ Whitney.whitneyLayer m hn n, omega ∉ BadEvents.bad M Q → ∀ (L : ℤ), Q.scale ≤ L → ∀ T ∈ Whitney.whitneySimplexCells m hn n Q, ∀ (p q : HCPolySupport.Vec d), HCPolySupport.blockVecDot ((√↑(Annealed.sigmaBar M i))⁻¹ • p, √↑(Annealed.sigmaBar M i) • q) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix (simplexDomain T) (simplexCoeffOn (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) T)) ((√↑(Annealed.sigmaBar M i))⁻¹ • p, √↑(Annealed.sigmaBar M i) • q)) ≤ 640 * simplexCrudeConst d (1 / 4) * HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q (Whitney.simplexScale m hn n) (1 / 4) * (1 + 8 * BadEvents.bigLambdaSensitivityConst d * (Disorder.cstar M)⁻¹ * M.gamma * 3 ^ (-(2 * M.gamma * ↑Q.scale)) * (BadEvents.incrementUnitCube₂ Q Q.scale L omega).w1Infinity ^ 2) * HCPolySupport.vecNormSq p + 320 * simplexCrudeConst d (1 / 4) * HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q (Whitney.simplexScale m hn n) (1 / 4) * 3 ^ (M.gamma * (↑i - ↑Q.scale)) * HCPolySupport.vecNormSq q

e.good.simplex.consequence on a Whitney layer. Almost surely, for every layer n, every layer-n Whitney cube □ on which the bad event does not occur, and every cell 𝔰 of the layer-n decomposition of □, the load-(p,q) quadratic form of 𝐀_L(𝔰) in the 𝐀hom_i^{-1/2} frame obeys the Step-1 bound at the cell scale simplexScale m hn n = m - (n+1) - h_{n+1} of e.SW.def.

Q.scale ≤ i is automatic: layer 0 is empty and a layer-n cube has scale m - n - h_n ≤ m - 1 ≤ i.

e.bounds.on.slopes.when.bad's constant

theorem Algsuperdiff.Section3.Provider.Multiscale.vecNormSq_le_four_mul_of_slope_error {d : ℕ} {Cgrad t : ℝ} {F p : HCPolySupport.Vec d} (hC : 1 ≤ Cgrad) (ht : 1 ≤ t) (hF : HCPolySupport.vecNormSq (F - p) ≤ Cgrad ^ 2 * t * HCPolySupport.vecNormSq p) : HCPolySupport.vecNormSq F ≤ 4 * (Cgrad ^ 2 * t) * HCPolySupport.vecNormSq p

The per-leg step. If a field's slope on a cell differs from the load by at most Cgrad 3^{b(k+h_k)} times the load, its square is at most 4 Cgrad² 3^{2b(k+h_k)} times the load's square:

|F|² ≤ 2(|F - p|² + |p|²) ≤ 2(A + 1)|p|² ≤ 4 A |p|²      (A := Cgrad² 3^{2b(k+h_k)} ≥ 1) .

writes the middle quantity as 2(1 + ratio²) and the last step is exactly its "uses 1 ≤ 3^{b(k+h_k)} and 1 ≤ Cgrad". Stated with the amplitude t as a free real, so that no rpow enters the arithmetic.

The collar leg's per-cell bound

theorem Algsuperdiff.Section3.Provider.Multiscale.quadratic_form_le_of_slope_bounds {Φ Kp Kq A nF nG np nq : ℝ} (hform : Φ ≤ Kp * nF + Kq * nG) (hKp : 0 ≤ Kp) (hKq : 0 ≤ Kq) (hF : nF ≤ A * np) (hG : nG ≤ A * nq) : Φ ≤ A * (Kp * np + Kq * nq)

The trade of the competitor's slopes for the load, as pure real arithmetic. Φ is the cell's quadratic form, Kp/Kq the two Step-1 coefficients, nF/nG the competitor's squared slopes and np/nq the load's. This is the only step of the collar leg that is not Step 1.

theorem Algsuperdiff.Section3.Provider.Multiscale.blockVecDot_coarseBlockMatrix_collar_whitneySimplexCells_le_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) (m : ℤ) (hn : ℕ → ℕ) {i : ℤ} (hmi : m - 1 ≤ i) (hi : i ≤ m0) {b Cgrad : ℝ} (hCgrad : 1 ≤ Cgrad) (hb : 0 ≤ b) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (n : ℕ), ∀ Q ∈ Whitney.whitneyLayer m hn n, omega ∉ BadEvents.bad M Q → ∀ (L : ℤ), Q.scale ≤ L → ∀ T ∈ Whitney.whitneySimplexCells m hn n Q, ∀ (p q Fv Gv : HCPolySupport.Vec d), HCPolySupport.vecNormSq (Fv - p) ≤ Cgrad ^ 2 * 3 ^ (2 * (b * (↑n + ↑(hn n)))) * HCPolySupport.vecNormSq p → HCPolySupport.vecNormSq (Gv - q) ≤ Cgrad ^ 2 * 3 ^ (2 * (b * (↑n + ↑(hn n)))) * HCPolySupport.vecNormSq q → HCPolySupport.blockVecDot ((√↑(Annealed.sigmaBar M i))⁻¹ • Fv, √↑(Annealed.sigmaBar M i) • Gv) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix (simplexDomain T) (simplexCoeffOn (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) T)) ((√↑(Annealed.sigmaBar M i))⁻¹ • Fv, √↑(Annealed.sigmaBar M i) • Gv)) ≤ 4 * (Cgrad ^ 2 * 3 ^ (2 * (b * (↑n + ↑(hn n))))) * (640 * simplexCrudeConst d (1 / 4) * HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q (Whitney.simplexScale m hn n) (1 / 4) * (1 + 8 * BadEvents.bigLambdaSensitivityConst d * (Disorder.cstar M)⁻¹ * M.gamma * 3 ^ (-(2 * M.gamma * ↑Q.scale)) * (BadEvents.incrementUnitCube₂ Q Q.scale L omega).w1Infinity ^ 2) * HCPolySupport.vecNormSq p + 320 * simplexCrudeConst d (1 / 4) * HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q (Whitney.simplexScale m hn n) (1 / 4) * 3 ^ (M.gamma * (↑i - ↑Q.scale)) * HCPolySupport.vecNormSq q)

The collar leg of e.sum-of-a-decomp, per cell (ABK26). Almost surely, for every layer n, every good layer-n Whitney cube □, every cell 𝔰 of □ and every load (p,q) and competitor cell constants (Fv, Gv) satisfying the collar A of e.bounds.on.slopes.when.bad, the competitor's own quadratic form at 𝔰 is at most 4 Cgrad² 3^{2b(n + h_n)} times the Step-1 majorant of the load's form.

The route is the manuscript's: e.good.simplex.consequence is proved for an arbitrary load, so it applies at the competitor's load verbatim; then vecNormSq_le_four_mul_of_slope_error (the per-leg half) trades |∇ℓ̂_p|² for |p|² and |(∇·D̂_q)|² for |q|². Because the frame 𝐀hom_i^{-1/2} is block diagonal with scalar blocks (e.homs.defs.U.diag), the framed competitor (σ_i^{-1/2} Fv, σ_i^{1/2} Gv) is the frame applied to the unframed slopes and no rescaling arithmetic is needed.

The right-hand side is a constant on the cells of one cube: it depends on □ only through Q.scale and the increment gauge, and on 𝔰 not at all. Since the increment gauge varies across a layer's cubes, a per-layer supremum is still needed before this is the abstract C of Step3Seams.sum_sum_ofReal_cellWeight_le_ofReal_mul on the collar leg; the good leg absorbs the same step into its layer constant.

The two legs of e.sum-of-a-decomp, in the hlayer shape

theorem Algsuperdiff.Section3.Provider.Multiscale.sum_sum_ofReal_two_leg_le_ofReal_layerContrib {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n : ℕ} {b γ Ktot Ccol : ℝ} {hs k₀ : ℕ} {Mass Bad : ℕ → ℝ} {ggood gcol : Whitney.KuhnCell d → ℝ} {Sgood Scol : Finset (HCPolySupport.TriadicCube d)} (hSgood : Sgood ⊆ Whitney.whitneyLayer m hn n) (hScol : Scol ⊆ Whitney.whitneyLayer m hn n) (hK : 0 ≤ Ktot) (hC : 0 ≤ Ccol) (hgood : ∀ Q ∈ Sgood, ∀ T ∈ Whitney.whitneySimplexCells m hn n Q, ggood T ≤ Ktot * 3 ^ (γ * layerQuantity b hs k₀ n)) (hgoodz : ∀ Q ∈ Whitney.whitneyLayer m hn n, Q ∉ Sgood → ∀ T ∈ Whitney.whitneySimplexCells m hn n Q, ggood T = 0) (hcol : ∀ Q ∈ Scol, ∀ T ∈ Whitney.whitneySimplexCells m hn n Q, gcol T ≤ Ccol * 3 ^ (2 * b * layerQuantity b hs k₀ n)) (hcolz : ∀ Q ∈ Whitney.whitneyLayer m hn n, Q ∉ Scol → ∀ T ∈ Whitney.whitneySimplexCells m hn n Q, gcol T = 0) (hmassgood : ∑ Q ∈ Sgood, Whitney.cubeMassRatio (HCPolySupport.originCube d m) Q ≤ Mass n) (hmasscol : ∑ Q ∈ Scol, Whitney.cubeMassRatio (HCPolySupport.originCube d m) Q ≤ Bad n) : ∑ Q ∈ Whitney.whitneyLayer m hn n, ∑ T ∈ Whitney.whitneySimplexCells m hn n Q, (ENNReal.ofReal (cellWeight m T * ggood T) + ENNReal.ofReal (cellWeight m T * gcol T)) ≤ ENNReal.ofReal (layerContrib b γ hs k₀ Ktot Ccol Mass Bad n)

One Whitney layer of e.sum-of-a-decomp, majorized by ConclusionAssembly.layerContrib. The two sums of e.sum-of-a-decomp are majorized separately by Step3Seams.sum_sum_ofReal_cellWeight_le_ofReal_mul, at the two per-cell constants of layerContrib:

• good leg -- S_good the good part of the layer, C = Ktot 3^{γ(k+h_k)} (the layer reading of e.good.simplex.consequence);
• collar leg -- S_col the good part of the collar 𝒩(ℐ) of the layer, C = Ccol 3^{2b(k+h_k)} (e.bounds.on.slopes.when.bad, at the constant of blockVecDot_coarseBlockMatrix_collar_whitneySimplexCells_le_ae).

hmassgood and hmasscol are the caller's mass obligations. hmassgood is discharged by Finset.sum_le_sum_of_subset_of_nonneg against LayerMass.sum_cubeMassRatio_whitneyLayer_le. hmasscol is the caller's collar-vs-bad mass comparison; the bounded-overlap geometry behind it is NOW proved locally (Provider/Multiscale/CollarMass.lean, at the concrete collar carrier collarLayer --- a filter, not the set-difference form this note once described;), with the feasible consumer instantiation recorded there. The binder remains abstract here so the assembly composes with any admissible Bad.