Cancellation-preserving grouped route weights for R-324

The exact refined Fourier expansion groups a complete compatible primitive fibre before taking a norm. This module attaches the reciprocal eighth-order cost to that grouped object, after the four endpoint integrations and before the final countable central-frequency routing.

The endpoint-free budget below contains only integrability and summability of the grouped internal core masses. In particular, it does not assume the final moment estimate.

Reciprocal decay cost of one common-increment group

noncomputable def Anderson4D.SmoothCutoff.r324GroupedIncrementCost {m : ℕ} (hm : 0 < m) (b : ℕ) (i : Fin m) : ℝ

Reciprocal eighth-order cost of one concrete grouped increment.

Unlike r324PairDecayCost, this cost is attached directly to the common increment key of the whole refined group; there is no remaining raw full-pairing index.

Equations

• Anderson4D.SmoothCutoff.r324GroupedIncrementCost hm b i = (1 + ‖Anderson4D.z4EuclideanFrequency ((Anderson4D.SmoothCutoff.r324NatEquivStandardConfigurations hm) b i)‖ ^ 2) ^ 4

theorem Anderson4D.SmoothCutoff.r324GroupedIncrementCost_pos {m : ℕ} (hm : 0 < m) (b : ℕ) (i : Fin m) : 0 < r324GroupedIncrementCost hm b i

theorem Anderson4D.SmoothCutoff.r324GroupedIncrementCost_mul_decay {m : ℕ} (hm : 0 < m) (b : ℕ) (i : Fin m) : r324GroupedIncrementCost hm b i * eighthOrderFrequencyDecay ‖z4EuclideanFrequency ((r324NatEquivStandardConfigurations hm) b i)‖ = 1

The grouped cost is exactly the reciprocal of the routed decay.

Endpoint-free grouped base weights

noncomputable def Anderson4D.SmoothCutoff.r324GroupedRefinedCoreL1 (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m × ℕ) : ℝ

Internal L¹ mass of one common-increment refined group.

The complete compatible primitive fibre has already been summed in r324KeyGroupedRefinedEndpointCore; only then is the norm taken and integrated over the doubled internal tuple.

Equations

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

theorem Anderson4D.SmoothCutoff.r324GroupedRefinedCoreL1_nonneg (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m × ℕ) : 0 ≤ ρ.r324GroupedRefinedCoreL1 hm ε p

noncomputable def Anderson4D.SmoothCutoff.r324GroupedRouteBaseWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m × ℕ) : ℝ

Endpoint-free route weight of one grouped configuration.

It consists of the common coupling factor, the integrated norm of the already-grouped primitive fibre, and one sum of reciprocal routed costs. No external Fourier mode or endpoint loss occurs in this definition.

Equations

• ρ.r324GroupedRouteBaseWeight lam hm ε p = |Anderson4D.lamEps lam ε| ^ (2 * m) * ρ.r324GroupedRefinedCoreL1 hm ε p * ∑ i : Fin m, Anderson4D.SmoothCutoff.r324GroupedIncrementCost hm p.2 i

theorem Anderson4D.SmoothCutoff.r324GroupedRouteBaseWeight_nonneg (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m × ℕ) : 0 ≤ ρ.r324GroupedRouteBaseWeight lam hm ε p

Removing the apparent second endpoint sacrifice

theorem Anderson4D.SmoothCutoff.norm_integral_r324EndpointSeparatedIntegrand_le_endpointLoss {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) (core : ℂ) : ‖∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), r324EndpointSeparatedIntegrand α β anchors flags core x y z w ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure‖ ≤ 16 * r324EndpointLoss ε α β * ‖core‖

The sacrificed endpoint estimate implies the same bound without an extra ε⁻⁸ on the left when 0 < ε ≤ 1.

Thus the single r324EndpointLoss on the right is the only endpoint scale loss passed to the routing layer.

Local grouped routed estimate

theorem Anderson4D.SmoothCutoff.norm_r324GroupedEndpointConfigurationTerm_le_groupedRouteBaseWeight_mul_decay (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) (p : R324RefinedScheduleIndex m × ℕ) (hcore : MeasureTheory.Integrable (fun (v : Fin (2 * m) → T4) => ‖ρ.r324KeyGroupedRefinedEndpointCore hm ε p.1 p.2 v‖) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)) (i : Fin m) : ‖r324GroupedEndpointConfigurationTerm hm ρ lam ε α β (r324RefinedScheduleRepresentative p.1) (ρ.r324KeyGroupedRefinedEndpointCore hm ε p.1 p.2)‖ ≤ 16 * r324EndpointLoss ε α β * ρ.r324GroupedRouteBaseWeight lam hm ε p * eighthOrderFrequencyDecay ‖ρ.r324ConcreteRefinedIncrement lam hm ε α β p i‖

A complete grouped core with integrable internal norm obeys the local eighth-order routed estimate required by the countable central-frequency constructor.

The zero-term branch is discharged before inspecting the artificial frequency-conserving delta route.

Endpoint-free integrated primitive-collapse budget

structure Anderson4D.SmoothCutoff.IntegratedPrimitiveCollapseBudget (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (hm : 0 < m) (amplitude : ℝ) : Prop

Output expected from the integrated primitive-collapse phase.

It certifies integrability and a summable total budget for the norms of the already-grouped internal cores. The endpoint loss, the external modes, and the final moment estimate are absent from this interface.

• integrable_groupedCore (p : R324RefinedScheduleIndex m × ℕ) : MeasureTheory.Integrable (fun (v : Fin (2 * m) → T4) => ‖ρ.r324KeyGroupedRefinedEndpointCore hm ε p.1 p.2 v‖) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)
• summable_baseWeight : Summable (ρ.r324GroupedRouteBaseWeight lam hm ε)
• tsum_baseWeight_le : ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324GroupedRouteBaseWeight lam hm ε p ≤ amplitude

theorem Anderson4D.SmoothCutoff.countableCentralRoutedMomentReductionOutput_of_integratedPrimitiveCollapseBudget (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (α β : Z4) (amplitude : ℝ) (budget : ρ.IntegratedPrimitiveCollapseBudget lam ε m hm amplitude) : CountableCentralRoutedMomentReductionOutput ρ lam ε m α β (16 * amplitude * r324EndpointLoss ε α β)

The concrete exact expansion and an endpoint-free integrated primitive-collapse budget produce the routed output used by the final central-frequency estimate.