Residual-refined physical fibres for R-324

Inside one fixed within-half contraction signature, the residual nested schedule can still vary. This file performs the second exact regrouping used in paper Section 4.2: first by the residual endpoint signature and then, within each refined fibre, with one common Fourier/Green skeleton.

Every covariance factor is nonnegative. Consequently the norm of the original fixed-signature physical integrand is exactly the sum of the norms of the residual-refined integrands, not merely bounded by it. This is the pointwise cancellation-preserving entry to the recursive primitive block collapse.

def Anderson4D.momentResidualChainSignaturesAt (m : ℕ) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : Finset (Finset (Fin (2 * m)) × Finset (Fin (2 * m)))

Residual endpoint signatures realized inside one concrete within-half signature fibre.

Equations

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

def Anderson4D.momentRefinedContractionFiber (m : ℕ) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : Finset (MomentContraction m)

The contraction entities with both a fixed within-half signature and a fixed residual-chain endpoint signature.

Equations

• Anderson4D.momentRefinedContractionFiber m s r = {e ∈ Anderson4D.momentContractionFiber m s | Anderson4D.momentResidualChainSignature e.fst e.snd.fst e.snd.snd = r}

@[simp]

theorem Anderson4D.mem_momentRefinedContractionFiber {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} {e : MomentContraction m} : e ∈ momentRefinedContractionFiber m s r ↔ momentContractionSignature e = s ∧ momentResidualChainSignature e.fst e.snd.fst e.snd.snd = r

theorem Anderson4D.card_momentResidualChainSignaturesAt_le (m : ℕ) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : (momentResidualChainSignaturesAt m s).card ≤ 4 ^ (2 * m)

The extra residual grouping costs at most 4^(2m).

theorem Anderson4D.sum_momentContractionFiber_by_residualChainSignature {m : ℕ} (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) {A : Type u_1} [AddCommMonoid A] (F : MomentContraction m → A) : ∑ r ∈ momentResidualChainSignaturesAt m s, ∑ e ∈ momentRefinedContractionFiber m s r, F e = ∑ e ∈ momentContractionFiber m s, F e

Exact second regrouping of a fixed moment-signature fibre.

theorem Anderson4D.momentNonemptyPrimitiveBlocks_eq_of_mem_refinedFiber {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} {e e' : MomentContraction m} (he : e ∈ momentRefinedContractionFiber m s r) (he' : e' ∈ momentRefinedContractionFiber m s r) : momentNonemptyPrimitiveBlocks e.fst e.snd.fst e.snd.snd = momentNonemptyPrimitiveBlocks e'.fst e'.snd.fst e'.snd.snd

All entities in one refined fibre have literally the same primitive block schedule.

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

The pointwise physical integrand of one residual-refined fibre.

Equations

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

theorem Anderson4D.momentSignaturePhysicalIntegrand_eq_sum_refined (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (x y z w : T4) (v : Fin (2 * m) → T4) : momentSignaturePhysicalIntegrand ρ ε m α β s x y z w v = ∑ r ∈ momentResidualChainSignaturesAt m s, momentRefinedPhysicalIntegrand ρ ε m α β s r x y z w v

Exact regrouping of the physical integrand by residual endpoint signature.

theorem Anderson4D.momentRefinedPhysicalIntegrand_eq_commonSkeletons_mul_sum_covariance (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentContractionFiber m s) (x y z w : T4) (v : Fin (2 * m) → T4) : momentRefinedPhysicalIntegrand ρ ε m α β s r x y z w v = momentFourierPhase α β x y z w * renormalizedGreenSkeleton e₀.fst (assemble x y fun (i : Fin m) => v (leftMomentIndex i)) * renormalizedGreenSkeleton e₀.snd.fst (assemble z w fun (i : Fin m) => v (rightMomentIndex i)) * ∑ e ∈ momentRefinedContractionFiber m s r, ↑(primitiveCovarianceProduct ρ ε m (momentCombinedPairing e.fst e.snd.fst e.snd.snd) v)

On every refined fibre the Fourier phase and both renormalized Green skeletons remain common, while only the nonnegative covariance product is summed.

theorem Anderson4D.norm_momentRefinedPhysicalIntegrand_eq_commonSkeletons_mul_sum_covariance (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentContractionFiber m s) (x y z w : T4) (v : Fin (2 * m) → T4) : ‖momentRefinedPhysicalIntegrand ρ ε m α β s r x y z w v‖ = ‖renormalizedGreenSkeleton e₀.fst (assemble x y fun (i : Fin m) => v (leftMomentIndex i))‖ * ‖renormalizedGreenSkeleton e₀.snd.fst (assemble z w fun (i : Fin m) => v (rightMomentIndex i))‖ * ∑ e ∈ momentRefinedContractionFiber m s r, primitiveCovarianceProduct ρ ε m (momentCombinedPairing e.fst e.snd.fst e.snd.snd) v

Norm form of the refined common-skeleton factorization.

theorem Anderson4D.norm_momentSignaturePhysicalIntegrand_eq_sum_refined (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hs : s ∈ momentContractionSignatures m) (x y z w : T4) (v : Fin (2 * m) → T4) : ‖momentSignaturePhysicalIntegrand ρ ε m α β s x y z w v‖ = ∑ r ∈ momentResidualChainSignaturesAt m s, ‖momentRefinedPhysicalIntegrand ρ ε m α β s r x y z w v‖

Pointwise exact additivity of the norm across residual-refined fibres. No triangle inequality or pairing-cardinality loss occurs here.

theorem Anderson4D.norm_momentSignaturePhysicalIntegrand_le_four_pow_mul_of_refined (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hs : s ∈ momentContractionSignatures m) (x y z w : T4) (v : Fin (2 * m) → T4) (B : ℝ) (hB : 0 ≤ B) (hrefined : ∀ r ∈ momentResidualChainSignaturesAt m s, ‖momentRefinedPhysicalIntegrand ρ ε m α β s r x y z w v‖ ≤ B) : ‖momentSignaturePhysicalIntegrand ρ ε m α β s x y z w v‖ ≤ 4 ^ (2 * m) * B

Absorb the exponential number of residual schedules into a single coarse 4^(2m) factor.

theorem Anderson4D.scaled_norm_momentSignaturePhysicalIntegrand_le_insertedMajorant_of_refined (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hs : s ∈ momentContractionSignatures m) (x y z w : T4) (v : Fin (2 * m) → T4) (scale C supportConstant : ℝ) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hrefined : ∀ r ∈ momentResidualChainSignaturesAt m s, scale * ‖momentRefinedPhysicalIntegrand ρ ε m α β s r x y z w v‖ ≤ primitiveInsertedMajorant C lam ε supportConstant m x) : scale * ‖momentSignaturePhysicalIntegrand ρ ε m α β s x y z w v‖ ≤ primitiveInsertedMajorant (4 * C) lam ε supportConstant m x

Per-refined-schedule inserted bounds assemble into the exact fixed-signature pointwise majorant, with the residual signature count absorbed by replacing C with 4C.