Paper Step 4(B): whole-series high-frequency producer

Paper: R-324 — §4.2 Step 4(B), whole-series high-frequency producer

The common-left Fourier argument is needed only when the canonical refined representative has a residual single. If both halves are full, the whole physical integral vanishes at a non-zero conserved external mode. This file records that dichotomy at the exact boundary required by the final capstone.

Keeping the residual input at the complete signed-series boundary is intentional: no selected-slot, first-high, cell, or contraction-wise triangle inequality occurs here. The analytic residual producer is supplied by the endpoint common-left Fourier identity, the grouped residual Fourier estimate, and the mixed-cutoff complete nested run imported above.

Absorbing the common-left Haar average

noncomputable def Anderson4D.SmoothCutoff.r324CommonLeftHaarAverage {I : Type u_1} {J : Type u_2} (auxiliary : (I → T4) → (J → T4) → ℝ) (left : I → T4) (right : J → T4) : ℝ

Normalized common-left Haar average of a nonnegative auxiliary coefficient. The normalization is the paper's (non-probability) torus mass.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.SmoothCutoff.r324CommonLeftHaarAverage_nonneg {I : Type u_1} {J : Type u_2} (auxiliary : (I → T4) → (J → T4) → ℝ) (hauxiliary : ∀ (left : I → T4) (right : J → T4), 0 ≤ auxiliary left right) (left : I → T4) (right : J → T4) : 0 ≤ r324CommonLeftHaarAverage auxiliary left right

theorem Anderson4D.SmoothCutoff.exists_frequencyCoordinate_two_mul_abs_ge_euclidean (mode : Z4) : ∃ (coord : Fin dim), ‖z4EuclideanFrequency mode‖ ≤ 2 * |↑(mode coord)|

One coordinate of a four-dimensional lattice mode carries at least half of its Euclidean size. The factor two is exactly sqrt 4; the selected coordinate itself is an honest maximum for the auxiliary sup norm.

theorem Anderson4D.SmoothCutoff.eps_inv_pow_eight_mul_inv_frequencyCoordinate_pow_eight_le_centralDecay {eps L a : ℝ} (heps : 0 < eps) (heps1 : eps ≤ 1) (hL : 0 ≤ L) (hcoord : L ≤ 2 * a) (hlarge : 1 ≤ eps ^ 2 * L) : eps⁻¹ ^ 8 * a⁻¹ ^ 8 ≤ 4096 * eighthOrderFrequencyDecay (eps ^ 2 * L)

At the high-frequency threshold, the inverse eighth power of a coordinate carrying half the Euclidean norm is absorbed by the paper's central bracket. The explicit constant is 2^8 * 2^4 = 4096.

theorem Anderson4D.SmoothCutoff.r324LeftInternalTranslate_coordinateDisplacement_eq_commonLeftMomentTranslation {m : ℕ} (v : Fin (2 * m) → T4) (coord : Fin dim) (t : ℝ) : (r324LeftInternalTranslateMeasurableEquiv m (r324CoordinateDisplacementT4 coord t)) v = r324CommonLeftMomentTranslation v coord t

The coordinate subgroup used by the one-dimensional Fourier estimate is literally the restriction of the canonical left-copy torus translation.

theorem Anderson4D.SmoothCutoff.r324LeftInternalTranslate_add {m : ℕ} (v : Fin (2 * m) → T4) (a b : T4) : (r324LeftInternalTranslateMeasurableEquiv m b) ((r324LeftInternalTranslateMeasurableEquiv m a) v) = (r324LeftInternalTranslateMeasurableEquiv m (a + b)) v

theorem Anderson4D.SmoothCutoff.integrable_char_mul_r324ResidualPrimitiveSumProduct_leftTranslate (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) (heps1 : eps ≤ 1) {m : ℕ} (kappaPlus kappaMinus : PartialPairing (Fin m)) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (mode : Z4) (v : Fin (2 * m) → T4) : MeasureTheory.Integrable (fun (a : T4) => charT4 mode a * ↑(r324ResidualPrimitiveSumProduct rho eps kappaPlus kappaMinus pi ((r324LeftInternalTranslateMeasurableEquiv m a) v))) paperMeasure

The complete grouped residual coefficient, translated as one signed family, is integrable against a torus character. This uses the repository's existing measurable and uniform-bound theorems for the whole residual sum; no primitive-coordinate triangle inequality is introduced here.

