Summable routed weights for one R-324 full pairing

For one full doubled pairing, every Fourier configuration has exactly m signed covariance-mode increments. This file attaches to the configuration its physical L¹ norm times the sum of the inverse eighth-order decays of those increments. Only one covariance slot is polynomially weighted at a time, so the construction pays one degree-eight cutoff loss rather than an incorrect product of m such losses.

Zero integrated configurations are harmless analytically, but the downstream routing structure asks for exact frequency conservation for every enumerated term. Their increments are therefore replaced by one external increment followed by zeros.

Polynomial control of one routed increment

noncomputable def Anderson4D.SmoothCutoff.r324PairDecayCost {m : ℕ} (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) (i : Fin m) : ℝ

The exact reciprocal cost of one eighth-order routed decay.

Equations

• Anderson4D.SmoothCutoff.r324PairDecayCost κ q i = (1 + ‖Anderson4D.SmoothCutoff.r324StandardPairIncrement κ q i‖ ^ 2) ^ 4

theorem Anderson4D.SmoothCutoff.r324PairDecayCost_pos {m : ℕ} (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) (i : Fin m) : 0 < r324PairDecayCost κ q i

theorem Anderson4D.SmoothCutoff.r324PairDecayCost_mul_decay {m : ℕ} (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) (i : Fin m) : r324PairDecayCost κ q i * eighthOrderFrequencyDecay ‖r324StandardPairIncrement κ q i‖ = 1

theorem Anderson4D.SmoothCutoff.norm_r324StandardPairIncrement_le_mode {m : ℕ} (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) (i : Fin m) : ‖r324StandardPairIncrement κ q i‖ ≤ ‖z4EuclideanFrequency (q i)‖

A signed left-copy contribution is either q i, -q i, or zero.

theorem Anderson4D.SmoothCutoff.norm_z4EuclideanFrequency_le_two_mul_latticeBase (k : Z4) : ‖z4EuclideanFrequency k‖ ≤ 2 * ∑ i : Fin dim, (↑(k i).natAbs + 1)

The raw Euclidean lattice norm is controlled by twice the coordinatewise polynomial base.

theorem Anderson4D.SmoothCutoff.r324PairDecayCost_le_latticePolynomialWeight {m : ℕ} (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) (i : Fin m) : r324PairDecayCost κ q i ≤ 625 * latticePolynomialWeight 8 (q i)

One reciprocal routed decay is bounded by a fixed multiple of the degree-eight lattice weight of the corresponding covariance mode.

A single polynomially weighted covariance slot

