The full/full endpoint half at the Step-1 terminal seam

This module closes the exact finite-sum, endpoint-Fubini, and proper-prefix trace part of the full/full branch. Starting from the complete endpoint signature fibre, the coupling-weighted half is transported to the retained terminal raw-local block of the certified Proposition 4.1 trace.

The terminal trace carries scaled edge kernels. The final conversion to R324Step1Reduction therefore additionally requires an exact normalization ledger for those edges; the declarations below deliberately expose that seam without replacing it by a target-shaped estimate.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeLastTrace.weightedIntegrableAlong_one_of_integrable {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {res : R324WithinHalfResidualPrefix rho lam eps pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeLastTrace terminal res scale) (x y : T4) (hroot : MeasureTheory.Integrable (fun (v : res.SurvivingCoordinate → T4) => ↑(res.residualIntegrand rho eps x y (res.reconstruct v))) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) : WeightedIntegrableAlong x y trace fun (x : trace.stopPrefix.SurvivingCoordinate → T4) => 1

Root integrability propagates through a trace stopped immediately before its retained terminal block, discharging the unit-outer-factor premise used by the exact proper-prefix iteration.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeLastTrace.integrable_stopPrefix_residualIntegrand_of_integrable {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {res : R324WithinHalfResidualPrefix rho lam eps pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeLastTrace terminal res scale) (x y : T4) (hroot : MeasureTheory.Integrable (fun (v : res.SurvivingCoordinate → T4) => ↑(res.residualIntegrand rho eps x y (res.reconstruct v))) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) : MeasureTheory.Integrable (fun (v : trace.stopPrefix.SurvivingCoordinate → T4) => ↑(trace.stopPrefix.residualIntegrand rho eps x y (trace.stopPrefix.reconstruct v))) (MeasureTheory.Measure.pi fun (x : trace.stopPrefix.SurvivingCoordinate) => paperMeasure)

The same root premise gives honest integrability of the stopped residual section needed by the terminal coordinate split.

The complete endpoint fibre as one grouped root integral

theorem Anderson4D.R324WithinHalfResidualPrefix.sum_deterministicFullHalfIntegral_eq_integral_initialGroupedResidual (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) (heps1 : eps ≤ 1) (lam : ℝ) (q : ℕ) (alpha beta : Z4) (kappa : PartialPairing (Fin (2 * q))) (hkappa : kappa.IsFull) : ∑ tau : ReductionEndpointFiberAt kappa, deterministicFullHalfIntegral rho eps (2 * q) alpha beta ↑tau = ∫ (p : T4 × T4 × (Fin (2 * q) → T4)), charT4 alpha p.1 * charT4 beta p.2.1 * ↑((initial rho lam eps kappa).residualIntegrand rho eps p.1 p.2.1 p.2.2) ∂paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure))

The finite endpoint-signature sum may be moved under the genuine joint half integral before any norm is taken. Pointwise, the resulting signed sum is exactly the grouped initial residual consumed by the certified trace.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.terminalRawLocalFourierIntegral {rho : SmoothCutoff} {C lam eps K A : ℝ} {q : ℕ} {kappa : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace kappa} (data : R324FullPairingBudgetTerminalAdapter budget) (alpha beta : Z4) : ℂ

The literal terminal raw-local Fourier integral left after all proper within-half blocks have been consumed. The empty post-terminal coordinate integral is retained exactly as in the certified Fubini theorem.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.lamEps_pow_sum_deterministicFullHalfIntegral_eq_terminalRawLocal {rho : SmoothCutoff} {C lam eps K A : ℝ} {q : ℕ} {kappa : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace kappa} (data : R324FullPairingBudgetTerminalAdapter budget) (hkappa : kappa.IsFull) (heps : 0 < eps) (heps1 : eps ≤ 1) (alpha beta : Z4) : ↑(lamEps lam eps) ^ (2 * q) * ∑ tau : ReductionEndpointFiberAt kappa, deterministicFullHalfIntegral rho eps (2 * q) alpha beta ↑tau = data.terminalRawLocalFourierIntegral alpha beta

Exact full-half terminal producer.

The complete endpoint-signature half sum, with its full coupling weight, is exactly the Fourier integral of the retained terminal raw-local block. All finite grouping and every Fubini premise are discharged from the proved joint integrability of the original deterministic half.

Uniform construction of the exact terminal producer

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.exists_fullPairing_terminalRawLocal_producer (rho : SmoothCutoff) : ∃ (supportConstant : ℝ) (C : ℝ) (K : ℝ) (A : ℝ), 0 < supportConstant ∧ 0 < C ∧ 0 < K ∧ 1 ≤ A ∧ ∀ (lam eps : ℝ) (q : ℕ) (kappa : PartialPairing (Fin (2 * q))), 0 < lam → 0 < eps → eps ≤ 1 → 1 ≤ |Real.log eps| → q ≤ truncOrder eps → 1 ≤ q → kappa.IsFull → ∃ (budget : R324FullPairingBudgetStopTrace kappa) (data : R324FullPairingBudgetTerminalAdapter budget), ∀ (alpha beta : Z4), ↑(lamEps lam eps) ^ (2 * q) * ∑ tau : ReductionEndpointFiberAt kappa, deterministicFullHalfIntegral rho eps (2 * q) alpha beta ↑tau = data.terminalRawLocalFourierIntegral alpha beta

Proposition 4.1 at the paper truncation constructs the complete adapter and the preceding exact identity uniformly. Thus no finite-sum, Fubini, or proper-prefix hypothesis remains in the full-pairing half.

The sole remaining representation seam

def Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.TerminalRemovalRepresentation {rho : SmoothCutoff} {C lam eps K A : ℝ} {q : ℕ} {kappa : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace kappa} (data : R324FullPairingBudgetTerminalAdapter budget) (Citer : ℝ) (alpha beta : Z4) : Prop

The literal statement that the scaled terminal trace is represented by the successive-removal vocabulary of R324PaperIteration.

This is deliberately an equality to r324RemovalAmplitude, together with the structural and integrability facts consumed by that construction. It does not assume a bound on the desired half sum.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.exists_step1Reduction_of_terminalRemovalRepresentation (rho : SmoothCutoff) : ∃ (Citer : ℝ), 0 < Citer ∧ ∀ {C lam eps K A : ℝ} {q : ℕ} {kappa : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace kappa} (data : R324FullPairingBudgetTerminalAdapter budget), 0 < lam → 0 < eps → eps ≤ 1 → 1 ≤ |Real.log eps| → kappa.IsFull → ∀ (alpha beta : Z4), data.TerminalRemovalRepresentation Citer alpha beta → R324Step1Reduction rho lam eps (2 * q) alpha beta Citer (↑(lamEps lam eps) ^ (2 * q) * ∑ tau : ReductionEndpointFiberAt kappa, deterministicFullHalfIntegral rho eps (2 * q) alpha beta ↑tau)

Once the terminal edge state has the literal successive-removal representation, the exact producer above and the proved §4.1 iteration close R324Step1Reduction without any further analytic estimate.