noncomputable def Anderson4D.SmoothCutoff.r324ResidualCommonLeftTorusCoefficient (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (kappaPlus kappaMinus : PartialPairing (Fin m)) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (mode : Z4) (v : Fin (2 * m) → T4) : ℂ

The full four-dimensional common-left Fourier coefficient of one grouped residual primitive sum.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.SmoothCutoff.integral_commonLeftCoordinateShift_eq_two_pi_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (coord : Fin dim) (f : T4 → E) (hjoint : MeasureTheory.Integrable (Function.uncurry fun (t : ℝ) (a : T4) => f (a + r324CoordinateDisplacementT4 coord t)) ((MeasureTheory.volume.restrict (Set.uIoc (-Real.pi) Real.pi)).prod paperMeasure)) : ∫ (a : T4), ∫ (t : ℝ) in -Real.pi..Real.pi, f (a + r324CoordinateDisplacementT4 coord t) ∂paperMeasure = (2 * Real.pi) • ∫ (a : T4), f a ∂paperMeasure

Averaging a function over one coordinate subgroup and over full torus Haar gives exactly 2π times its original integral. This is the Fubini normalization seam used twice below: once for the signed coefficient and once for its nonnegative auxiliary majorant.

theorem Anderson4D.SmoothCutoff.quasiMeasurePreserving_commonLeftCoordinateShift (coord : Fin dim) : MeasureTheory.Measure.QuasiMeasurePreserving (fun (q : ℝ × T4) => q.2 + r324CoordinateDisplacementT4 coord q.1) ((MeasureTheory.volume.restrict (Set.uIoc (-Real.pi) Real.pi)).prod paperMeasure) paperMeasure

The interval-parameterized coordinate shift projects quasi-preservingly to full torus Haar.

theorem Anderson4D.SmoothCutoff.integrable_commonLeftCoordinateShift_char_mul_residual (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) (heps1 : eps ≤ 1) {m : ℕ} (kappaPlus kappaMinus : PartialPairing (Fin m)) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (mode : Z4) (v : Fin (2 * m) → T4) (coord : Fin dim) : MeasureTheory.Integrable (Function.uncurry fun (t : ℝ) (a : T4) => charT4 mode (a + r324CoordinateDisplacementT4 coord t) * ↑(r324ResidualPrimitiveSumProduct rho eps kappaPlus kappaMinus pi ((r324LeftInternalTranslateMeasurableEquiv m (a + r324CoordinateDisplacementT4 coord t)) v))) ((MeasureTheory.volume.restrict (Set.uIoc (-Real.pi) Real.pi)).prod paperMeasure)

theorem Anderson4D.SmoothCutoff.integrable_r324ResidualPrimitiveSumProduct_leftTranslate (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) (heps1 : eps ≤ 1) {m : ℕ} (kappaPlus kappaMinus : PartialPairing (Fin m)) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (v : Fin (2 * m) → T4) : MeasureTheory.Integrable (fun (a : T4) => r324ResidualPrimitiveSumProduct rho eps kappaPlus kappaMinus pi ((r324LeftInternalTranslateMeasurableEquiv m a) v)) paperMeasure

theorem Anderson4D.SmoothCutoff.integrable_commonLeftCoordinateShift_residual (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) (heps1 : eps ≤ 1) {m : ℕ} (kappaPlus kappaMinus : PartialPairing (Fin m)) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (v : Fin (2 * m) → T4) (coord : Fin dim) : MeasureTheory.Integrable (Function.uncurry fun (t : ℝ) (a : T4) => r324ResidualPrimitiveSumProduct rho eps kappaPlus kappaMinus pi ((r324LeftInternalTranslateMeasurableEquiv m (a + r324CoordinateDisplacementT4 coord t)) v)) ((MeasureTheory.volume.restrict (Set.uIoc (-Real.pi) Real.pi)).prod paperMeasure)

theorem Anderson4D.SmoothCutoff.normalized_torusCoefficient_eq_integral_coordinateFourierCoeffOn (mode : Z4) (coord : Fin dim) (source : T4 → ℂ) (hjoint : MeasureTheory.Integrable (Function.uncurry fun (t : ℝ) (a : T4) => charT4 mode (a + r324CoordinateDisplacementT4 coord t) * source (a + r324CoordinateDisplacementT4 coord t)) ((MeasureTheory.volume.restrict (Set.uIoc (-Real.pi) Real.pi)).prod paperMeasure)) : (↑r324PaperTorusMass)⁻¹ * ∫ (a : T4), charT4 mode a * source a ∂paperMeasure = (↑r324PaperTorusMass)⁻¹ * ∫ (a : T4), charT4 mode a * fourierCoeffOn ⋯ (fun (t : ℝ) => source (a + r324CoordinateDisplacementT4 coord t)) (-mode coord) ∂paperMeasure

Exact partial-Fourier decomposition of the normalized full-torus coefficient. The common coordinate is averaged only after the complete signed source has been formed.

theorem Anderson4D.SmoothCutoff.r324ResidualCommonLeftTorusCoefficient_eq_integral_fourierCoeffOn (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) (heps1 : eps ≤ 1) {m : ℕ} (e0 : MomentContraction m) (mode : Z4) (v : Fin (2 * m) → T4) (coord : Fin dim) : rho.r324ResidualCommonLeftTorusCoefficient eps e0.fst e0.snd.fst e0.snd.snd mode v = (↑r324PaperTorusMass)⁻¹ * ∫ (a : T4), charT4 mode a * fourierCoeffOn ⋯ (r324ResidualPrimitiveSumCommonLeftCoordLineC rho eps e0 ((r324LeftInternalTranslateMeasurableEquiv m a) v) coord) (-mode coord) ∂paperMeasure

Concrete exact decomposition of the grouped residual torus coefficient into one-dimensional coordinate Fourier coefficients.

theorem Anderson4D.SmoothCutoff.norm_r324ResidualCommonLeftTorusCoefficient_le_auxiliaryHaarAverage (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) (heps1 : eps ≤ 1) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (mode : Z4) (v : Fin (2 * m) → T4) (coord : Fin dim) (hcoord : mode coord ≠ 0) : ‖rho.r324ResidualCommonLeftTorusCoefficient eps e0.fst e0.snd.fst e0.snd.snd mode v‖ ≤ |(↑(mode coord))⁻¹| ^ 8 * (↑m ^ 8 * r324ResidualFourierMajorantBase rho ^ (3 * m) * eps⁻¹ ^ 8) * (r324PaperTorusMass⁻¹ * ∫ (a : T4), r324ResidualPrimitiveSumProduct rho.auxiliaryCutoff eps e0.fst e0.snd.fst e0.snd.snd ((r324LeftInternalTranslateMeasurableEquiv m a) v) ∂paperMeasure)

Global grouped Step 4(B) Fourier estimate at one nonzero coordinate. The 2π in the one-dimensional Fourier coefficient cancels exactly against the coordinate-subgroup Haar average.

theorem Anderson4D.SmoothCutoff.norm_r324ResidualCommonLeftTorusCoefficient_le_centralDecay_auxiliaryHaarAverage (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) (heps1 : eps ≤ 1) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (mode : Z4) (v : Fin (2 * m) → T4) (hlarge : 1 ≤ eps ^ 2 * ‖z4EuclideanFrequency mode‖) : ‖rho.r324ResidualCommonLeftTorusCoefficient eps e0.fst e0.snd.fst e0.snd.snd mode v‖ ≤ 4096 * (↑m ^ 8 * r324ResidualFourierMajorantBase rho ^ (3 * m)) * eighthOrderFrequencyDecay (eps ^ 2 * ‖z4EuclideanFrequency mode‖) * (r324PaperTorusMass⁻¹ * ∫ (a : T4), r324ResidualPrimitiveSumProduct rho.auxiliaryCutoff eps e0.fst e0.snd.fst e0.snd.snd ((r324LeftInternalTranslateMeasurableEquiv m a) v) ∂paperMeasure)

Coordinate-free form of the grouped Step 4(B) estimate, with the explicit finite-dimensional loss absorbed into a fixed scalar.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperLeftRouteExactPackage.commonLeftFourierCoefficient_eq_residualTorusCoefficient {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {alpha beta : Z4} {p : R324RefinedScheduleIndex m} {e0 : MomentContraction m} {leftProviders : R324PaperHalfRouteProviders e0.fst alpha} {rightProviders : R324PaperHalfRouteProviders e0.snd.fst (-alpha)} {leftRoute : R324PaperHalfEndpointRoute leftProviders} {rightRoute : R324PaperHalfEndpointRoute rightProviders} (left : R324PaperLeftRouteExactPackage p e0 leftRoute beta) (right : R324PaperRightRouteExactLinearPackage left rightRoute) (leftPost : left.bound.carrier.SurvivingCoordinate → T4) (rightPost : right.package.bound.carrier.SurvivingCoordinate → T4) : r324CommonLeftFourierCoefficient (alpha + beta) (left.bound.crossCoefficient right.package.bound e0.snd.snd) leftPost rightPost = rho.r324ResidualCommonLeftTorusCoefficient eps e0.fst e0.snd.fst e0.snd.snd (alpha + beta) (r324TwoHalfRootDoubledReconstruct left.bound.carrier right.package.bound.carrier (leftPost, rightPost))

The canonical route coefficient is exactly the grouped residual torus coefficient at the doubled terminal root.

theorem Anderson4D.SmoothCutoff.integrable_geometry_mul_commonLeft_of_projection {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] (geometry auxiliary : (I → T4) → (J → T4) → ℝ) (hgeometry : ∀ (a : T4) (left : I → T4) (right : J → T4), geometry (R324WithinHalfResidualPrefix.r324CommonTranslate a left) right = geometry left right) (hprojection : MeasureTheory.Measure.QuasiMeasurePreserving (fun (q : T4 × (I → T4) × (J → T4)) => (R324WithinHalfResidualPrefix.r324CommonTranslate q.1 q.2.1, q.2.2)) (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : I) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : J) => paperMeasure))) ((MeasureTheory.Measure.pi fun (x : I) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : J) => paperMeasure))) (hbase : MeasureTheory.Integrable (fun (p : (I → T4) × (J → T4)) => geometry p.1 p.2 * auxiliary p.1 p.2) ((MeasureTheory.Measure.pi fun (x : I) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : J) => paperMeasure))) : MeasureTheory.Integrable (fun (q : T4 × (I → T4) × (J → T4)) => geometry q.2.1 q.2.2 * auxiliary (R324WithinHalfResidualPrefix.r324CommonTranslate q.1 q.2.1) q.2.2) (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : I) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : J) => paperMeasure)))

