SuperposedFluxUpperPerDescendant

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

Per-descendant upper split for the superposed flux

This module constructs the twelve analytic lanes controlling the coarse upper block on a single descendant cube. It packages them into a deterministic contribution, an ordinary Gamma_1 contribution, and an exceptional contribution.

The public result superposedFlux_upper_per_descendant_split deliberately stops before the depth and exponent aggregation. Its exceptional scale remains in the raw form produced by the twelve-lane construction.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFlux_upper_per_descendant_split {d : ℕ} (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }) (hstate : Frozen.Section3.inductionState M (m - 1) E) (sigma Clane : ℝ) (hsigma0 : 0 < sigma) (hsigmaHalf : sigma ≤ 1 / 2) (hmaxLane : max (Real.exp (Clane / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hE2 : ↑E ≤ M.gamma ^ (-(1 / 5))) (hlanePos : 0 < Clane) (hgoodBaseOutput : Multiscale.probeSharpGoodBaseConst d ≤ Clane) (hgoodHeadOutput : goodHeadTunedOutputConst d ≤ Clane) (hgoodBandOutput : probeSharpBandMeanTunedOutputConst d ≤ Clane) (hgoodDeepOutput : probeSharpDeepBandTailTunedOutputConst d ≤ Clane) (hgoodAfterOutput : probeSharpAfterBandTunedOutputConst d ≤ Clane) (hgoodWaveOutput : probeSharpWaveTailTunedOutputConst d ≤ Clane) (hcollarBaseOutput : probeSharpCollarBaseTunedOutputConst d ≤ Clane) (hcollarHeadOutput : collarHeadTunedPerDescendantOutputConst d ≤ Clane) (hcollarBandOutput : collarBandMeanTunedOutputConst d ≤ Clane) (hcollarDeepOutput : collarDeepTailTunedOutputConst d ≤ Clane) (hcollarAfterOutput : collarAfterBandTunedOutputConst d ≤ Clane) (hcollarWaveOutput : probeSharpCollarWaveTailTunedOutputConst d ≤ Clane) (hprofileAuxLane : profileAuxiliaryConst d ≤ Clane) (hdepthThresholdLane : collarBandMeanDepthThreshold d ≤ Clane) (hk0 : 3 ≤ collarBandMeanDepth M ↑E) : have Cblock := (12 + 12 * HCPolySupport.IndependentSums.gammaTriangleConst 1) * Clane; ∀ (k : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k), ∃ (Uone : Cutoff.CutoffSample d → ℝ) (Uexp : Cutoff.CutoffSample d → ℝ), (∀ (omega : Cutoff.CutoffSample d), 0 ≤ Uone omega) ∧ Measurable Uone ∧ (∀ (omega : Cutoff.CutoffSample d), 0 ≤ Uexp omega) ∧ Measurable Uexp ∧ (∀ (omega : Cutoff.CutoffSample d), cutoffBBlockFamily M m (↑(Annealed.sigmaBar M (m - 1)))⁻¹ R omega ≤ Cblock + Uone omega + Uexp omega) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) Uone (upperSaturatedPerCubeAmplitude Cblock (Disorder.cstar M) M.gamma k) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) Uexp (12 * upperAfterBandRareTriangleConst * (3 ^ (M.gamma * (↑k + 1)) * Real.exp (-(Clane⁻¹ * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹))) ^ 8))

Constructs the pointwise deterministic, ordinary, and exceptional split for every single descendant cube. The exceptional scale is left in its raw twelve-lane form for the upper-leg aggregation layer to normalize.