Joint integrability of the nested physical core

Paper: R-324 — §4.2 Step 3, the last integrability premise

The two-half physical core on the terminal carriers is (left residual)·(right residual)·(marked covariance). The two residual factors depend on disjoint coordinate groups, and the covariance factor is bounded at a fixed scale — so the fixed-scale integrability recipe in docs/R324_PAPER_PROOF.md applies verbatim: an integrable product across the two factors, times a bounded measurable weight.

Transporting along the measure-preserving terminal-to-nested equivalence then gives the premise exists_terminalPayload_physicalIntegral_le takes.

theorem Anderson4D.R324TwoHalfTerminalData.integrable_terminalMarkedPhysicalCore {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hε : 0 < ε) (hε1 : ε ≤ 1) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (L : ℝ) (x y z w : T4) (hleft : MeasureTheory.Integrable (fun (v : terminal.left.SurvivingCoordinate → T4) => ↑(terminal.left.residualIntegrand ρ ε x y (terminal.left.reconstruct v))) (MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure)) (hright : MeasureTheory.Integrable (fun (v : terminal.right.SurvivingCoordinate → T4) => ↑(terminal.right.residualIntegrand ρ ε z w (terminal.right.reconstruct v))) (MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure)) : MeasureTheory.Integrable (terminal.terminalMarkedPhysicalCore π selected L x y z w) ((MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure))

The two-half terminal physical core is jointly integrable.

The two half residual integrands live on disjoint coordinate groups, so their product is integrable on the product measure; the marked covariance is a bounded measurable weight.

theorem Anderson4D.R324TwoHalfTerminalData.integrable_initialNestedMarkedPhysicalCore {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hε : 0 < ε) (hε1 : ε ≤ 1) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (L : ℝ) (x y z w : T4) (hleft : MeasureTheory.Integrable (fun (v : terminal.left.SurvivingCoordinate → T4) => ↑(terminal.left.residualIntegrand ρ ε x y (terminal.left.reconstruct v))) (MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure)) (hright : MeasureTheory.Integrable (fun (v : terminal.right.SurvivingCoordinate → T4) => ↑(terminal.right.residualIntegrand ρ ε z w (terminal.right.reconstruct v))) (MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure)) : MeasureTheory.Integrable (terminal.initialNestedMarkedPhysicalCore π selected L x y z w) (MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure)

The nested physical core is jointly integrable.

Transport of the previous statement along the measure-preserving terminal-to-nested equivalence, using the pointwise losslessness initialNestedMarkedPhysicalCore_reindex. This is exactly the premise exists_terminalPayload_physicalIntegral_le and exists_r324InitialNestedContextFactorization_of_head take.