Joint integrability required by common-left Fubini follows from integrability on the terminal product carrier and quasi-measure-preservation of the common-translation projection.

theorem Anderson4D.SmoothCutoff.integral_geometry_mul_commonLeftHaarAverage_eq {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] (geometry auxiliary : (I → T4) → (J → T4) → ℝ) (hgeometry : ∀ (a : T4) (left : I → T4) (right : J → T4), geometry (R324WithinHalfResidualPrefix.r324CommonTranslate a left) right = geometry left right) (hjoint : MeasureTheory.Integrable (fun (q : T4 × (I → T4) × (J → T4)) => geometry q.2.1 q.2.2 * auxiliary (R324WithinHalfResidualPrefix.r324CommonTranslate q.1 q.2.1) q.2.2) (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : I) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : J) => paperMeasure)))) : ∫ (p : (I → T4) × (J → T4)), geometry p.1 p.2 * r324CommonLeftHaarAverage auxiliary p.1 p.2 ∂(MeasureTheory.Measure.pi fun (x : I) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : J) => paperMeasure) = ∫ (p : (I → T4) × (J → T4)), geometry p.1 p.2 * auxiliary p.1 p.2 ∂(MeasureTheory.Measure.pi fun (x : I) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : J) => paperMeasure)

Product Haar absorbs a normalized common-left average whenever the remaining endpoint geometry is invariant under the same translation. This is the positive Fubini seam between the global Fourier coefficient estimate and completeNestedRunDensityWithCrossCutoff.

No norm or triangle inequality occurs here. The only analytic premise is joint integrability before exchanging the common translation with the two terminal configuration integrals.

theorem Anderson4D.SmoothCutoff.r324EndpointErasedInvSqChainProduct_commonTranslate {rho : SmoothCutoff} {lam epsilon : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix rho lam epsilon pairing) (hactive : res.state.active.Nonempty) (v : res.SurvivingCoordinate → T4) (a : T4) : res.endpointErasedInvSqChainProduct hactive (R324WithinHalfResidualPrefix.r324CommonTranslate a v) = res.endpointErasedInvSqChainProduct hactive v

The endpoint-erased inverse-square geometry is invariant under a common translation of every surviving coordinate in one completed half.

Exact mixed-cutoff transport to the initial nested run

noncomputable def Anderson4D.R324PaperMixedEndpoint.endpointIntegratedGroupedMajorantWithCrossCutoff {rho : SmoothCutoff} {lam epsilon : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam epsilon kappaPlus kappaMinus) (sigma : SmoothCutoff) (leftScale rightScale : Fin (m + 1) → ℝ) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) : ℝ

The terminal endpoint geometry with only the complete residual covariance factor replaced by sigma. The two certified half traces, their scale products, and both endpoint-erased inverse-square chains remain those of rho, exactly as in paper Step 4(B).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Anderson4D.R324PaperMixedEndpoint.initialNestedEndpointIntegratedGroupedMajorantWithCrossCutoff {rho : SmoothCutoff} {lam epsilon : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam epsilon kappaPlus kappaMinus) (sigma : SmoothCutoff) (leftScale rightScale : Fin (m + 1) → ℝ) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (v : terminal.NestedCoordinate pi → T4) : ℝ

Pullback of the mixed-cutoff endpoint geometry to the literal initial nested-cross carrier.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.R324PaperMixedEndpoint.initialNestedEndpointIntegratedGroupedMajorantWithCrossCutoff_mul_coupling_eq {rho : SmoothCutoff} {lam epsilon : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam epsilon kappaPlus kappaMinus) (sigma : SmoothCutoff) (leftScale rightScale : Fin (m + 1) → ℝ) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (head : R324NestedCrossBlock kappaPlus kappaMinus pi) (tail : List (R324NestedCrossBlock kappaPlus kappaMinus pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaPlus kappaMinus pi).remaining = head :: tail) (v : terminal.NestedCoordinate pi → T4) : let step := r324InitialNestedCrossStepContext kappaPlus kappaMinus pi head tail hremaining; have hleftInitial := ⋯; have hrightInitial := ⋯; lamEps lam epsilon ^ (2 * step.residual.remainingOrder) * initialNestedEndpointIntegratedGroupedMajorantWithCrossCutoff terminal sigma leftScale rightScale hleft hright pi v = ((∏ edge ∈ terminal.left.activeEdgeSlots, leftScale edge) * ∏ edge ∈ terminal.right.activeEdgeSlots, rightScale edge) * invSqKerMass ^ 4 * terminal.completeNestedRunDensityWithCrossCutoff sigma step hleftInitial hrightInitial v

Exact mixed-cutoff counterpart of initialNestedEndpointIntegratedGroupedMajorant_mul_coupling_eq.

