Certificate-produced integrability for the full-pairing terminal block

The integrated full-pairing terminal identity is stated with the exact per-primitive-pairing integrability premise needed by finite-sum Fubini. For a budget/geometry adapter that premise is automatic: its terminal edge certificate supplies measurability, a positive scale, class-E membership, and the scaled off-diagonal bound for every heterogeneous internal edge.

The public scaled off-diagonal assembly theorem includes the order-one zero-dimensional case, so no extra lower-order hypothesis is needed here.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.integrable_terminalClosedIntegrand_section {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} (data : R324FullPairingBudgetTerminalAdapter budget) (hε : 0 < ε) (hε1 : ε ≤ 1) (κB : ↥(primitiveFullPairings (residualBlockOrder data.geometry.terminalData.terminal.2))) (z w : T4) : MeasureTheory.Integrable (fun (u : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.geometry.terminalData.terminal.2) (↑κB) (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges (primitiveAssemble (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ z w u)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2)) => paperMeasure)

Every closed primitive summand in the adapter's retained terminal block has an absolutely integrable internal section, pointwise in both endpoints. This includes terminal block order one.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.lamEps_pow_integral_terminalGroupedPrimitiveCore_eq_predecessor_mul_primitiveKernel_of_certificate {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} (data : R324FullPairingBudgetTerminalAdapter budget) (hε : 0 < ε) (hε1 : ε ≤ 1) (x z w : T4) : (lamEps lam ε ^ (2 * residualBlockOrder data.geometry.terminalData.terminal.2) * ∫ (u : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2) → T4), data.geometry.terminalGroupedPrimitiveCore x (primitiveAssemble (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ z w u) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2)) => paperMeasure) = data.geometry.trace.stopPrefix.state.edges (r324WithinHalfPredecessorSlot data.geometry.trace.stopPrefix.state data.geometry.terminalData.terminal) (x - z) * primitiveKernel ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges z w

The integrated terminal identity with its finite-sum Fubini premise discharged directly from the adapter's edge certificate.