Exact grouped-half bridge to the full-pairing terminal block

The certified within-half trace acts on the complete primitive-pairing fibre grouped by the extraction blocks of a full pairing. It therefore starts from R324WithinHalfResidualPrefix.initial, whose primitive factor is a product of finite primitive-pairing sums, rather than from one fixed detIntegrand summand.

This module records the smallest exact analytic bridge needed after that finite grouping. It reindexes the standard Fin (2 * q) carrier to the initial sparse carrier, runs every proper block with the exact lamEps ledger, and then applies Fubini once at the singleton terminal stop. The result is the genuine signed terminal rawLocalIntegrand; no norm or estimate is taken.

Honest finite grouping of the frozen half terms

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.sum_endpointFiber_detIntegrand_eq_initialGroupedResidual {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (hκ : κ.IsFull) (x y : T4) (v : Fin (2 * q) → T4) : ∑ τ : ReductionEndpointFiberAt κ, ↑(detIntegrand ρ ε (2 * q) (↑τ) (assemble x y v)) = ↑((initial ρ lam ε κ).residualIntegrand ρ ε x y v)

A full endpoint-signature fibre of frozen detIntegrand summands is pointwise exactly the initial grouped residual consumed by the trace.

This is the necessary finite grouping before Proposition 4.1 is applied: the theorem does not identify one fixed summand with the grouped residual.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.sum_endpointFiber_integral_detIntegrand_eq_integral_initialGroupedResidual {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (hκ : κ.IsFull) (x y : T4) (hint : ∀ (τ : ReductionEndpointFiberAt κ), MeasureTheory.Integrable (fun (v : Fin (2 * q) → T4) => ↑(detIntegrand ρ ε (2 * q) (↑τ) (assemble x y v))) (MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure)) : (∑ τ : ReductionEndpointFiberAt κ, ∫ (v : Fin (2 * q) → T4), ↑(detIntegrand ρ ε (2 * q) (↑τ) (assemble x y v)) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure) = ∫ (v : Fin (2 * q) → T4), ↑((initial ρ lam ε κ).residualIntegrand ρ ε x y v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure

Integral form of the finite grouping. The hypotheses are exactly the termwise Bochner-integrability premises required to commute the finite sum with the internal integral.

Proper-prefix and terminal bridges

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.initial_remainingOrder_eq {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (hκ : κ.IsFull) : (initial ρ lam ε κ).remainingOrder = q

For a full pairing, the initial grouped residual carries exactly the ambient perturbative order q.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.lamEps_pow_integral_initialGroupedResidual_eq_stopResidual {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} (data : R324FullPairingBudgetTerminalAdapter budget) (hκ : κ.IsFull) (x y : T4) (hweighted : R324WithinHalfStopBeforeLastTrace.WeightedIntegrableAlong x y data.geometry.trace fun (x : data.geometry.trace.stopPrefix.SurvivingCoordinate → T4) => 1) : (↑(lamEps lam ε) ^ (2 * q) * ∫ (v : Fin (2 * q) → T4), ↑((initial ρ lam ε κ).residualIntegrand ρ ε x y v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure) = ↑(lamEps lam ε) ^ (2 * residualBlockOrder data.geometry.terminalData.terminal.2) * ∫ (v : data.geometry.trace.stopPrefix.SurvivingCoordinate → T4), ↑(data.geometry.trace.stopPrefix.residualIntegrand ρ ε x y (data.geometry.trace.stopPrefix.reconstruct v)) ∂MeasureTheory.Measure.pi fun (x : data.geometry.trace.stopPrefix.SurvivingCoordinate) => paperMeasure

Exact proper-prefix iteration from the standard internal carrier to the singleton terminal stop.

The hypothesis is precisely the weighted integrability consumed by the certified trace. The terminal residual itself is left untouched.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.lamEps_pow_integral_initialGroupedResidual_eq_terminalRawLocal {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} (data : R324FullPairingBudgetTerminalAdapter budget) (hκ : κ.IsFull) (x y : T4) (hweighted : R324WithinHalfStopBeforeLastTrace.WeightedIntegrableAlong x y data.geometry.trace fun (x : data.geometry.trace.stopPrefix.SurvivingCoordinate → T4) => 1) (hstop : MeasureTheory.Integrable (fun (v : data.geometry.trace.stopPrefix.SurvivingCoordinate → T4) => ↑(data.geometry.trace.stopPrefix.residualIntegrand ρ ε x y (data.geometry.trace.stopPrefix.reconstruct v))) (MeasureTheory.Measure.pi fun (x : data.geometry.trace.stopPrefix.SurvivingCoordinate) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * q) * ∫ (v : Fin (2 * q) → T4), ↑((initial ρ lam ε κ).residualIntegrand ρ ε x y v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure) = ↑(lamEps lam ε) ^ (2 * residualBlockOrder data.geometry.terminalData.terminal.2) * ∫ (t : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2) → T4), ∫ (_v : (data.geometry.trace.stopPrefix.afterHead data.geometry.terminalData.terminal [] ⋯).SurvivingCoordinate → T4), ↑((data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).step.2)) => t j - y) ∂MeasureTheory.Measure.pi fun (x : (data.geometry.trace.stopPrefix.afterHead data.geometry.terminalData.terminal [] ⋯).SurvivingCoordinate) => paperMeasure ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2)) => paperMeasure

Exact terminal Fubini normal form. The only additional premise is the honest integrability of the stopped residual section needed to split its surviving coordinates. The post-terminal coordinate integral is retained literally (its carrier is empty), so this theorem makes no hidden probability-measure simplification.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.lamEps_pow_sum_endpointFiber_integral_detIntegrand_eq_terminalRawLocal {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} (data : R324FullPairingBudgetTerminalAdapter budget) (hκ : κ.IsFull) (x y : T4) (hint : ∀ (τ : ReductionEndpointFiberAt κ), MeasureTheory.Integrable (fun (v : Fin (2 * q) → T4) => ↑(detIntegrand ρ ε (2 * q) (↑τ) (assemble x y v))) (MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure)) (hweighted : R324WithinHalfStopBeforeLastTrace.WeightedIntegrableAlong x y data.geometry.trace fun (x : data.geometry.trace.stopPrefix.SurvivingCoordinate → T4) => 1) (hstop : MeasureTheory.Integrable (fun (v : data.geometry.trace.stopPrefix.SurvivingCoordinate → T4) => ↑(data.geometry.trace.stopPrefix.residualIntegrand ρ ε x y (data.geometry.trace.stopPrefix.reconstruct v))) (MeasureTheory.Measure.pi fun (x : data.geometry.trace.stopPrefix.SurvivingCoordinate) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * q) * ∑ τ : ReductionEndpointFiberAt κ, ∫ (v : Fin (2 * q) → T4), ↑(detIntegrand ρ ε (2 * q) (↑τ) (assemble x y v)) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure) = ↑(lamEps lam ε) ^ (2 * residualBlockOrder data.geometry.terminalData.terminal.2) * ∫ (t : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2) → T4), ∫ (_v : (data.geometry.trace.stopPrefix.afterHead data.geometry.terminalData.terminal [] ⋯).SurvivingCoordinate → T4), ↑((data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).step.2)) => t j - y) ∂MeasureTheory.Measure.pi fun (x : (data.geometry.trace.stopPrefix.afterHead data.geometry.terminalData.terminal [] ⋯).SurvivingCoordinate) => paperMeasure ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2)) => paperMeasure

The complete fixed-endpoint bridge from the honest finite sum of frozen half terms to the signed terminal raw-local density. This is the closest valid analogue of a bridge for one detIntegrand: Proposition 4.1 acts only after the endpoint-signature fibre has been grouped.