Fixed-signature block collapse for R-324

Paper §4.2 first identifies a contraction triple (κ⁺, κ⁻, π) with a full pairing of the doubled carrier. It then fixes the within-half extraction signature and sums all primitive pairings in each extracted block before applying Proposition 4.1.

This file starts the exact finite reindexing needed for that argument. The first structural fact is that the doubled pairing remembers the entire contraction triple: no multiplicity is introduced when the contraction sum is viewed as a sum over full doubled pairings.

Separating the two halves of a moment signature

@[simp]

theorem Anderson4D.leftMomentIndex_mem_endpointImageUnion_iff {m : ℕ} (A B : Finset (Fin m)) (i : Fin m) : leftMomentIndex i ∈ Finset.image leftMomentIndex A ∪ Finset.image rightMomentIndex B ↔ i ∈ A

@[simp]

theorem Anderson4D.rightMomentIndex_mem_endpointImageUnion_iff {m : ℕ} (A B : Finset (Fin m)) (j : Fin m) : rightMomentIndex j ∈ Finset.image leftMomentIndex A ∪ Finset.image rightMomentIndex B ↔ j ∈ B

theorem Anderson4D.reductionEndpointSignatures_eq_of_momentContractionSignature_eq {m : ℕ} (e e' : MomentContraction m) (hsignature : momentContractionSignature e = momentContractionSignature e') : reductionEndpointSignature e.fst = reductionEndpointSignature e'.fst ∧ reductionEndpointSignature e.snd.fst = reductionEndpointSignature e'.snd.fst

Equality of doubled moment signatures recovers the two ordinary endpoint signatures separately.

theorem Anderson4D.renormalizedGreenSkeletons_eq_of_momentContractionSignature_eq {m : ℕ} (e e' : MomentContraction m) (hsignature : momentContractionSignature e = momentContractionSignature e') : renormalizedGreenSkeleton e.fst = renormalizedGreenSkeleton e'.fst ∧ renormalizedGreenSkeleton e.snd.fst = renormalizedGreenSkeleton e'.snd.fst

The fixed moment signature makes both signed Green skeletons common across its whole contraction fibre.

Splitting a full pairing on the two copies

def Anderson4D.momentLeftRestrictionMap {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) : Fin m → Fin m

Retain pairs contained in the left copy and turn every cross-copy endpoint into a single.

Equations

• Anderson4D.momentLeftRestrictionMap κ i = match κ (Sum.inl i) with | Sum.inl j => j | Sum.inr val => i

theorem Anderson4D.momentLeftRestrictionMap_involutive {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) : Function.Involutive (momentLeftRestrictionMap κ)

def Anderson4D.momentLeftRestriction {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) : PartialPairing (Fin m)

The partial pairing induced inside the left copy.

Equations

• Anderson4D.momentLeftRestriction κ = { toFun := Anderson4D.momentLeftRestrictionMap κ, involutive := ⋯ }

def Anderson4D.momentRightRestrictionMap {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) : Fin m → Fin m

Retain pairs contained in the right copy and turn every cross-copy endpoint into a single.

Equations

• Anderson4D.momentRightRestrictionMap κ j = match κ (Sum.inr j) with | Sum.inl val => j | Sum.inr i => i

theorem Anderson4D.momentRightRestrictionMap_involutive {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) : Function.Involutive (momentRightRestrictionMap κ)

def Anderson4D.momentRightRestriction {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) : PartialPairing (Fin m)

The partial pairing induced inside the right copy.

Equations

• Anderson4D.momentRightRestriction κ = { toFun := Anderson4D.momentRightRestrictionMap κ, involutive := ⋯ }

@[simp]

theorem Anderson4D.momentLeftRestriction_apply_of_left {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) {i j : Fin m} (h : κ (Sum.inl i) = Sum.inl j) : (momentLeftRestriction κ) i = j

@[simp]

theorem Anderson4D.momentLeftRestriction_apply_of_right {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) {i j : Fin m} (h : κ (Sum.inl i) = Sum.inr j) : (momentLeftRestriction κ) i = i

@[simp]

theorem Anderson4D.momentRightRestriction_apply_of_left {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) {i j : Fin m} (h : κ (Sum.inr j) = Sum.inl i) : (momentRightRestriction κ) j = j

@[simp]

