Summable grouped covariance budgets for R-324

The cancellation-preserving refined expansion is grouped by the common signed increment vector before a norm is taken. This file proves that the scalar covariance weights of those groups remain summable after inserting the reciprocal eighth-order routing cost. The proof first establishes the corresponding statement for raw refined configurations and then uses the exact tsumByKey fibre decomposition.

No primitive-collapse estimate is assumed here. This is a qualitative Fubini/summability layer only: separating the scalar covariance weights from the physical Green skeleton is too coarse to recover the paper-scale P-3.5b-det amplitude. The quantitative critical path must keep the unexpanded covariances inside the primitive physical collapse and expand only the final marked surviving edge.

noncomputable def Anderson4D.SmoothCutoff.r324IncrementKeyCost {m : ℕ} (key : Fin m → Z4) : ℝ

Reciprocal routing cost carried by one arbitrary increment key.

Equations

• Anderson4D.SmoothCutoff.r324IncrementKeyCost key = ∑ i : Fin m, (1 + ‖Anderson4D.z4EuclideanFrequency (key i)‖ ^ 2) ^ 4

theorem Anderson4D.SmoothCutoff.r324IncrementKeyCost_nonneg {m : ℕ} (key : Fin m → Z4) : 0 ≤ r324IncrementKeyCost key

theorem Anderson4D.SmoothCutoff.r324IncrementKeyCost_natConfiguration {m : ℕ} (hm : 0 < m) (b : ℕ) : r324IncrementKeyCost ((r324NatEquivStandardConfigurations hm) b) = ∑ i : Fin m, r324GroupedIncrementCost hm b i

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

Raw refined covariance weight with one reciprocal routing cost.

Equations

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

theorem Anderson4D.SmoothCutoff.r324RefinedRawCovarianceRouteWeight_nonneg (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m) (a : ℕ) : 0 ≤ ρ.r324RefinedRawCovarianceRouteWeight hm ε p a

theorem Anderson4D.SmoothCutoff.summable_r324RefinedRawCovarianceRouteWeight (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) : Summable (ρ.r324RefinedRawCovarianceRouteWeight hm ε p)

Raw refined covariance route weights are summable. Only one degree-eight cost is inserted at a time.

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

Grouped scalar covariance route weight.

Equations

• ρ.r324GroupedCovarianceRouteWeight hm ε p = ρ.r324KeyGroupedRefinedCovarianceWeight hm ε p.1 p.2 * ∑ i : Fin m, Anderson4D.SmoothCutoff.r324GroupedIncrementCost hm p.2 i

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

theorem Anderson4D.SmoothCutoff.r324GroupedCovarianceRouteWeight_eq_tsumByKey (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m) (b : ℕ) : ρ.r324GroupedCovarianceRouteWeight hm ε (p, b) = tsumByKey (ρ.r324RefinedRawCovarianceRouteWeight hm ε p) (r324RefinedRawIncrementKey hm p) ((r324NatEquivStandardConfigurations hm) b)

One grouped route weight is exactly the fibrewise sum of the raw route weights carrying that increment key.

theorem Anderson4D.SmoothCutoff.summable_r324GroupedCovarianceRouteWeight_fiber (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) : Summable fun (b : ℕ) => ρ.r324GroupedCovarianceRouteWeight hm ε (p, b)

For one refined schedule, all common-increment grouped covariance route weights are summable.

theorem Anderson4D.SmoothCutoff.summable_r324GroupedCovarianceRouteWeight (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) : Summable (ρ.r324GroupedCovarianceRouteWeight hm ε)

The complete schedule-by-key grouped covariance route budget is summable.

theorem Anderson4D.SmoothCutoff.tsum_r324GroupedCovarianceRouteWeight_fiber (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) : ∑' (b : ℕ), ρ.r324GroupedCovarianceRouteWeight hm ε (p, b) = ∑' (a : ℕ), ρ.r324RefinedRawCovarianceRouteWeight hm ε p a

Exact removal of the common-increment grouping from the scalar route budget of one refined schedule.

Passage from a physical core majorant to the routed budget

theorem Anderson4D.SmoothCutoff.r324GroupedRouteBaseWeight_le_groupedCovarianceRouteWeight (ρ : SmoothCutoff) (lam C : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (hcore : ∀ (p : R324RefinedScheduleIndex m × ℕ), ρ.r324GroupedRefinedCoreL1 hm ε p ≤ C * ρ.r324KeyGroupedRefinedCovarianceWeight hm ε p.1 p.2) (p : R324RefinedScheduleIndex m × ℕ) : ρ.r324GroupedRouteBaseWeight lam hm ε p ≤ |lamEps lam ε| ^ (2 * m) * C * ρ.r324GroupedCovarianceRouteWeight hm ε p

A uniform physical L¹ bound by the grouped scalar covariance weight dominates the concrete grouped route base weight.

theorem Anderson4D.SmoothCutoff.summable_r324GroupedRouteBaseWeight_of_coreCovarianceMajorant (ρ : SmoothCutoff) (lam C : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hcore : ∀ (p : R324RefinedScheduleIndex m × ℕ), ρ.r324GroupedRefinedCoreL1 hm ε p ≤ C * ρ.r324KeyGroupedRefinedCovarianceWeight hm ε p.1 p.2) : Summable (ρ.r324GroupedRouteBaseWeight lam hm ε)

A uniform grouped-core majorant transfers the already-proved scalar covariance summability to the concrete grouped route weights.

theorem Anderson4D.SmoothCutoff.integratedPrimitiveCollapseBudget_of_coreCovarianceMajorant (ρ : SmoothCutoff) (lam C covarianceAmplitude : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hC : 0 ≤ C) (hintegrable : ∀ (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)) (hcore : ∀ (p : R324RefinedScheduleIndex m × ℕ), ρ.r324GroupedRefinedCoreL1 hm ε p ≤ C * ρ.r324KeyGroupedRefinedCovarianceWeight hm ε p.1 p.2) (hcovariance : ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324GroupedCovarianceRouteWeight hm ε p ≤ covarianceAmplitude) : ρ.IntegratedPrimitiveCollapseBudget lam ε m hm (|lamEps lam ε| ^ (2 * m) * C * covarianceAmplitude)

A logically exact, but generally coarse, constructor for the downstream integrated primitive-collapse budget.

It applies when a sharp core/covariance separation is independently available. Naive instances of hcore and hcovariance lose unacceptable powers of ε and the primitive-fibre cancellation.