Fixed-endpoint integrability at the R-322 terminal step

The final carrier collapse is a generalized primitive kernel whose edge family is the current heterogeneous edge state. Reachability supplies measurability of every such edge, while the quantitative edge certificate supplies its class-E membership and off-diagonal inverse-square bound. The scaled off-diagonal primitive-integrability theorem can therefore be applied directly at each fixed pair of endpoints.

In particular, no exceptional endpoint is selected from a joint Fubini statement: the result below holds pointwise in both endpoints.

theorem Anderson4D.R322AnalyticAbsorbedState.integrable_terminalClosedIntegrand_section {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} {scale : Fin (2 * q - 1) → ℝ} (ctx : R322AnalyticTerminalStepContext q hq) (hstate : R322AnalyticAbsorbedState ρ lam ε hq κ hκ ctx.state) (hcert : R322AnalyticEdgeCertificate ctx.state scale) (hε : 0 < ε) (hε1 : ε ≤ 1) (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.terminal.2))) (z w : T4) : MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder ctx.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.terminal.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.terminal.2) ⋯ z w v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.terminal.2 - 2)) => paperMeasure)

Every closed primitive summand in a reachable terminal carrier has an absolutely integrable internal section, pointwise in both fixed endpoints.

theorem Anderson4D.R322AnalyticAbsorbedState.terminalClosedIntegrand_hint {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} {scale : Fin (2 * q - 1) → ℝ} (ctx : R322AnalyticTerminalStepContext q hq) (hstate : R322AnalyticAbsorbedState ρ lam ε hq κ hκ ctx.state) (hcert : R322AnalyticEdgeCertificate ctx.state scale) (hε : 0 < ε) (hε1 : ε ≤ 1) (z : T4) (_hz : z ≠ 0) (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.terminal.2))) : MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder ctx.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.terminal.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.terminal.2) ⋯ z 0 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.terminal.2 - 2)) => paperMeasure)

The exact fixed-endpoint package consumed by the terminal-collapse identity. The nonzero endpoint assumption belongs to the subsequent Proposition 4.1 estimate; integrability itself also holds on the diagonal.