No estimate occurs here. The equality only reindexes the completed terminal pair, identifies its reconstruction with the initial nested reconstruction, and unfolds the grouped residual product with cutoff sigma.

theorem Anderson4D.R324PaperMixedEndpoint.integral_lamEps_pow_initialNestedEndpointIntegratedGroupedMajorantWithCrossCutoff_eq {rho : SmoothCutoff} {lam epsilon : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam epsilon kappaPlus kappaMinus) (sigma : SmoothCutoff) (leftScale rightScale : Fin (m + 1) → ℝ) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (head : R324NestedCrossBlock kappaPlus kappaMinus pi) (tail : List (R324NestedCrossBlock kappaPlus kappaMinus pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaPlus kappaMinus pi).remaining = head :: tail) : let step := r324InitialNestedCrossStepContext kappaPlus kappaMinus pi head tail hremaining; have hleftInitial := ⋯; have hrightInitial := ⋯; (∫ (v : terminal.NestedCoordinate pi → T4), lamEps lam epsilon ^ (2 * step.residual.remainingOrder) * initialNestedEndpointIntegratedGroupedMajorantWithCrossCutoff terminal sigma leftScale rightScale hleft hright pi v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure) = ((∏ edge ∈ terminal.left.activeEdgeSlots, leftScale edge) * ∏ edge ∈ terminal.right.activeEdgeSlots, rightScale edge) * invSqKerMass ^ 4 * ∫ (v : step.SurvivingCoordinate → T4), terminal.completeNestedRunDensityWithCrossCutoff sigma step hleftInitial hrightInitial v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure

Integrated form of the exact mixed-cutoff transport. This is the form consumed by the scalar complete-run estimate after the endpoint norm has been taken once.

theorem Anderson4D.R324PaperMixedEndpoint.integrable_initialNestedEndpointIntegratedGroupedMajorantWithCrossCutoff_at_truncation {rho : SmoothCutoff} {lam epsilon : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam epsilon kappaPlus kappaMinus) (sigma : SmoothCutoff) (leftScale rightScale : Fin (m + 1) → ℝ) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (head : R324NestedCrossBlock kappaPlus kappaMinus pi) (tail : List (R324NestedCrossBlock kappaPlus kappaMinus pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaPlus kappaMinus pi).remaining = head :: tail) (hlam : 0 < lam) (hepsilon : 0 < epsilon) (hepsilonOne : epsilon ≤ 1) (hlog : 1 ≤ |Real.log epsilon|) (hmtrunc : m ≤ truncOrder epsilon) : MeasureTheory.Integrable (initialNestedEndpointIntegratedGroupedMajorantWithCrossCutoff terminal sigma leftScale rightScale hleft hright pi) (MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure)

Integrability of the initial mixed grouped majorant. The only division is by the strictly positive even power of lamEps; all scale products remain as harmless finite constants.

theorem Anderson4D.R324PaperMixedEndpoint.integrable_endpointIntegratedGroupedMajorantWithCrossCutoff_at_truncation {rho : SmoothCutoff} {lam epsilon : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam epsilon kappaPlus kappaMinus) (sigma : SmoothCutoff) (leftScale rightScale : Fin (m + 1) → ℝ) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (head : R324NestedCrossBlock kappaPlus kappaMinus pi) (tail : List (R324NestedCrossBlock kappaPlus kappaMinus pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaPlus kappaMinus pi).remaining = head :: tail) (hlam : 0 < lam) (hepsilon : 0 < epsilon) (hepsilonOne : epsilon ≤ 1) (hlog : 1 ≤ |Real.log epsilon|) (hmtrunc : m ≤ truncOrder epsilon) : MeasureTheory.Integrable (endpointIntegratedGroupedMajorantWithCrossCutoff terminal sigma leftScale rightScale hleft hright pi) ((MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure))

The preceding integrability statement transported back to the completed two-half terminal carrier.

noncomputable def Anderson4D.R324PaperCommonLeftAverage.coefficientEndpointGeometry {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) : ℝ

The coefficient-free spatial geometry in the parametric two-half endpoint majorant.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.R324PaperCommonLeftAverage.coefficientEndpointGroupedMajorant_eq_geometry_mul_norm {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (coefficient : (left.carrier.SurvivingCoordinate → T4) → (right.carrier.SurvivingCoordinate → T4) → ℂ) (p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) : left.coefficientEndpointGroupedMajorant right coefficient p = coefficientEndpointGeometry left right p * ‖coefficient p.1 p.2‖

theorem Anderson4D.R324PaperCommonLeftAverage.coefficientEndpointGeometry_nonneg {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) : 0 ≤ coefficientEndpointGeometry left right p

theorem Anderson4D.R324PaperCommonLeftAverage.coefficientEndpointGeometry_commonTranslate_left {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (a : T4) (leftPost : left.carrier.SurvivingCoordinate → T4) (rightPost : right.carrier.SurvivingCoordinate → T4) : coefficientEndpointGeometry left right (R324WithinHalfResidualPrefix.r324CommonTranslate a leftPost, rightPost) = coefficientEndpointGeometry left right (leftPost, rightPost)

theorem Anderson4D.R324PaperCommonLeftAverage.integral_coefficientEndpointGeometry_mul_commonLeftHaarAverage_eq {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (auxiliary : (left.carrier.SurvivingCoordinate → T4) → (right.carrier.SurvivingCoordinate → T4) → ℝ) (hjoint : MeasureTheory.Integrable (fun (q : T4 × (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) => coefficientEndpointGeometry left right q.2 * auxiliary (R324WithinHalfResidualPrefix.r324CommonTranslate q.1 q.2.1) q.2.2) (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure)))) : ∫ (p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)), coefficientEndpointGeometry left right p * SmoothCutoff.r324CommonLeftHaarAverage auxiliary p.1 p.2 ∂(MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure) = ∫ (p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)), coefficientEndpointGeometry left right p * auxiliary p.1 p.2 ∂(MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure)

Specialization of the generic Haar-absorption identity to the exact coefficient-free geometry emitted by the parametric endpoint majorant.

theorem Anderson4D.R324PaperCommonLeftAverage.integrable_coefficientEndpointGeometry_mul_commonLeftHaarAverage {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (auxiliary : (left.carrier.SurvivingCoordinate → T4) → (right.carrier.SurvivingCoordinate → T4) → ℝ) (hjoint : MeasureTheory.Integrable (fun (q : T4 × (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) => coefficientEndpointGeometry left right q.2 * auxiliary (R324WithinHalfResidualPrefix.r324CommonTranslate q.1 q.2.1) q.2.2) (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure)))) : MeasureTheory.Integrable (fun (p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) => coefficientEndpointGeometry left right p * SmoothCutoff.r324CommonLeftHaarAverage auxiliary p.1 p.2) ((MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure))

