Producer for the signed routed primitive slot collapse datum

SignedRoutedPrimitiveSlotCollapseData is the single routing input of the final R-324 assembly. Its proved constructors consume a family of per-pattern densities. This file eliminates the density data entirely: the datum follows from one scalar inequality per marked slot — the countable signed route weight against the integrated inserted majorant. The density is chosen as the inserted majorant itself, concentrated on the all-directFourier pattern, whose sacrifice product is 1; every pattern-adjusted domination then holds pointwise with no analytic content.

noncomputable def Anderson4D.SmoothCutoff.signedRoutedPrimitiveSlotCollapseData_of_slotInsertedBudget (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (primitiveConstant supportConstant : ℝ) (hC : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (budget : ∀ (i : Fin m), ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324SignedRouteSlotWeight lam hm ε i p ≤ ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure) : ρ.SignedRoutedPrimitiveSlotCollapseData lam ε m hm primitiveConstant supportConstant

The signed collapse datum from a single scalar budget per slot. The only remaining content of the routing input is the inequality budget: the total signed route weight of each marked slot is at most the integrated inserted majorant.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.signedRoutedPrimitiveSlotCollapseData_of_rawCaseIntegralBudget (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (primitiveConstant supportConstant : ℝ) (hC : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (budget : ∀ (i : Fin m), (∑ cases : R324EndpointReductionPattern, ∫ (v : Fin (2 * m) → T4), ρ.r324RawCaseDensity lam hm ε i cases v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) ≤ ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure) : ρ.SignedRoutedPrimitiveSlotCollapseData lam ε m hm primitiveConstant supportConstant

Physical-space form of the same producer: it suffices to bound the sixteen pattern-grouped raw case-density integrals — the genuine doubled-configuration integrals of the marked-slot series — by the integrated inserted majorant. The countable regrouping itself is the proved exact equality.

Equations

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