Paper §4.2, Step 3: nested-reduction handoff

Paper: R-324 — §4.2 Step 3

exists_terminalPayload_physicalIntegral_le is Step 3's end-to-end handoff from the physical initial nested integral to the endpoint- preserving terminal payload. Its three inputs are:

• R324ProperHeadSharpProvider — exists_r324ProperHeadSharpProvider, which is paper Step 3(c) ((4.4) on the block, then the elementary eight-dimensional integral);
• R324InitialNestedContextFactorization — exists_r324InitialNestedContextFactorization_of_head, using that every schedule block is some slot's marked block and that the Step 4 marking is inert at a nonpositive threshold;
• the joint integrability of the nested physical core — integrable_initialNestedMarkedPhysicalCore, whose two half premises come from root integrability propagated along the certified traces.

Root integrability holds at almost every endpoint pair because fixed-endpoint Green sections fail on exceptional diagonals.

theorem Anderson4D.eventually_integrable_terminalPrefix_residualIntegrand (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} {pairing : PartialPairing (Fin m)} {scale : Fin (m + 1) → ℝ} (trace : (R324WithinHalfResidualPrefix.initial ρ lam ε pairing).R324WithinHalfCertifiedAnalyticTrace scale) : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, MeasureTheory.Integrable (fun (v : trace.terminalPrefix.SurvivingCoordinate → T4) => ↑(trace.terminalPrefix.residualIntegrand ρ ε p.1 p.2 (trace.terminalPrefix.reconstruct v))) (MeasureTheory.Measure.pi fun (x : trace.terminalPrefix.SurvivingCoordinate) => paperMeasure)

Terminal half integrability at almost every endpoint pair.

The all-Green root is jointly L¹ in its endpoints and coordinates (integrable_initial_residualIntegrand_pair), so its fixed-endpoint section is integrable a.e.; the certified trace then propagates that to the terminal prefix.

theorem Anderson4D.exists_r324Step3_handoff_inputs (ρ : SmoothCutoff) {lam ε : ℝ} (hlam : 0 < lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) {m : ℕ} {κp κm : PartialPairing (Fin m)} (hmtrunc : m ≤ truncOrder ε) (π : ↥κp.singles ≃ ↥κm.singles) {leftScale rightScale : Fin (m + 1) → ℝ} (leftTrace : (R324WithinHalfResidualPrefix.initial ρ lam ε κp).R324WithinHalfCertifiedAnalyticTrace leftScale) (rightTrace : (R324WithinHalfResidualPrefix.initial ρ lam ε κm).R324WithinHalfCertifiedAnalyticTrace rightScale) (head : R324NestedCrossBlock κp κm π) (tail : List (R324NestedCrossBlock κp κm π)) (hremaining : (R324NestedCrossResidualPrefix.initial κp κm π).remaining = head :: tail) (L : ℝ) : ∃ (D : ℝ), 0 < D ∧ R324ProperHeadSharpProvider ρ lam ε D κp κm π ∧ ∀ᵐ (q : (T4 × T4) × T4 × T4) ∂(paperMeasure.prod paperMeasure).prod (paperMeasure.prod paperMeasure), ∃ (selected : R324ResidualCovarianceSlot κp), Nonempty (R324InitialNestedContextFactorization ρ lam ε κp κm π selected (R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace) L q.1.1 q.1.2 q.2.1 q.2.2)

Step 3's handoff, with every input supplied.

For almost every pair of external endpoint pairs, the nested context factorization exists at a slot chosen inside the schedule head, and the proper-head provider is unconditional. So exists_terminalPayload_physicalIntegral_le applies with no analytic hypothesis left.