Exact endpoint-case grouping of the raw signed R-324 slot series

The raw marked-slot series lives on the full doubled internal configuration space. This file groups that series by the actual four-endpoint reduction pattern before any phase-A physical-space estimate is applied.

The later phase-A bridge is represented separately: it pushes each raw case density to a density in one surviving relative endpoint variable. Thus the target primitive majorant does not occur in the definition of the raw density.

A reusable L¹ summation lemma

Raw case densities on the full internal configuration space

noncomputable def Anderson4D.SmoothCutoff.r324RawCaseDensityTerm (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (i : Fin m) (cases : R324EndpointReductionPattern) (p : R324RefinedScheduleIndex m × ℕ) (v : Fin (2 * m) → T4) : ℝ

One raw grouped schedule term, retained exactly when its actual four endpoint cases agree with cases.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324RawCaseDensity (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (i : Fin m) (cases : R324EndpointReductionPattern) (v : Fin (2 * m) → T4) : ℝ

The exact raw density of one endpoint-case fibre. Its domain is the full doubled internal configuration space, not the final relative endpoint torus.

Equations

• ρ.r324RawCaseDensity lam hm ε i cases v = ∑' (p : Anderson4D.R324RefinedScheduleIndex m × ℕ), ρ.r324RawCaseDensityTerm lam hm ε i cases p v

theorem Anderson4D.SmoothCutoff.r324RawCaseDensityTerm_nonneg (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (i : Fin m) (cases : R324EndpointReductionPattern) (p : R324RefinedScheduleIndex m × ℕ) (v : Fin (2 * m) → T4) : 0 ≤ ρ.r324RawCaseDensityTerm lam hm ε i cases p v

theorem Anderson4D.SmoothCutoff.integrable_r324RawCaseDensityTerm (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (i : Fin m) (cases : R324EndpointReductionPattern) (p : R324RefinedScheduleIndex m × ℕ) : MeasureTheory.Integrable (ρ.r324RawCaseDensityTerm lam hm ε i cases p) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)

theorem Anderson4D.SmoothCutoff.integral_r324RawCaseDensityTerm (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (i : Fin m) (cases : R324EndpointReductionPattern) (p : R324RefinedScheduleIndex m × ℕ) : (∫ (v : Fin (2 * m) → T4), ρ.r324RawCaseDensityTerm lam hm ε i cases p v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) = if r324RefinedEndpointReductionCase p.1 = cases then ρ.r324SignedRouteSlotWeight lam hm ε i p else 0

theorem Anderson4D.SmoothCutoff.integral_norm_r324RawCaseDensityTerm (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (i : Fin m) (cases : R324EndpointReductionPattern) (p : R324RefinedScheduleIndex m × ℕ) : (∫ (v : Fin (2 * m) → T4), ‖ρ.r324RawCaseDensityTerm lam hm ε i cases p v‖ ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) = if r324RefinedEndpointReductionCase p.1 = cases then ρ.r324SignedRouteSlotWeight lam hm ε i p else 0

theorem Anderson4D.SmoothCutoff.summable_r324RawCaseSelectedSlotWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (i : Fin m) (cases : R324EndpointReductionPattern) : Summable fun (p : R324RefinedScheduleIndex m × ℕ) => if r324RefinedEndpointReductionCase p.1 = cases then ρ.r324SignedRouteSlotWeight lam hm ε i p else 0

The subseries selected by one endpoint pattern is summable.

theorem Anderson4D.SmoothCutoff.summable_integral_norm_r324RawCaseDensityTerm (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (i : Fin m) (cases : R324EndpointReductionPattern) : Summable fun (p : R324RefinedScheduleIndex m × ℕ) => ∫ (v : Fin (2 * m) → T4), ‖ρ.r324RawCaseDensityTerm lam hm ε i cases p v‖ ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

theorem Anderson4D.SmoothCutoff.integrable_r324RawCaseDensity (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (i : Fin m) (cases : R324EndpointReductionPattern) : MeasureTheory.Integrable (ρ.r324RawCaseDensity lam hm ε i cases) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)

Every exact case density is integrable.

theorem Anderson4D.SmoothCutoff.integral_r324RawCaseDensity (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (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) = ∑' (p : R324RefinedScheduleIndex m × ℕ), if r324RefinedEndpointReductionCase p.1 = cases then ρ.r324SignedRouteSlotWeight lam hm ε i p else 0

Integrating one raw case density gives exactly the corresponding subseries of marked-slot weights.

theorem Anderson4D.SmoothCutoff.tsum_r324SignedRouteSlotWeight_eq_sum_integral_rawCaseDensity (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (i : Fin m) : ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324SignedRouteSlotWeight lam hm ε i p = ∑ cases : R324EndpointReductionPattern, ∫ (v : Fin (2 * m) → T4), ρ.r324RawCaseDensity lam hm ε i cases v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

Exact regrouping of the complete raw marked-slot series by the actual four-endpoint reduction pattern.

Non-circular interface to the physical phase-A collapse

structure Anderson4D.SmoothCutoff.R324RawCaseDensityPhaseAOutput (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (hm : 0 < m) (primitiveConstant supportConstant : ℝ) : Type

Output required from the genuine phase-A physical-space reduction.

For each marked slot and actual endpoint pattern, the bridge pushes the full doubled-configuration density above to a density in one surviving relative endpoint variable. Its integral comparison is stated case-by-case; no total routed budget or downstream slot tsum estimate is a field of this structure.

• reducedDensity : Fin m → R324EndpointReductionPattern → T4 → ℝ
• reducedDensity_integrable (i : Fin m) (cases : R324EndpointReductionPattern) : MeasureTheory.Integrable (self.reducedDensity i cases) paperMeasure
• raw_case_integral_le_reduced_integral (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), self.reducedDensity i cases z ∂paperMeasure
• pointwise_reduced_le_caseAdjustedMajorant (i : Fin m) (cases : R324EndpointReductionPattern) (z : T4) : self.reducedDensity i cases z ≤ r324EndpointPatternAdjustedPrimitiveMajorant ε cases primitiveConstant lam supportConstant m z

def Anderson4D.SmoothCutoff.signedRoutedPrimitiveSlotCollapseData_of_rawCaseDensityPhaseAOutput (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (primitiveConstant supportConstant : ℝ) (phaseA : ρ.R324RawCaseDensityPhaseAOutput lam ε m hm primitiveConstant supportConstant) : ρ.SignedRoutedPrimitiveSlotCollapseData lam ε m hm primitiveConstant supportConstant

Exact case regrouping plus a genuine phase-A output produces the normalized collapse datum consumed by the routed endpoint budget.

The only inequality before the proved constructor is the case-by-case full-configuration-to-relative-endpoint comparison stored in phaseA; countable regrouping itself remains an equality.

Equations

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