theorem Anderson4D.momentRightRestriction_apply_of_right {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) {i j : Fin m} (h : κ (Sum.inr j) = Sum.inr i) : (momentRightRestriction κ) j = i

theorem Anderson4D.mem_momentLeftRestriction_singles_iff {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) (hfull : κ.IsFull) (i : Fin m) : i ∈ (momentLeftRestriction κ).singles ↔ ∃ (j : Fin m), κ (Sum.inl i) = Sum.inr j

For a full pairing, a left index is a single of the within-left restriction exactly when it is paired across the cut.

theorem Anderson4D.mem_momentRightRestriction_singles_iff {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) (hfull : κ.IsFull) (j : Fin m) : j ∈ (momentRightRestriction κ).singles ↔ ∃ (i : Fin m), κ (Sum.inr j) = Sum.inl i

Right-copy counterpart of mem_momentLeftRestriction_singles_iff.

noncomputable def Anderson4D.momentCrossRight {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) (hfull : κ.IsFull) (i : ↥(momentLeftRestriction κ).singles) : Fin m

The right endpoint paired with a left single in a full sum pairing.

Equations

• Anderson4D.momentCrossRight κ hfull i = Classical.choose ⋯

theorem Anderson4D.momentCrossRight_spec {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) (hfull : κ.IsFull) (i : ↥(momentLeftRestriction κ).singles) : κ (Sum.inl ↑i) = Sum.inr (momentCrossRight κ hfull i)

theorem Anderson4D.momentCrossRight_mem_singles {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) (hfull : κ.IsFull) (i : ↥(momentLeftRestriction κ).singles) : momentCrossRight κ hfull i ∈ (momentRightRestriction κ).singles

noncomputable def Anderson4D.momentCrossLeft {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) (hfull : κ.IsFull) (j : ↥(momentRightRestriction κ).singles) : Fin m

The left endpoint paired with a right single in a full sum pairing.

Equations

• Anderson4D.momentCrossLeft κ hfull j = Classical.choose ⋯

theorem Anderson4D.momentCrossLeft_spec {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) (hfull : κ.IsFull) (j : ↥(momentRightRestriction κ).singles) : κ (Sum.inr ↑j) = Sum.inl (momentCrossLeft κ hfull j)

theorem Anderson4D.momentCrossLeft_mem_singles {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) (hfull : κ.IsFull) (j : ↥(momentRightRestriction κ).singles) : momentCrossLeft κ hfull j ∈ (momentLeftRestriction κ).singles

noncomputable def Anderson4D.momentCrossEquiv {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) (hfull : κ.IsFull) : ↥(momentLeftRestriction κ).singles ≃ ↥(momentRightRestriction κ).singles

The cross-copy pairs of a full sum pairing form an equivalence between the singles of its two within-copy restrictions.

Equations

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

theorem Anderson4D.momentCombinedSumPairing_restrictions {m : ℕ} (κ : PartialPairing (Fin m ⊕ Fin m)) (hfull : κ.IsFull) : momentCombinedSumPairing (momentLeftRestriction κ) (momentRightRestriction κ) (momentCrossEquiv κ hfull) = κ

Splitting a full sum pairing into its two within-copy restrictions and its cross equivalence, then recombining, returns the original pairing.

