Endpoint budgets for grouped refined R-324 fibres

The preceding module rewrites a complete residual-refined fibre as four separated external Green legs times one internal core. Here we perform the four external Fourier integrations and derive the endpoint budget, still without moving a norm through the primitive-pairing sum contained in the core.

noncomputable def Anderson4D.r324RefinedEndpointCoefficient (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (v : Fin (2 * m) → T4) : ℂ

Endpoint-first coefficient of one refined fibre at fixed internal variables.

Equations

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

theorem Anderson4D.r324RefinedEndpointCoefficient_eq (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentContractionFiber m s) (v : Fin (2 * m) → T4) : r324RefinedEndpointCoefficient ρ ε m α β s r v = r324EndpointCoefficient α (r324ContractionEndpointAnchors hm e₀ v 0).1 (r324ContractionEndpointAnchors hm e₀ v 0).2 (r324ContractionEndpointFlags e₀ 0) * (r324EndpointCoefficient β (r324ContractionEndpointAnchors hm e₀ v 1).1 (r324ContractionEndpointAnchors hm e₀ v 1).2 (r324ContractionEndpointFlags e₀ 1) * (r324EndpointCoefficient (-α) (r324ContractionEndpointAnchors hm e₀ v 2).1 (r324ContractionEndpointAnchors hm e₀ v 2).2 (r324ContractionEndpointFlags e₀ 2) * (r324EndpointCoefficient (-β) (r324ContractionEndpointAnchors hm e₀ v 3).1 (r324ContractionEndpointAnchors hm e₀ v 3).2 (r324ContractionEndpointFlags e₀ 3) * r324RefinedEndpointCore ρ ε m s r e₀ v)))

Exact coefficient formula. he₀ is only the certificate selecting a common Green skeleton for the realized within-half signature.

theorem Anderson4D.norm_r324RefinedEndpointCoefficient_eq (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentContractionFiber m s) (v : Fin (2 * m) → T4) : ‖r324RefinedEndpointCoefficient ρ ε m α β s r v‖ = r324FourEndpointCoefficientWeight α β (r324ContractionEndpointAnchors hm e₀ v) (r324ContractionEndpointFlags e₀) * ‖r324RefinedEndpointCore ρ ε m s r e₀ v‖

Norm of the fixed-internal-variable coefficient: all primitive-pairing cancellation remains inside the norm of the refined core.

theorem Anderson4D.sacrificed_norm_r324RefinedEndpointCoefficient_le (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentContractionFiber m s) (v : Fin (2 * m) → T4) : ε⁻¹ ^ 8 * ‖r324RefinedEndpointCoefficient ρ ε m α β s r v‖ ≤ 16 * r324EndpointLoss ε α β * ‖r324RefinedEndpointCore ρ ε m s r e₀ v‖

The paper's complete four-endpoint loss at fixed internal variables. The ε⁻⁸ factor is exactly the four ordinary-versus-inserted sacrifices.

Finite aggregation over the actual refined signatures

noncomputable def Anderson4D.r324ResidualEndpointCoefficientNormSum (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (v : Fin (2 * m) → T4) : ℝ

Sum of endpoint-first coefficient norms over all residual schedules inside one realized within-half signature.

Equations

• Anderson4D.r324ResidualEndpointCoefficientNormSum ρ ε m α β s v = ∑ r ∈ Anderson4D.momentResidualChainSignaturesAt m s, ‖Anderson4D.r324RefinedEndpointCoefficient ρ ε m α β s r v‖

noncomputable def Anderson4D.r324ResidualEndpointCoreNormSum (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (e₀ : MomentContraction m) (v : Fin (2 * m) → T4) : ℝ

Matching grouped-core budget. The norm is outside the complete primitive-pairing sum in each residual-refined fibre.

Equations

• Anderson4D.r324ResidualEndpointCoreNormSum ρ ε m s e₀ v = ∑ r ∈ Anderson4D.momentResidualChainSignaturesAt m s, ‖Anderson4D.r324RefinedEndpointCore ρ ε m s r e₀ v‖

theorem Anderson4D.r324ResidualEndpointCoreNormSum_nonneg (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (e₀ : MomentContraction m) (v : Fin (2 * m) → T4) : 0 ≤ r324ResidualEndpointCoreNormSum ρ ε m s e₀ v

theorem Anderson4D.sacrificed_r324ResidualEndpointCoefficientNormSum_le (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentContractionFiber m s) (v : Fin (2 * m) → T4) : ε⁻¹ ^ 8 * r324ResidualEndpointCoefficientNormSum ρ ε m α β s v ≤ 16 * r324EndpointLoss ε α β * r324ResidualEndpointCoreNormSum ρ ε m s e₀ v

The four-leg endpoint estimate summed over every actual residual schedule. No residual-cardinality factor appears: both sides contain the same finite sum.

Aggregation over every realized within-half signature

noncomputable def Anderson4D.r324MomentSignatureRepresentative (m : ℕ) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : MomentContraction m

Canonical representative of a realized moment signature. Outside the realized signature finset the value is irrelevant.

Equations

• Anderson4D.r324MomentSignatureRepresentative m s = if hs : s ∈ Anderson4D.momentContractionSignatures m then Classical.choose ⋯ else default

theorem Anderson4D.r324MomentSignatureRepresentative_mem (m : ℕ) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hs : s ∈ momentContractionSignatures m) : r324MomentSignatureRepresentative m s ∈ momentContractionFiber m s

noncomputable def Anderson4D.r324AllRefinedEndpointCoefficientNormSum (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (v : Fin (2 * m) → T4) : ℝ

Complete pointwise endpoint-first norm budget over every realized refined fibre.

Equations

• Anderson4D.r324AllRefinedEndpointCoefficientNormSum ρ ε m α β v = ∑ s ∈ Anderson4D.momentContractionSignatures m, Anderson4D.r324ResidualEndpointCoefficientNormSum ρ ε m α β s v

noncomputable def Anderson4D.r324AllRefinedEndpointCoreNormSum (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (v : Fin (2 * m) → T4) : ℝ

Complete matching grouped-core budget.

Equations

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

theorem Anderson4D.r324AllRefinedEndpointCoreNormSum_nonneg (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (v : Fin (2 * m) → T4) : 0 ≤ r324AllRefinedEndpointCoreNormSum ρ ε m v

theorem Anderson4D.sacrificed_r324AllRefinedEndpointCoefficientNormSum_le (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4) (v : Fin (2 * m) → T4) : ε⁻¹ ^ 8 * r324AllRefinedEndpointCoefficientNormSum ρ ε m α β v ≤ 16 * r324EndpointLoss ε α β * r324AllRefinedEndpointCoreNormSum ρ ε m v

Concrete aggregate endpoint budget. This is the direct weightBudget ≤ amplitude * r324EndpointLoss shape before the remaining internal-variable integral and primitive block bounds are applied.