Integrability companion to the preceding Haar-absorption identity. The joint T4 × terminal function is integrated first in the common-left Haar parameter; normalization by the fixed torus mass is then harmless.

theorem Anderson4D.R324PaperCommonLeftAverage.integral_initialNested_coefficientEndpointGeometry_mul_commonLeftHaarAverage_eq {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (auxiliary : (left.carrier.SurvivingCoordinate → T4) → (right.carrier.SurvivingCoordinate → T4) → ℝ) (hjoint : MeasureTheory.Integrable (fun (q : T4 × (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) => coefficientEndpointGeometry left right q.2 * auxiliary (R324WithinHalfResidualPrefix.r324CommonTranslate q.1 q.2.1) q.2.2) (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure)))) : (∫ (v : (left.twoHalfTerminal right).NestedCoordinate pi → T4), (left.twoHalfTerminal right).initialNestedPullback pi (fun (p : ((left.twoHalfTerminal right).left.SurvivingCoordinate → T4) × ((left.twoHalfTerminal right).right.SurvivingCoordinate → T4)) => ↑(coefficientEndpointGeometry left right p) * ↑(SmoothCutoff.r324CommonLeftHaarAverage auxiliary p.1 p.2)) v ∂MeasureTheory.Measure.pi fun (x : (left.twoHalfTerminal right).NestedCoordinate pi) => paperMeasure) = ∫ (v : (left.twoHalfTerminal right).NestedCoordinate pi → T4), (left.twoHalfTerminal right).initialNestedPullback pi (fun (p : ((left.twoHalfTerminal right).left.SurvivingCoordinate → T4) × ((left.twoHalfTerminal right).right.SurvivingCoordinate → T4)) => ↑(coefficientEndpointGeometry left right p) * ↑(auxiliary p.1 p.2)) v ∂MeasureTheory.Measure.pi fun (x : (left.twoHalfTerminal right).NestedCoordinate pi) => paperMeasure

The same absorption identity on the literal initial nested carrier used by the exact four-endpoint collapse and by the mixed-cutoff run.

theorem Anderson4D.R324PaperCommonLeftAverage.integrable_initialNested_coefficientEndpointGeometry_mul_commonLeftHaarAverage {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (auxiliary : (left.carrier.SurvivingCoordinate → T4) → (right.carrier.SurvivingCoordinate → T4) → ℝ) (hjoint : MeasureTheory.Integrable (fun (q : T4 × (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) => coefficientEndpointGeometry left right q.2 * auxiliary (R324WithinHalfResidualPrefix.r324CommonTranslate q.1 q.2.1) q.2.2) (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure)))) : MeasureTheory.Integrable ((left.twoHalfTerminal right).initialNestedPullback pi fun (p : ((left.twoHalfTerminal right).left.SurvivingCoordinate → T4) × ((left.twoHalfTerminal right).right.SurvivingCoordinate → T4)) => ↑(coefficientEndpointGeometry left right p) * ↑(SmoothCutoff.r324CommonLeftHaarAverage auxiliary p.1 p.2)) (MeasureTheory.Measure.pi fun (x : (left.twoHalfTerminal right).NestedCoordinate pi) => paperMeasure)

The Haar-averaged endpoint geometry is integrable on the literal initial nested carrier. This is the missing Integrable premise for the first legal post-collapse norm comparison.

theorem Anderson4D.R324PaperCommonLeftAverage.integrable_initialNested_coefficientEndpointGeometry_mul_commonLeftHaarAverage_real {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (auxiliary : (left.carrier.SurvivingCoordinate → T4) → (right.carrier.SurvivingCoordinate → T4) → ℝ) (hjoint : MeasureTheory.Integrable (fun (q : T4 × (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) => coefficientEndpointGeometry left right q.2 * auxiliary (R324WithinHalfResidualPrefix.r324CommonTranslate q.1 q.2.1) q.2.2) (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure)))) : MeasureTheory.Integrable (fun (v : (left.twoHalfTerminal right).NestedCoordinate pi → T4) => have p := ((left.twoHalfTerminal right).terminalProductPiMeasurableEquivNested pi).symm v; coefficientEndpointGeometry left right p * SmoothCutoff.r324CommonLeftHaarAverage auxiliary p.1 p.2) (MeasureTheory.Measure.pi fun (x : (left.twoHalfTerminal right).NestedCoordinate pi) => paperMeasure)

Real-valued form of the preceding integrability statement. The complex-valued initialNestedPullback is only an implementation detail of the exact endpoint-density API.