theorem Anderson4D.SmoothCutoff.summable_latticePolynomialWeight_mul_norm_covarianceModeCoeff (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : Summable fun (k : Z4) => latticePolynomialWeight 8 k * ‖ρ.covarianceModeCoeff ε k‖

The covariance coefficient remains summable after one degree-eight lattice weight is inserted.

theorem Anderson4D.SmoothCutoff.summable_standardConfigurationWeight_mul_latticePolynomialWeight (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (i : Fin m) : Summable fun (q : Fin m → Z4) => ρ.r324CovarianceConfigurationWeight ε (↑κ) (r324FullConfigurationOfStandard κ q) * latticePolynomialWeight 8 (q i)

After standardizing the pair enumeration, weighting any one covariance slot by a degree-eight lattice polynomial preserves summability of the full configuration product.

theorem Anderson4D.SmoothCutoff.summable_standardConfigurationWeight_mul_pairDecayCost (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (i : Fin m) : Summable fun (q : Fin m → Z4) => ρ.r324CovarianceConfigurationWeight ε (↑κ) (r324FullConfigurationOfStandard κ q) * r324PairDecayCost κ q i

Physical L¹ weight and natural enumeration

noncomputable def Anderson4D.SmoothCutoff.r324BareSkeletonL1 {m : ℕ} (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) : ℝ

The bare two-skeleton L¹ mass of one full doubled pairing.

Equations

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

theorem Anderson4D.SmoothCutoff.r324BareSkeletonL1_nonneg {m : ℕ} (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) : 0 ≤ r324BareSkeletonL1 κ

theorem Anderson4D.SmoothCutoff.integral_norm_r324FullPairingFourierIntegrand (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin {i ∈ (↑κ).pairSupport | i < ↑κ i}.card → Z4) : ∫ (p : R324PhysicalPoint m), ‖r324Flatten (ρ.r324FullPairingFourierIntegrand ε α β κ q) p‖ ∂r324PhysicalMeasure m = ρ.r324CovarianceConfigurationWeight ε (↑κ) q * r324BareSkeletonL1 κ

Exact separation of a configuration's constant covariance weight from the physical L¹ mass.

noncomputable def Anderson4D.SmoothCutoff.r324StandardFullPairingRouteWeight (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) : ℝ

Routed L¹ majorant of one standardized Fourier configuration.

Equations

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

theorem Anderson4D.SmoothCutoff.r324StandardFullPairingRouteWeight_nonneg (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) : 0 ≤ ρ.r324StandardFullPairingRouteWeight ε α β κ q

theorem Anderson4D.SmoothCutoff.summable_r324StandardFullPairingRouteWeight (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) : Summable (ρ.r324StandardFullPairingRouteWeight ε α β κ)

theorem Anderson4D.SmoothCutoff.norm_r324FullPairingFourierIntegral_le_routeWeight_mul_decay (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) (i : Fin m) : ‖ρ.r324FullPairingFourierIntegral ε α β κ (r324FullConfigurationOfStandard κ q)‖ ≤ ρ.r324StandardFullPairingRouteWeight ε α β κ q * eighthOrderFrequencyDecay ‖r324StandardPairIncrement κ q i‖

The physical integral is bounded by every routed slot after paying that slot's eighth-order decay.

noncomputable def Anderson4D.SmoothCutoff.r324SharpFullPairingRouteWeight (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) : ℝ

Cancellation-preserving routed weight. In contrast to r324StandardFullPairingRouteWeight, all five physical variable groups are integrated before the norm is taken. Thus the external α/β oscillations remain available to the endpoint-first argument.

Equations

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

theorem Anderson4D.SmoothCutoff.r324SharpFullPairingRouteWeight_nonneg (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) : 0 ≤ ρ.r324SharpFullPairingRouteWeight ε α β κ q

theorem Anderson4D.SmoothCutoff.r324SharpFullPairingRouteWeight_le_standard (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) : ρ.r324SharpFullPairingRouteWeight ε α β κ q ≤ ρ.r324StandardFullPairingRouteWeight ε α β κ q

The sharp routed weight is dominated by the absolute-integral weight. This transfers summability without moving the norm inside in the final endpoint budget.

theorem Anderson4D.SmoothCutoff.summable_r324SharpFullPairingRouteWeight (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) : Summable (ρ.r324SharpFullPairingRouteWeight ε α β κ)

theorem Anderson4D.SmoothCutoff.norm_r324FullPairingFourierIntegral_le_sharpRouteWeight_mul_decay (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) (i : Fin m) : ‖ρ.r324FullPairingFourierIntegral ε α β κ (r324FullConfigurationOfStandard κ q)‖ ≤ ρ.r324SharpFullPairingRouteWeight ε α β κ q * eighthOrderFrequencyDecay ‖r324StandardPairIncrement κ q i‖

Each slot pays one eighth-order routed decay while the sharp weight retains the fully integrated endpoint oscillations.

noncomputable def Anderson4D.SmoothCutoff.r324NatFullPairingRouteWeight (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (a : ℕ) : ℝ

Natural-number form of the routed configuration weight.

Equations

• ρ.r324NatFullPairingRouteWeight hm ε α β κ a = ρ.r324StandardFullPairingRouteWeight ε α β κ ((Anderson4D.SmoothCutoff.r324NatEquivStandardConfigurations hm) a)

noncomputable def Anderson4D.SmoothCutoff.r324NatSharpFullPairingRouteWeight (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (a : ℕ) : ℝ

Natural-number form of the cancellation-preserving sharp routed weight.

Equations

• ρ.r324NatSharpFullPairingRouteWeight hm ε α β κ a = ρ.r324SharpFullPairingRouteWeight ε α β κ ((Anderson4D.SmoothCutoff.r324NatEquivStandardConfigurations hm) a)

noncomputable def Anderson4D.SmoothCutoff.r324NatFullPairingRoutedIncrement (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (a : ℕ) (i : Fin m) : EuclideanSpace ℝ (Fin dim)

Conservation-complete increments: nonzero terms retain their genuine signed covariance modes; zero terms are padded by the external mode in the first slot and zeros elsewhere.

Equations

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

theorem Anderson4D.SmoothCutoff.summable_r324NatFullPairingRouteWeight (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) : Summable (ρ.r324NatFullPairingRouteWeight hm ε α β κ)

theorem Anderson4D.SmoothCutoff.summable_r324NatSharpFullPairingRouteWeight (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) : Summable (ρ.r324NatSharpFullPairingRouteWeight hm ε α β κ)

theorem Anderson4D.SmoothCutoff.r324NatSharpFullPairingRouteWeight_nonneg (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (a : ℕ) : 0 ≤ ρ.r324NatSharpFullPairingRouteWeight hm ε α β κ a

theorem Anderson4D.SmoothCutoff.r324NatFullPairingRouteWeight_nonneg (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (a : ℕ) : 0 ≤ ρ.r324NatFullPairingRouteWeight hm ε α β κ a

theorem Anderson4D.SmoothCutoff.sum_r324NatFullPairingRoutedIncrement (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (a : ℕ) : ∑ i : Fin m, ρ.r324NatFullPairingRoutedIncrement hm ε α β κ a i = z4EuclideanFrequency (α + β)

theorem Anderson4D.SmoothCutoff.norm_r324NatFullPairingFourierTerm_le_routeWeight_mul_decay (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (a : ℕ) (i : Fin m) : ‖ρ.r324NatFullPairingFourierTerm hm ε α β κ a‖ ≤ ρ.r324NatFullPairingRouteWeight hm ε α β κ a * eighthOrderFrequencyDecay ‖ρ.r324NatFullPairingRoutedIncrement hm ε α β κ a i‖

theorem Anderson4D.SmoothCutoff.norm_r324NatFullPairingFourierTerm_le_sharpRouteWeight_mul_decay (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (a : ℕ) (i : Fin m) : ‖ρ.r324NatFullPairingFourierTerm hm ε α β κ a‖ ≤ ρ.r324NatSharpFullPairingRouteWeight hm ε α β κ a * eighthOrderFrequencyDecay ‖ρ.r324NatFullPairingRoutedIncrement hm ε α β κ a i‖

Raw countable reindexing across all full pairings

This is deliberately an intermediate Fourier/Fubini layer. It gives an exact single ℕ-indexed series and a summable majorant, but the final R-324 reduction must regroup terms by a residual-refined primitive schedule before taking norms.

@[reducible, inline]

abbrev Anderson4D.SmoothCutoff.R324FullPairingIndex (m : ℕ) : Type

Finite outer index of full doubled pairings.

Equations

• Anderson4D.SmoothCutoff.R324FullPairingIndex m = { τ : Anderson4D.PartialPairing (Fin (2 * m)) // τ.IsFull }

def Anderson4D.SmoothCutoff.r324CanonicalMomentContraction (m : ℕ) : MomentContraction m

A canonical contraction witnesses that the finite full-pairing index is nonempty for every m.

Equations

• Anderson4D.SmoothCutoff.r324CanonicalMomentContraction m = ⟨Anderson4D.PartialPairing.id, ⟨Anderson4D.PartialPairing.id, Equiv.refl ↥Anderson4D.PartialPairing.id.singles⟩⟩

instance Anderson4D.SmoothCutoff.instNonemptyR324FullPairingIndex (m : ℕ) : Nonempty (R324FullPairingIndex m)

noncomputable def Anderson4D.SmoothCutoff.r324NatEquivRawFullPairingConfigurations (m : ℕ) : ℕ ≃ R324FullPairingIndex m × ℕ

One exact enumeration of all pairs (full pairing, Fourier configuration number).

Equations

• Anderson4D.SmoothCutoff.r324NatEquivRawFullPairingConfigurations m = (Denumerable.eqv (Anderson4D.SmoothCutoff.R324FullPairingIndex m × ℕ)).symm

noncomputable def Anderson4D.SmoothCutoff.r324RawMomentFourierTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (lam ε : ℝ) (α β : Z4) (a : ℕ) : ℂ

Raw term obtained by flattening the finite full-pairing sum and each pairing's natural-number Fourier series.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324RawMomentRouteWeight (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (lam ε : ℝ) (α β : Z4) (a : ℕ) : ℝ

Raw cancellation-preserving weight for one flattened term. It is used only as a summable majorant before the residual-refined regrouping.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324RawMomentRoutedIncrement (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (a : ℕ) (i : Fin m) : EuclideanSpace ℝ (Fin dim)

Every raw flattened term carries exactly the m covariance-pair increments of its full doubled pairing.

Equations

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

theorem Anderson4D.SmoothCutoff.r324RawMomentRouteWeight_nonneg (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (lam ε : ℝ) (α β : Z4) (a : ℕ) : 0 ≤ ρ.r324RawMomentRouteWeight hm lam ε α β a

theorem Anderson4D.SmoothCutoff.summable_r324RawMomentRouteWeight (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (α β : Z4) : Summable (ρ.r324RawMomentRouteWeight hm lam ε α β)

theorem Anderson4D.SmoothCutoff.sum_r324RawMomentRoutedIncrement (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (a : ℕ) : ∑ i : Fin m, ρ.r324RawMomentRoutedIncrement hm ε α β a i = z4EuclideanFrequency (α + β)

theorem Anderson4D.SmoothCutoff.norm_r324RawMomentFourierTerm_le_routeWeight_mul_decay (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (lam ε : ℝ) (α β : Z4) (a : ℕ) (i : Fin m) : ‖ρ.r324RawMomentFourierTerm hm lam ε α β a‖ ≤ ρ.r324RawMomentRouteWeight hm lam ε α β a * eighthOrderFrequencyDecay ‖ρ.r324RawMomentRoutedIncrement hm ε α β a i‖