theorem Anderson4D.momentCombinedPairing_injective_pairings {m : ℕ} {κp κm κp' κm' : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {π' : ↥κp'.singles ≃ ↥κm'.singles} (hcombined : momentCombinedPairing κp κm π = momentCombinedPairing κp' κm' π') : κp = κp' ∧ κm = κm'

The full doubled pairing determines both within-copy partial pairings.

theorem Anderson4D.momentCombinedPairing_injective_crossEquiv {m : ℕ} {κp κm : PartialPairing (Fin m)} {π π' : ↥κp.singles ≃ ↥κm.singles} (hcombined : momentCombinedPairing κp κm π = momentCombinedPairing κp κm π') : π = π'

The full doubled pairing determines the cross-single equivalence once the two within-copy partial pairings have been identified.

theorem Anderson4D.momentCombinedPairing_injective {m : ℕ} : Function.Injective fun (e : MomentContraction m) => momentCombinedPairing e.fst e.snd.fst e.snd.snd

The map from contraction entities to full doubled pairings is injective. Consequently the passage from (4.18) to a full-pairing sum carries no hidden multiplicity.

Equivalence with full doubled pairings

def Anderson4D.momentSplitSumPairing {m : ℕ} (κ : PartialPairing (Fin (2 * m))) : PartialPairing (Fin m ⊕ Fin m)

Transport a doubled pairing back to the disjoint-union carrier.

Equations

• Anderson4D.momentSplitSumPairing κ = (Anderson4D.PartialPairing.congr (Anderson4D.momentDoubleFinEquiv m).symm) κ

theorem Anderson4D.momentSplitSumPairing_isFull {m : ℕ} {κ : PartialPairing (Fin (2 * m))} (hfull : κ.IsFull) : (momentSplitSumPairing κ).IsFull

noncomputable def Anderson4D.momentContractionOfFull {m : ℕ} (κ : PartialPairing (Fin (2 * m))) (hfull : κ.IsFull) : MomentContraction m

The contraction triple canonically recovered from a full doubled pairing.

Equations

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

theorem Anderson4D.momentCombinedPairing_momentContractionOfFull {m : ℕ} (κ : PartialPairing (Fin (2 * m))) (hfull : κ.IsFull) : momentCombinedPairing (momentContractionOfFull κ hfull).fst (momentContractionOfFull κ hfull).snd.fst (momentContractionOfFull κ hfull).snd.snd = κ

Recombining the canonical contraction triple of a full doubled pairing returns that pairing.

theorem Anderson4D.momentCombinedPairing_surjective_full {m : ℕ} (κ : PartialPairing (Fin (2 * m))) (hfull : κ.IsFull) : ∃ (e : MomentContraction m), momentCombinedPairing e.fst e.snd.fst e.snd.snd = κ

Every full pairing of the doubled carrier arises from a unique contraction triple.

noncomputable def Anderson4D.momentContractionEquivFullPairing (m : ℕ) : MomentContraction m ≃ { κ : PartialPairing (Fin (2 * m)) // κ.IsFull }

Exact equivalence used to replace the contraction sum in (4.18) by the sum over full pairings on the doubled carrier.

Equations

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

Fixed-signature fibres on full pairings

noncomputable def Anderson4D.momentFullPairingSignature {m : ℕ} (κ : { κ : PartialPairing (Fin (2 * m)) // κ.IsFull }) : Finset (Fin (2 * m)) × Finset (Fin (2 * m))

The within-half extraction signature, now regarded as data carried by a full doubled pairing via the canonical inverse contraction.

Equations

• Anderson4D.momentFullPairingSignature κ = Anderson4D.momentContractionSignature ((Anderson4D.momentContractionEquivFullPairing m).symm κ)

@[simp]

theorem Anderson4D.momentFullPairingSignature_momentCombinedPairing {m : ℕ} (e : MomentContraction m) : momentFullPairingSignature ⟨momentCombinedPairing e.fst e.snd.fst e.snd.snd, ⋯⟩ = momentContractionSignature e

noncomputable def Anderson4D.momentContractionFiberEquivFullPairingFiber (m : ℕ) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : ↥(momentContractionFiber m s) ≃ { κ : { κ : PartialPairing (Fin (2 * m)) // κ.IsFull } // momentFullPairingSignature κ = s }

Exact equivalence between a fixed contraction-signature fibre and the corresponding fibre of full doubled pairings. This is the precise finite domain on which the primitive block sums must subsequently be factorized.

Equations

• Anderson4D.momentContractionFiberEquivFullPairingFiber m s = (Anderson4D.momentContractionEquivFullPairing m).subtypeEquiv ⋯

noncomputable def Anderson4D.momentFullPairingFiber (m : ℕ) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : Finset { κ : PartialPairing (Fin (2 * m)) // κ.IsFull }

The finite set of full doubled pairings having one fixed within-half extraction signature.

Equations

• Anderson4D.momentFullPairingFiber m s = {κ : { κ : Anderson4D.PartialPairing (Fin (2 * m)) // κ.IsFull } | Anderson4D.momentFullPairingSignature κ = s}

@[simp]

theorem Anderson4D.mem_momentFullPairingFiber {m : ℕ} {s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} {κ : { κ : PartialPairing (Fin (2 * m)) // κ.IsFull }} : κ ∈ momentFullPairingFiber m s ↔ momentFullPairingSignature κ = s

theorem Anderson4D.momentContractionFiber_nonempty_iff_mem_signatures {m : ℕ} {s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} : (momentContractionFiber m s).Nonempty ↔ s ∈ momentContractionSignatures m

A signature occurs in the finite signature set exactly when its contraction fibre is nonempty.

theorem Anderson4D.renormalizedGreenSkeletons_eq_of_mem_momentFullPairingFiber {m : ℕ} {s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} {κ κ' : { κ : PartialPairing (Fin (2 * m)) // κ.IsFull }} (hκ : κ ∈ momentFullPairingFiber m s) (hκ' : κ' ∈ momentFullPairingFiber m s) : have e := (momentContractionEquivFullPairing m).symm κ; have e' := (momentContractionEquivFullPairing m).symm κ'; renormalizedGreenSkeleton e.fst = renormalizedGreenSkeleton e'.fst ∧ renormalizedGreenSkeleton e.snd.fst = renormalizedGreenSkeleton e'.snd.fst

Two full doubled pairings in one moment-signature fibre have the same left and right renormalized Green skeletons after applying the canonical inverse contraction.

theorem Anderson4D.image_momentContractionFiber_eq_momentFullPairingFiber (m : ℕ) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : Finset.image (⇑(momentContractionEquivFullPairing m)) (momentContractionFiber m s) = momentFullPairingFiber m s

The image of the original contraction fibre is exactly the full-pairing fibre, not merely a subset of it.

theorem Anderson4D.sum_momentContractionFiber_eq_sum_fullPairingFiber {m : ℕ} {A : Type u_1} [AddCommMonoid A] (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (F : { κ : PartialPairing (Fin (2 * m)) // κ.IsFull } → A) : ∑ e ∈ momentContractionFiber m s, F ((momentContractionEquivFullPairing m) e) = ∑ κ ∈ momentFullPairingFiber m s, F κ

Exact finite-sum replacement of a fixed contraction fibre by the corresponding full-pairing fibre.

theorem Anderson4D.sum_momentContractionFiber_eq_sum_doubledPairingImage {m : ℕ} {A : Type u_1} [AddCommMonoid A] (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (F : PartialPairing (Fin (2 * m)) → A) : ∑ e ∈ momentContractionFiber m s, F (momentCombinedPairing e.fst e.snd.fst e.snd.snd) = ∑ κ ∈ Finset.image (fun (e : MomentContraction m) => momentCombinedPairing e.fst e.snd.fst e.snd.snd) (momentContractionFiber m s), F κ

Exact fixed-signature reindexing onto the corresponding set of full doubled pairings. This is the finite-sum form used before the successive primitive-block collapses; injectivity shows that no fibre cardinality factor is introduced.

theorem Anderson4D.isFull_of_mem_momentContractionFiber_image {m : ℕ} {s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} {κ : PartialPairing (Fin (2 * m))} (hκ : κ ∈ Finset.image (fun (e : MomentContraction m) => momentCombinedPairing e.fst e.snd.fst e.snd.snd) (momentContractionFiber m s)) : κ.IsFull

Every pairing in the fixed-signature image is full.

Reindexing the actual physical integrand

noncomputable def Anderson4D.momentFullPairingPhysicalIntegrand (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κ : { κ : PartialPairing (Fin (2 * m)) // κ.IsFull }) (x y z w : T4) (v : Fin (2 * m) → T4) : ℂ

One R-324 physical integrand indexed by the equivalent full doubled pairing rather than by a contraction triple.

Equations

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

@[simp]

theorem Anderson4D.momentFullPairingPhysicalIntegrand_momentContraction (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (e : MomentContraction m) (x y z w : T4) (v : Fin (2 * m) → T4) : momentFullPairingPhysicalIntegrand ρ ε m α β ((momentContractionEquivFullPairing m) e) x y z w v = deterministicMomentIntegrand ρ ε m α β e.fst e.snd.fst e.snd.snd x y z w v

theorem Anderson4D.momentSignaturePhysicalIntegrand_eq_sum_fullPairingFiber (ρ : 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 = ∑ κ ∈ momentFullPairingFiber m s, momentFullPairingPhysicalIntegrand ρ ε m α β κ x y z w v

Equation (4.18), with the fixed-signature contraction sum replaced exactly by its full-pairing fibre.

noncomputable def Anderson4D.momentFourierPhase (α β : Z4) (x y z w : T4) : ℂ

The Fourier phase common to every contraction in a fixed physical configuration.

Equations

• Anderson4D.momentFourierPhase α β x y z w = Anderson4D.charT4 α x * Anderson4D.charT4 β y * Anderson4D.charT4 (-α) z * Anderson4D.charT4 (-β) w

theorem Anderson4D.deterministicMomentIntegrand_eq_skeletons_mul_fullCovariance (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (x y z w : T4) (v : Fin (2 * m) → T4) : deterministicMomentIntegrand ρ ε m α β κp κm π x y z w v = momentFourierPhase α β x y z w * renormalizedGreenSkeleton κp (assemble x y fun (i : Fin m) => v (leftMomentIndex i)) * renormalizedGreenSkeleton κm (assemble z w fun (i : Fin m) => v (rightMomentIndex i)) * ↑(primitiveCovarianceProduct ρ ε m (momentCombinedPairing κp κm π) v)

The deterministic R-324 integrand factors through the Green skeletons of the two within-copy restrictions and the covariance product of the one full doubled pairing. This is the algebraic content of the passage to κ' immediately before paper (4.18).

theorem Anderson4D.momentFullPairingPhysicalIntegrand_eq_skeletons_mul_covariance (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κ : { κ : PartialPairing (Fin (2 * m)) // κ.IsFull }) (x y z w : T4) (v : Fin (2 * m) → T4) : momentFullPairingPhysicalIntegrand ρ ε m α β κ x y z w v = have e := (momentContractionEquivFullPairing m).symm κ; 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)) * ↑(primitiveCovarianceProduct ρ ε m (↑κ) v)

Full-pairing-indexed form of the preceding factorization.

theorem Anderson4D.momentSignaturePhysicalIntegrand_eq_commonSkeletons_mul_sum_covariance (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s : 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) : momentSignaturePhysicalIntegrand ρ ε m α β s 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)) * ∑ κ ∈ momentFullPairingFiber m s, ↑(primitiveCovarianceProduct ρ ε m (↑κ) v)

On a nonempty fixed-signature fibre, both Green skeletons are common factors. Consequently the complete primitive-pairing sum is formed before any absolute-value estimate is applied. This is the exact algebraic factorization underlying paper (4.18) and avoids a factorial loss from termwise bounds.

theorem Anderson4D.exists_commonSkeleton_factorization_of_mem_momentContractionSignatures (ρ : 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) : ∃ e₀ ∈ momentContractionFiber m s, momentSignaturePhysicalIntegrand ρ ε m α β s 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)) * ∑ κ ∈ momentFullPairingFiber m s, ↑(primitiveCovarianceProduct ρ ε m (↑κ) v)

Every realized signature admits a representative whose two Green skeletons can be pulled in front of the complete primitive-pairing sum.

theorem Anderson4D.norm_momentSignaturePhysicalIntegrand_eq_commonSkeletons_mul_sum_covariance (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s : 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) : ‖momentSignaturePhysicalIntegrand ρ ε m α β s 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))‖ * ∑ κ ∈ momentFullPairingFiber m s, primitiveCovarianceProduct ρ ε m (↑κ) v

Norm form of the common-skeleton factorization. Positivity of every covariance factor removes the absolute value from the complete primitive-pairing sum, while all Fourier characters have norm one.

theorem Anderson4D.scaled_momentSignaturePhysicalDensity_le_integral_of_pointwise (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (x : T4) (scale : ℝ) (hscale : 0 ≤ scale) (B : R324PhysicalRest m → ℝ) (hB : MeasureTheory.Integrable B (r324PhysicalRestMeasure m)) (hBnonneg : ∀ (r : R324PhysicalRest m), 0 ≤ B r) (hpointwise : ∀ (r : R324PhysicalRest m), scale * ‖r324Flatten (momentSignaturePhysicalIntegrand ρ ε m α β s) (x, r)‖ ≤ B r) : scale * momentSignaturePhysicalDensity ρ ε m α β s x ≤ ∫ (r : R324PhysicalRest m), B r ∂r324PhysicalRestMeasure m

Pointwise domination on the four inner physical variables passes to the canonical fixed-signature density. The proof also handles exceptional nonintegrable sections: mathlib's Bochner integral is then zero. This is the generic Tonelli bridge used after each concrete block collapse has produced its nonnegative inner majorant.