noncomputable def Anderson4D.R324PaperCommonLeftAverage.mixedResidualAuxiliary {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (sigma : SmoothCutoff) (leftPost : left.carrier.SurvivingCoordinate → T4) (rightPost : right.carrier.SurvivingCoordinate → T4) : ℝ

The complete positive auxiliary residual sum evaluated on the reconstructed terminal pair. This is the sole coefficient that changes from rho to the analytic cross cutoff sigma; the endpoint geometry is untouched.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.R324PaperCommonLeftAverage.mixedResidualAuxiliary_nonneg {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (sigma : SmoothCutoff) (leftPost : left.carrier.SurvivingCoordinate → T4) (rightPost : right.carrier.SurvivingCoordinate → T4) : 0 ≤ mixedResidualAuxiliary left right pi sigma leftPost rightPost

theorem Anderson4D.R324PaperCommonLeftAverage.mixedResidualAuxiliary_commonTranslate_left {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (sigma : SmoothCutoff) (leftPost : left.carrier.SurvivingCoordinate → T4) (rightPost : right.carrier.SurvivingCoordinate → T4) (a : T4) : mixedResidualAuxiliary left right pi sigma (R324WithinHalfResidualPrefix.r324CommonTranslate a leftPost) rightPost = r324ResidualPrimitiveSumProduct sigma epsilon kappaPlus kappaMinus pi ((r324LeftInternalTranslateMeasurableEquiv m a) (r324TwoHalfRootDoubledReconstruct left.carrier right.carrier (leftPost, rightPost)))

Translating the completed left terminal tuple is exactly the canonical left-copy translation of the doubled root, on the genuine support of the grouped residual sum.

theorem Anderson4D.R324PaperCommonLeftAverage.commonLeftHaarAverage_mixedResidualAuxiliary_eq_rootAverage {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (sigma : SmoothCutoff) (leftPost : left.carrier.SurvivingCoordinate → T4) (rightPost : right.carrier.SurvivingCoordinate → T4) : SmoothCutoff.r324CommonLeftHaarAverage (mixedResidualAuxiliary left right pi sigma) leftPost rightPost = r324PaperTorusMass⁻¹ * ∫ (a : T4), r324ResidualPrimitiveSumProduct sigma epsilon kappaPlus kappaMinus pi ((r324LeftInternalTranslateMeasurableEquiv m a) (r324TwoHalfRootDoubledReconstruct left.carrier right.carrier (leftPost, rightPost))) ∂paperMeasure

theorem Anderson4D.R324PaperCommonLeftAverage.coefficientEndpointGeometry_mul_mixedResidualAuxiliary_eq {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (sigma : SmoothCutoff) (p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) : coefficientEndpointGeometry left right p * mixedResidualAuxiliary left right pi sigma p.1 p.2 = R324PaperMixedEndpoint.endpointIntegratedGroupedMajorantWithCrossCutoff (left.twoHalfTerminal right) sigma routes.left.completedRoute.terminalScale routes.right.completedRoute.terminalScale ⋯ ⋯ pi p

On the terminal product carrier, coefficient-free endpoint geometry times the complete auxiliary residual sum is definitionally the mixed-cutoff grouped endpoint majorant (up to reassociation of scalar products).

theorem Anderson4D.R324PaperCommonLeftAverage.integrable_coefficientEndpointGeometry_mul_mixedResidual_commonLeft {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (sigma : SmoothCutoff) (head : R324NestedCrossBlock kappaPlus kappaMinus pi) (tail : List (R324NestedCrossBlock kappaPlus kappaMinus pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaPlus kappaMinus pi).remaining = head :: tail) (hlam : 0 < lam) (hepsilon : 0 < epsilon) (hepsilonOne : epsilon ≤ 1) (hlog : 1 ≤ |Real.log epsilon|) (hmtrunc : m ≤ truncOrder epsilon) : MeasureTheory.Integrable (fun (q : T4 × (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) => coefficientEndpointGeometry left right q.2 * mixedResidualAuxiliary left right pi sigma (R324WithinHalfResidualPrefix.r324CommonTranslate q.1 q.2.1) q.2.2) (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure)))

The mixed endpoint geometry supplies the joint integrability needed for the common-left Haar/Fubini step.

theorem Anderson4D.R324PaperCommonLeftAverage.integral_initialNested_geometry_mul_commonLeftAverage_eq_mixedMajorant {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (sigma : SmoothCutoff) (hjoint : MeasureTheory.Integrable (fun (q : T4 × (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) => coefficientEndpointGeometry left right q.2 * mixedResidualAuxiliary left right pi sigma (R324WithinHalfResidualPrefix.r324CommonTranslate q.1 q.2.1) q.2.2) (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure)))) : (∫ (v : (left.twoHalfTerminal right).NestedCoordinate pi → T4), (left.twoHalfTerminal right).initialNestedPullback pi (fun (p : ((left.twoHalfTerminal right).left.SurvivingCoordinate → T4) × ((left.twoHalfTerminal right).right.SurvivingCoordinate → T4)) => ↑(coefficientEndpointGeometry left right p) * ↑(SmoothCutoff.r324CommonLeftHaarAverage (mixedResidualAuxiliary left right pi sigma) p.1 p.2)) v ∂MeasureTheory.Measure.pi fun (x : (left.twoHalfTerminal right).NestedCoordinate pi) => paperMeasure) = ↑(∫ (v : (left.twoHalfTerminal right).NestedCoordinate pi → T4), R324PaperMixedEndpoint.initialNestedEndpointIntegratedGroupedMajorantWithCrossCutoff (left.twoHalfTerminal right) sigma routes.left.completedRoute.terminalScale routes.right.completedRoute.terminalScale ⋯ ⋯ pi v ∂MeasureTheory.Measure.pi fun (x : (left.twoHalfTerminal right).NestedCoordinate pi) => paperMeasure)

Common-left Haar absorption followed by the exact terminal-to-nested reindexing. The result is precisely the mixed-cutoff grouped majorant read by the Steps 2--3 complete-run identity; no pointwise comparison between the original and auxiliary cutoff is used.

theorem Anderson4D.R324PaperCommonLeftAverage.integral_initialNested_coefficientEndpointGeometry_mul_commonLeftHaarAverage_eq_real {rho : SmoothCutoff} {C lam epsilon K A : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaPlus alpha} {rightProviders : R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders kappaMinus (-alpha)} {routes : R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound routes.right.completedRoute) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (sigma : SmoothCutoff) (hjoint : MeasureTheory.Integrable (fun (q : T4 × (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) => coefficientEndpointGeometry left right q.2 * mixedResidualAuxiliary left right pi sigma (R324WithinHalfResidualPrefix.r324CommonTranslate q.1 q.2.1) q.2.2) (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure)))) : (∫ (v : (left.twoHalfTerminal right).NestedCoordinate pi → T4), have p := ((left.twoHalfTerminal right).terminalProductPiMeasurableEquivNested pi).symm v; coefficientEndpointGeometry left right p * SmoothCutoff.r324CommonLeftHaarAverage (mixedResidualAuxiliary left right pi sigma) p.1 p.2 ∂MeasureTheory.Measure.pi fun (x : (left.twoHalfTerminal right).NestedCoordinate pi) => paperMeasure) = ∫ (v : (left.twoHalfTerminal right).NestedCoordinate pi → T4), R324PaperMixedEndpoint.initialNestedEndpointIntegratedGroupedMajorantWithCrossCutoff (left.twoHalfTerminal right) sigma routes.left.completedRoute.terminalScale routes.right.completedRoute.terminalScale ⋯ ⋯ pi v ∂MeasureTheory.Measure.pi fun (x : (left.twoHalfTerminal right).NestedCoordinate pi) => paperMeasure

Real-valued common-left Haar absorption on the literal nested carrier. This is the scalar identity used after the first legal endpoint norm.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperLeftRouteExactPackage.norm_commonLeftFourierCoefficient_le_auxiliaryAverage {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {alpha beta : Z4} {p : R324RefinedScheduleIndex m} {e0 : MomentContraction m} {leftProviders : R324PaperHalfRouteProviders e0.fst alpha} {rightProviders : R324PaperHalfRouteProviders e0.snd.fst (-alpha)} {leftRoute : R324PaperHalfEndpointRoute leftProviders} {rightRoute : R324PaperHalfEndpointRoute rightProviders} (left : R324PaperLeftRouteExactPackage p e0 leftRoute beta) (right : R324PaperRightRouteExactLinearPackage left rightRoute) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (heps : 0 < eps) (heps1 : eps ≤ 1) (hlarge : 1 ≤ eps ^ 2 * ‖z4EuclideanFrequency (alpha + beta)‖) (leftPost : left.bound.carrier.SurvivingCoordinate → T4) (rightPost : right.package.bound.carrier.SurvivingCoordinate → T4) : ‖r324CommonLeftFourierCoefficient (alpha + beta) (left.bound.crossCoefficient right.package.bound e0.snd.snd) leftPost rightPost‖ ≤ 4096 * (↑m ^ 8 * r324ResidualFourierMajorantBase rho ^ (3 * m)) * eighthOrderFrequencyDecay (eps ^ 2 * ‖z4EuclideanFrequency (alpha + beta)‖) * SmoothCutoff.r324CommonLeftHaarAverage (R324PaperCommonLeftAverage.mixedResidualAuxiliary left.bound right.package.bound e0.snd.snd rho.auxiliaryCutoff) leftPost rightPost

Pointwise coefficient estimate on the actual completed route packages. This is the exact input expected by the coefficient-parametric endpoint majorant.

Minimal signed endpoint/Fourier certificate

Uniform absorption of the grouped Fourier loss

noncomputable def Anderson4D.SmoothCutoff.r324CommonLeftFourierAbsorptionBase (rho : SmoothCutoff) : ℝ

Fixed base which absorbs the endpoint mass normalization, the explicit 4096, the eighth-degree order loss, and the three copies per order of the cutoff derivative majorant.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.SmoothCutoff.one_le_r324CommonLeftFourierAbsorptionBase (rho : SmoothCutoff) : 1 ≤ rho.r324CommonLeftFourierAbsorptionBase

theorem Anderson4D.SmoothCutoff.r324CommonLeftFourierLoss_le_absorptionBase_pow (rho : SmoothCutoff) {m : ℕ} (hm : 1 ≤ m) : 4096 * R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.twoHalfEndpointMassCompensation * (↑m ^ 8 * r324ResidualFourierMajorantBase rho ^ (3 * m)) ≤ rho.r324CommonLeftFourierAbsorptionBase ^ (2 * m)

The whole grouped Fourier loss is exponential in the ambient order and therefore fits into the 2m power already present in the inserted primitive majorant.

structure Anderson4D.SmoothCutoff.R324PaperResidualCommonLeftEndpointCertificate (X : Type u_1) [MeasurableSpace X] (rho : SmoothCutoff) (primitiveConstant supportConstant epsilon : ℝ) (m : ℕ) (alpha beta : Z4) (p : R324RefinedScheduleIndex m) : Type u_1

Optional abstract certificate for the exact downstream information produced by the common-left endpoint calculation for one residual schedule.

This interface is useful for independent consumers, but it is not an assumption of the final proof chain: the unconditional producer below constructs the physical estimate directly.

canonicalCommonLeftIdentity is the signed Haar/Fubini identity and occurs before any norm. commonLeftCoefficient_le_auxiliary is the grouped Fourier-to-auxiliary estimate. The coefficient-parametric endpoint theorem then gives the first legal endpoint-density norm, and its weighted integral is discharged by the mixed-cutoff complete nested run.

• leftOrder : ℕ
• rightOrder : ℕ
• crossOrder : ℕ
• order_eq : self.leftOrder + self.rightOrder + self.crossOrder = m
• measure : MeasureTheory.Measure X
• endpointDensityWithCoefficient : (X → ℂ) → X → ℂ
• originalCoefficient : X → ℂ
• commonLeftCoefficient : X → ℂ
• auxiliaryCoefficientMajorant : X → ℝ
• mixedCutoffMajorant : X → ℝ
• exactEndpointCollapse : ↑(lamEps 1 epsilon) ^ (2 * (self.leftOrder + self.rightOrder)) * r324RefinedPhysicalIntegral rho epsilon m alpha beta p = ∫ (x : X), self.endpointDensityWithCoefficient self.originalCoefficient x ∂self.measure
• canonicalCommonLeftIdentity : ∫ (x : X), self.endpointDensityWithCoefficient self.originalCoefficient x ∂self.measure = ∫ (x : X), self.endpointDensityWithCoefficient self.commonLeftCoefficient x ∂self.measure
• commonLeftCoefficient_le_auxiliary : (fun (x : X) => ‖self.commonLeftCoefficient x‖) ≤ᵐ[self.measure] self.auxiliaryCoefficientMajorant
• coefficientParametricEndpointDensity_le_mixedCutoffMajorant : (fun (x : X) => ‖self.commonLeftCoefficient x‖) ≤ᵐ[self.measure] self.auxiliaryCoefficientMajorant → (fun (x : X) => ‖self.endpointDensityWithCoefficient self.commonLeftCoefficient x‖) ≤ᵐ[self.measure] self.mixedCutoffMajorant
• weightedMixedCutoffMajorant_integrable : MeasureTheory.Integrable (fun (x : X) => lamEps 1 epsilon ^ (2 * self.crossOrder) * self.mixedCutoffMajorant x) self.measure
• weightedMixedCutoffMajorant_integral_le : ∫ (x : X), lamEps 1 epsilon ^ (2 * self.crossOrder) * self.mixedCutoffMajorant x ∂self.measure ≤ paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * eighthOrderFrequencyDecay (epsilon ^ 2 * ‖z4EuclideanFrequency (alpha + beta)‖) * (epsilon⁻¹ ^ 8 * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant 1 epsilon supportConstant m z ∂paperMeasure)

def Anderson4D.SmoothCutoff.R324PaperResidualCommonLeftEndpointInput (rho : SmoothCutoff) (primitiveConstant supportConstant : ℝ) : Prop

Optional schedule-uniform certificate interface. A concrete instance would combine canonical endpoint averaging, the grouped residual Fourier-to-auxiliary estimate, and the mixed-cutoff run. The final unconditional route does not consume this interface as a hypothesis.

Equations

• One or more equations did not get rendered due to their size.

The concrete certificate is assembled after choosing the canonical routes as follows.

• X is the literal initial nested-coordinate function space of left.bound.twoHalfTerminal right.bound, with product paper measure.
• endpointDensityWithCoefficient is nestedEndpointProductDensityWithCoefficient after pulling a two-terminal coefficient back along terminalProductPiMeasurableEquivNested.
• originalCoefficient is left.bound.crossCoefficient right.bound pi; commonLeftCoefficient is its r324CommonLeftFourierCoefficient at alpha + beta. The canonical route package supplies the signed integral identity before the first norm.
• auxiliaryCoefficientMajorant is the common-left Haar average of r324ResidualPrimitiveSumProduct rho.auxiliaryCutoff. The grouped global Fourier theorem supplies its pointwise coefficient bound, including the eighth-order central decay and the absorbable m^8 C^(3m) loss.
• mixedCutoffMajorant is the coefficient-parametric endpoint majorant with that auxiliary coefficient. Common-translation invariance of product Haar turns its integral into completeNestedRunDensityWithCrossCutoff; the mixed complete-run theorem and the existing reachable-scale ledger then supply the final weighted integral field.

Thus the certificate has no selected-slot, cell, word, or contraction-local norm, and its fields correspond one-for-one to the paper's endpoint collapse, common translation, derivative estimate, and Steps 2--3 nested run.

def Anderson4D.SmoothCutoff.R324PaperResidualHighPhysicalWeightedMajorantBound (rho : SmoothCutoff) (primitiveConstant supportConstant : ℝ) : Prop

The analytic residual target in the physical-integral normalization used by the exact two-half endpoint packages. This is the convenient output of the common-left Fourier / mixed-cutoff nested-run proof.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.SmoothCutoff.exists_r324PaperResidualHighPhysicalWeightedMajorantBound (rho : SmoothCutoff) : ∃ (primitiveConstant : ℝ) (supportConstant : ℝ), 0 < primitiveConstant ∧ 0 < supportConstant ∧ rho.R324PaperResidualHighPhysicalWeightedMajorantBound primitiveConstant supportConstant

Unconditional Step 4(B) producer in the physical normalization. This is a whole-series implementation of the paper's high-frequency gain: complete both signed endpoint routes, apply the common-left Fourier identity before taking a norm, use the coefficient-parametric endpoint majorant once, Haar-average the complete residual family, and finally run the already closed Steps 2--3 majorant. It is mathematically equivalent at the public estimate boundary, but is not the paper's literal single-high-slot presentation.

theorem Anderson4D.SmoothCutoff.R324PaperResidualCommonLeftEndpointInput.toPhysical {rho : SmoothCutoff} {primitiveConstant supportConstant : ℝ} (hinput : rho.R324PaperResidualCommonLeftEndpointInput primitiveConstant supportConstant) : rho.R324PaperResidualHighPhysicalWeightedMajorantBound primitiveConstant supportConstant

The optional abstract signed endpoint/Fourier certificate suffices to close the residual physical estimate. This adapter is not on the final unconditional proof path.

def Anderson4D.SmoothCutoff.R324PaperResidualHighWholeSeriesWeightedMajorantBound (rho : SmoothCutoff) (primitiveConstant supportConstant : ℝ) : Prop

The genuinely residual part of paper Step 4(B), still at the complete signed open-series boundary. This is the precise target of the common-left Fourier calculation; the full/full branch is discharged structurally below.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.SmoothCutoff.R324PaperResidualHighPhysicalWeightedMajorantBound.toOpenSeries {rho : SmoothCutoff} {primitiveConstant supportConstant : ℝ} (hphysical : rho.R324PaperResidualHighPhysicalWeightedMajorantBound primitiveConstant supportConstant) : rho.R324PaperResidualHighWholeSeriesWeightedMajorantBound primitiveConstant supportConstant

Exact covariance reassembly transports a physical-integral estimate to the complete signed open series without any triangle inequality.

theorem Anderson4D.SmoothCutoff.R324PaperResidualHighWholeSeriesWeightedMajorantBound.toHighWholeSeries {rho : SmoothCutoff} {primitiveConstant supportConstant : ℝ} (hprimitive : 0 ≤ primitiveConstant) (hresidual : rho.R324PaperResidualHighWholeSeriesWeightedMajorantBound primitiveConstant supportConstant) : rho.R324PaperHighWholeSeriesWeightedMajorantBound primitiveConstant supportConstant

Adding the structurally vanishing full/full branch turns the residual common-left estimate into the public complete-series Step 4(B) producer.

theorem Anderson4D.SmoothCutoff.exists_r324PaperHighWholeSeriesWeightedMajorantBound_of_residual (rho : SmoothCutoff) (hresidual : ∃ (primitiveConstant : ℝ) (supportConstant : ℝ), 0 < primitiveConstant ∧ 0 < supportConstant ∧ rho.R324PaperResidualHighWholeSeriesWeightedMajorantBound primitiveConstant supportConstant) : ∃ (primitiveConstant : ℝ) (supportConstant : ℝ), 0 < primitiveConstant ∧ 0 < supportConstant ∧ rho.R324PaperHighWholeSeriesWeightedMajorantBound primitiveConstant supportConstant

Existential adapter from the residual common-left Fourier estimate to the final assembly.

theorem Anderson4D.SmoothCutoff.exists_r324PaperHighWholeSeriesWeightedMajorantBound_of_physical (rho : SmoothCutoff) (hphysical : ∃ (primitiveConstant : ℝ) (supportConstant : ℝ), 0 < primitiveConstant ∧ 0 < supportConstant ∧ rho.R324PaperResidualHighPhysicalWeightedMajorantBound primitiveConstant supportConstant) : ∃ (primitiveConstant : ℝ) (supportConstant : ℝ), 0 < primitiveConstant ∧ 0 < supportConstant ∧ rho.R324PaperHighWholeSeriesWeightedMajorantBound primitiveConstant supportConstant

One-step adapter from the exact endpoint/Fourier proof's physical normalization to the public complete signed-series producer.

theorem Anderson4D.SmoothCutoff.exists_r324PaperHighWholeSeriesWeightedMajorantBound (rho : SmoothCutoff) : ∃ (primitiveConstant : ℝ) (supportConstant : ℝ), 0 < primitiveConstant ∧ 0 < supportConstant ∧ rho.R324PaperHighWholeSeriesWeightedMajorantBound primitiveConstant supportConstant

Unconditional paper Step 4(B) producer consumed by the final assembly.

theorem Anderson4D.SmoothCutoff.exists_r324PaperHighWholeSeriesWeightedMajorantBound_of_commonLeftInput (rho : SmoothCutoff) (hinput : ∃ (primitiveConstant : ℝ) (supportConstant : ℝ), 0 < primitiveConstant ∧ 0 < supportConstant ∧ rho.R324PaperResidualCommonLeftEndpointInput primitiveConstant supportConstant) : ∃ (primitiveConstant : ℝ) (supportConstant : ℝ), 0 < primitiveConstant ∧ 0 < supportConstant ∧ rho.R324PaperHighWholeSeriesWeightedMajorantBound primitiveConstant supportConstant

Optional abstract assembly: a uniform common-left endpoint certificate also implies the public Step 4(B) producer. The stable final theorem above instead uses the unconditional physical producer directly.