Physical fixed-signature fibers for R-324

Paper §4.2 fixes the within-half extraction data in (4.18), sums every contraction with that data, and only then takes an absolute value. This file makes that operation concrete for the frozen deterministic moment sum.

The analytic ledger is joint integrability on the actual product space, not pointwise integrability of every section. This distinction is essential: fixed-endpoint Green sections may fail to be integrable on exceptional diagonals, whereas Tonelli--Fubini gives the required section statements almost everywhere from joint integrability.

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

The contraction entities realizing one fixed within-half extraction signature.

Equations

• Anderson4D.momentContractionFiber m s = {e : Anderson4D.MomentContraction m | Anderson4D.momentContractionSignature e = s}

@[simp]

theorem Anderson4D.mem_momentContractionFiber {m : ℕ} {s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} {e : MomentContraction m} : e ∈ momentContractionFiber m s ↔ momentContractionSignature e = s

@[reducible, inline]

abbrev Anderson4D.R324PhysicalRest (m : ℕ) : Type

The four inner physical variables in the order used by (4.18).

Equations

• Anderson4D.R324PhysicalRest m = (Anderson4D.T4 × Anderson4D.T4 × Anderson4D.T4 × (Fin (2 * m) → Anderson4D.T4))

@[reducible, inline]

abbrev Anderson4D.R324PhysicalPoint (m : ℕ) : Type

The full physical product space, right-associated in the frozen integration order (x,y,z,w,v).

Equations

• Anderson4D.R324PhysicalPoint m = (Anderson4D.T4 × Anderson4D.R324PhysicalRest m)

noncomputable def Anderson4D.r324PhysicalRestMeasure (m : ℕ) : MeasureTheory.Measure (R324PhysicalRest m)

Product measure on the four inner physical variables.

Equations

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

noncomputable def Anderson4D.r324PhysicalMeasure (m : ℕ) : MeasureTheory.Measure (R324PhysicalPoint m)

Product measure on all five physical variable groups.

Equations

• Anderson4D.r324PhysicalMeasure m = Anderson4D.paperMeasure.prod (Anderson4D.r324PhysicalRestMeasure m)

instance Anderson4D.instSFiniteR324PhysicalRestMeasure (m : ℕ) : MeasureTheory.SFinite (r324PhysicalRestMeasure m)

instance Anderson4D.instSFiniteR324PhysicalMeasure (m : ℕ) : MeasureTheory.SFinite (r324PhysicalMeasure m)

def Anderson4D.r324Flatten {m : ℕ} (f : T4 → T4 → T4 → T4 → (Fin (2 * m) → T4) → ℂ) (p : R324PhysicalPoint m) : ℂ

Flatten a five-variable R-324 integrand onto its genuine product space.

Equations

• Anderson4D.r324Flatten f p = f p.1 p.2.1 p.2.2.1 p.2.2.2.1 p.2.2.2.2

def Anderson4D.R324MomentIntegrable (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (e : MomentContraction m) : Prop

Joint product-space integrability of one frozen contraction term.

Equations

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

theorem Anderson4D.r324_integral_product_eq_five {m : ℕ} (f : T4 → T4 → T4 → T4 → (Fin (2 * m) → T4) → ℂ) (hf : MeasureTheory.Integrable (r324Flatten f) (r324PhysicalMeasure m)) : ∫ (p : R324PhysicalPoint m), r324Flatten f p ∂r324PhysicalMeasure m = ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), ∫ (v : Fin (2 * m) → T4), f x y z w v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure

Joint integrability gives the frozen five-fold iterated integral. Every inner use of Fubini is made only on the almost-everywhere integrable section supplied by the preceding product-space hypothesis.

