Terminal joint-integrability producer for R-324

This file supplies the two analytic ingredients needed for the premise isolated in R324EndpointJointIntegrabilityAdapter. A completed within-half trace is a finite heterogeneous Haar path. Its terminal edge certificate makes every edge genuinely L¹; the complete residual primitive sum is a bounded measurable finite product at positive mollification scale. A successor module combines the two half paths with that bounded factor and performs the remaining product-measure regrouping.

The path argument below is local because the corresponding general theorem in R322AnalyticReachableIntegrability is private.

Local heterogeneous Haar-path theorem

The ordered sparse chain of a completed half

Genuine joint integrability of one completed sparse half-chain

theorem Anderson4D.R324WithinHalfResidualPrefix.integrable_terminalResidualChainProduct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hremaining : res.remaining = []) (scale : Fin (m + 1) → ℝ) (hcert : R324WithinHalfEdgeCertificate res.state scale) : MeasureTheory.Integrable (fun (p : T4 × T4 × (res.SurvivingCoordinate → T4)) => res.residualChainProduct p.1 p.2.1 (res.reconstruct p.2.2)) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)))

A terminal slotwise inverse-square certificate gives joint L¹ control of the literal completed half-chain in both endpoints and all surviving coordinates.

Bounded measurable grouped residual primitive sum

theorem Anderson4D.SmoothCutoff.measurable_r324ResidualPrimitiveSumProduct (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Measurable (r324ResidualPrimitiveSumProduct ρ ε κp κm π)

theorem Anderson4D.SmoothCutoff.exists_norm_r324ResidualPrimitiveSumProduct_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : ∃ (bound : ℝ), 0 ≤ bound ∧ ∀ (v : Fin (2 * m) → T4), ‖r324ResidualPrimitiveSumProduct ρ ε κp κm π v‖ ≤ bound