The actual R-324 grouped core as a product of primitive block sums

The endpoint integrations leave two signed interior Green profiles and the complete covariance sum in one residual-refined fibre. This file keeps the two signed profiles outside the norm until the exact refined sum has been formed, then applies the multiplicity-free primitive-coordinate product bound from R324IntegratedMultiBlockCoordinates.

Realized refined representatives

theorem Anderson4D.momentRefinedContractionFiber_nonempty_of_mem {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (hr : r ∈ momentResidualChainSignaturesAt m s) : (momentRefinedContractionFiber m s r).Nonempty

Membership of a residual signature supplies an actual contraction in the corresponding refined fibre.

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

Canonical representative of a realized residual-refined fibre. Its value outside that realized fibre is irrelevant.

Equations

• Anderson4D.r324RefinedContractionRepresentative m s r = if hr : r ∈ Anderson4D.momentResidualChainSignaturesAt m s then Classical.choose ⋯ else default

theorem Anderson4D.r324RefinedContractionRepresentative_mem {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (hr : r ∈ momentResidualChainSignaturesAt m s) : r324RefinedContractionRepresentative m s r ∈ momentRefinedContractionFiber m s r

Norm of the actual grouped endpoint core

theorem Anderson4D.norm_r324RefinedEndpointCore_eq (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (eSkeleton : MomentContraction m) (v : Fin (2 * m) → T4) : ‖r324RefinedEndpointCore ρ ε m s r eSkeleton v‖ = ‖r324RenormalizedInteriorCore eSkeleton.fst fun (i : Fin m) => v (leftMomentIndex i)‖ * ‖r324RenormalizedInteriorCore eSkeleton.snd.fst fun (i : Fin m) => v (rightMomentIndex i)‖ * ∑ e ∈ momentRefinedContractionFiber m s r, primitiveCovarianceProduct ρ ε m (momentCombinedPairing e.fst e.snd.fst e.snd.snd) v

The norm of the genuine refined endpoint core is exactly the product of the two signed interior-profile norms and the nonnegative covariance fibre sum. The primitive-pairing sum remains inside the core until this identity.

noncomputable def Anderson4D.r324RefinedPrimitiveBlockProductMajorant (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (_s _r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (eSkeleton eBlocks : MomentContraction m) (v : Fin (2 * m) → T4) : ℝ

The concrete nonnegative product supplied to the successive block integrations for one realized refined fibre.

Equations

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

theorem Anderson4D.r324RefinedPrimitiveBlockProductMajorant_nonneg (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (eSkeleton eBlocks : MomentContraction m) (v : Fin (2 * m) → T4) : 0 ≤ r324RefinedPrimitiveBlockProductMajorant ρ ε m s r eSkeleton eBlocks v

theorem Anderson4D.norm_r324RefinedEndpointCore_le_primitiveBlockProduct (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (eSkeleton eBlocks : MomentContraction m) (heBlocks : eBlocks ∈ momentRefinedContractionFiber m s r) (v : Fin (2 * m) → T4) : ‖r324RefinedEndpointCore ρ ε m s r eSkeleton v‖ ≤ r324RefinedPrimitiveBlockProductMajorant ρ ε m s r eSkeleton eBlocks v

Actual grouped-core block-product bound. The only enlargement is from the realized refined fibre to all independent primitive coordinates on its fixed concrete schedule; nonnegativity makes the direction exact and no pairing-cardinality factor is paid.

All realized refined fibres

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

Sum of the genuine primitive-block product majorants over all residual schedules in one fixed within-half signature.

Equations

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

theorem Anderson4D.r324ResidualEndpointCoreNormSum_le_blockProductMajorant (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (eSkeleton : MomentContraction m) (v : Fin (2 * m) → T4) : r324ResidualEndpointCoreNormSum ρ ε m s eSkeleton v ≤ r324ResidualPrimitiveBlockProductMajorant ρ ε m s eSkeleton v

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

Complete block-product majorant after summing all realized within-half and residual signatures.

Equations

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

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