theorem Anderson4D.integral_r324Flatten_deterministicMomentIntegrand (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (e : MomentContraction m) (hint : R324MomentIntegrable ρ ε m α β e) : ∫ (p : R324PhysicalPoint m), r324Flatten (deterministicMomentIntegrand ρ ε m α β e.fst e.snd.fst e.snd.snd) p ∂r324PhysicalMeasure m = deterministicMomentContractionTerm ρ ε m α β e

Product-space form of one concrete contraction term.

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

The genuine physical integrand obtained by summing all contractions in one fixed signature fiber before taking a norm.

Equations

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

theorem Anderson4D.integrable_r324Flatten_momentSignaturePhysicalIntegrand (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hint : ∀ e ∈ momentContractionFiber m s, R324MomentIntegrable ρ ε m α β e) : MeasureTheory.Integrable (r324Flatten (momentSignaturePhysicalIntegrand ρ ε m α β s)) (r324PhysicalMeasure m)

The flattened fixed-signature integrand is jointly integrable whenever each concrete contraction in that finite fiber is.

theorem Anderson4D.integral_momentSignaturePhysicalIntegrand (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hint : ∀ e ∈ momentContractionFiber m s, R324MomentIntegrable ρ ε m α β e) : ∫ (p : R324PhysicalPoint m), r324Flatten (momentSignaturePhysicalIntegrand ρ ε m α β s) p ∂r324PhysicalMeasure m = ∑ e ∈ momentContractionFiber m s, deterministicMomentContractionTerm ρ ε m α β e

Fixed-signature form of (4.18): the product integral of the concrete signature integrand is exactly the sum of the frozen contraction terms.

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

Four inner product-space integrations of a fixed signature fiber, leaving the first external point as the explicit density variable.

Equations

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

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

The canonical nonnegative physical density for a signature fiber. The norm is outside both the contraction sum and all four inner physical integrations.

Equations

• Anderson4D.momentSignaturePhysicalDensity ρ ε m α β s x = ‖Anderson4D.momentSignatureOuterSection ρ ε m α β s x‖

theorem Anderson4D.momentSignaturePhysicalDensity_nonneg (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (x : T4) : 0 ≤ momentSignaturePhysicalDensity ρ ε m α β s x

theorem Anderson4D.integrable_momentSignaturePhysicalDensity (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hint : ∀ e ∈ momentContractionFiber m s, R324MomentIntegrable ρ ε m α β e) : MeasureTheory.Integrable (momentSignaturePhysicalDensity ρ ε m α β s) paperMeasure

The canonical physical density is genuinely integrable from joint product-space integrability; no exceptional section is promoted to a pointwise hypothesis.

theorem Anderson4D.momentContractionFiber_norm_le_density_integral (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hint : ∀ e ∈ momentContractionFiber m s, R324MomentIntegrable ρ ε m α β e) : ‖∑ e ∈ momentContractionFiber m s, deterministicMomentContractionTerm ρ ε m α β e‖ ≤ ∫ (x : T4), momentSignaturePhysicalDensity ρ ε m α β s x ∂paperMeasure

The norm of a fixed signature fiber is bounded by the integral of its canonical physical density. This is the exact triangle inequality used after the cancellation-preserving contraction sum has been formed.

structure Anderson4D.MomentPhysicalFiberReductionData (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) : Type

The fully constructed physical part of the fixed-signature R-324 reduction. Unlike MomentFiberReductionData, it stops immediately before the Proposition 4.1 pointwise majorization and contains no target bound.

• density : Finset (Fin (2 * m)) × Finset (Fin (2 * m)) → T4 → ℝ
• density_eq (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : s ∈ momentContractionSignatures m → self.density s = momentSignaturePhysicalDensity ρ ε m α β s
• density_integrable (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : s ∈ momentContractionSignatures m → MeasureTheory.Integrable (self.density s) paperMeasure
• density_nonneg (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : s ∈ momentContractionSignatures m → ∀ (x : T4), 0 ≤ self.density s x
• fiber_le_density_integral (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : s ∈ momentContractionSignatures m → ‖∑ e : MomentContraction m with momentContractionSignature e = s, deterministicMomentContractionTerm ρ ε m α β e‖ ≤ ∫ (x : T4), self.density s x ∂paperMeasure

noncomputable def Anderson4D.momentPhysicalFiberReductionData (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (hint : ∀ (e : MomentContraction m), R324MomentIntegrable ρ ε m α β e) : MomentPhysicalFiberReductionData ρ ε m α β

Construct the complete physical fixed-signature data directly from joint integrability of the frozen contraction terms.

Equations

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

def Anderson4D.MomentPhysicalFiberReductionData.toMomentFiberReductionData {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} {primitiveConstant supportConstant : ℝ} (d : MomentPhysicalFiberReductionData ρ ε m α β) (hdom : ∀ s ∈ momentContractionSignatures m, ∀ (x : T4), |lamEps lam ε| ^ (2 * m) * d.density s x ≤ primitiveInsertedMajorant primitiveConstant lam ε supportConstant m x) : MomentFiberReductionData ρ lam ε m α β primitiveConstant supportConstant

Compatibility adapter to the pointwise-density interface.

The concrete paper proof does not use this adapter: the remaining variable of momentSignaturePhysicalDensity is an absolute translation coordinate, not the relative primitive-block endpoint governed by Proposition 4.1. R324PrimitiveIterationClosure instead performs the external integrations first and records the resulting scalar relative-endpoint bound.

Equations

• d.toMomentFiberReductionData hdom = { density := d.density, density_integrable := ⋯, density_nonneg := ⋯, fiber_le_density_integral := ⋯, pointwise_fiber_domination := hdom }