Endpoint-integrated residual bridge for R-324

Paper §4.2 integrates the four external variables after the signed within-half collapses and before the nested cross reductions. At that stage the four boundary legs are the actual kernels stored in the two terminal edge states; in general they are no longer raw Green kernels. Consequently the raw-Green coefficient formulas in R324EndpointAggregate cannot be substituted pointwise here.

This file supplies the exact structural bridge needed by the paper order:

• the four-boundary split is parameterized by explicit nonempty terminal active carriers, with no selected primitive slot;
• the endpoint-free core retains the complete residual primitive-pairing product as one grouped factor;
• for each fixed terminal internal coordinate, the four genuine boundary legs are integrated against the external Fourier modes before any norm is taken;
• the resulting density is transported to the literal initial nested-cross carrier.

Two analytic interfaces are explicit. First, the fixed moment term integrates the internal coordinates inside the four endpoint integrals, so a joint-integrability/Fubini theorem is still required before the pointwise endpoint identity below can be substituted into that term. Second, the present edge certificate records only measurability, symmetry, and inverse-square domination; those data alone do not imply Fourier decay. The required coefficient estimate must instead use the exact reachable outer-Green structure (or a genuinely stronger Fourier certificate) together with the endpoint cancellation of the paper. Only after both steps may the nested core be split into its two outer connectors and current complete primitive head.

A selected-slot-free endpoint-erased terminal core

theorem Anderson4D.R324TwoHalfTerminalData.left_active_nonempty_of_singles_nonempty {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hsingles : κp.singles.Nonempty) : terminal.left.state.active.Nonempty

A nonempty left residual-single carrier gives a nonempty completed left half, without choosing a distinguished primitive-sum term.

theorem Anderson4D.R324TwoHalfTerminalData.right_active_nonempty_of_singles_nonempty {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (hsingles : κp.singles.Nonempty) : terminal.right.state.active.Nonempty

The residual-single equivalence transports nonemptiness to the completed right half.

noncomputable def Anderson4D.R324TwoHalfTerminalData.endpointErasedSignedTerminalCoreOfActive {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (vl : terminal.left.SurvivingCoordinate → T4) (vr : terminal.right.SurvivingCoordinate → T4) : ℝ

Product of the two signed endpoint-erased half chains, parameterized only by explicit nonempty active-carrier witnesses. These witnesses are available in every nonempty residual-cross branch and do not select a summand from the complete primitive covariance sum.

Equations

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

theorem Anderson4D.R324TwoHalfTerminalData.terminalChainProducts_eq_fourBoundary_mul_endpointErasedOfActive {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (x y z w : T4) (vl : terminal.left.SurvivingCoordinate → T4) (vr : terminal.right.SurvivingCoordinate → T4) : terminal.left.residualChainProduct x y (terminal.left.reconstruct vl) * terminal.right.residualChainProduct z w (terminal.right.reconstruct vr) = terminal.left.incomingBoundaryFactor x y (terminal.left.reconstruct vl) * terminal.left.outgoingBoundaryFactor hleft x y (terminal.left.reconstruct vl) * terminal.right.incomingBoundaryFactor z w (terminal.right.reconstruct vr) * terminal.right.outgoingBoundaryFactor hright z w (terminal.right.reconstruct vr) * terminal.endpointErasedSignedTerminalCoreOfActive hleft hright vl vr

Exact signed four-boundary split without a distinguished residual covariance slot.

noncomputable def Anderson4D.R324TwoHalfTerminalData.endpointErasedResidualSumTerminalCore {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) : ℂ

Endpoint-free two-half core with the complete residual primitive sum still grouped. No termwise absolute value is introduced.

Equations

• terminal.endpointErasedResidualSumTerminalCore π hleft hright p = ↑(terminal.endpointErasedSignedTerminalCoreOfActive hleft hright p.1 p.2) * terminal.residualSumCrossFactor π p.1 p.2

theorem Anderson4D.R324TwoHalfTerminalData.terminalResidualSumPhysicalCore_eq_fourBoundary_mul_endpointErased {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (x y z w : T4) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) : terminal.terminalResidualSumPhysicalCore π x y z w p = ↑(terminal.left.incomingBoundaryFactor x y (terminal.left.reconstruct p.1)) * ↑(terminal.left.outgoingBoundaryFactor hleft x y (terminal.left.reconstruct p.1)) * ↑(terminal.right.incomingBoundaryFactor z w (terminal.right.reconstruct p.2)) * ↑(terminal.right.outgoingBoundaryFactor hright z w (terminal.right.reconstruct p.2)) * terminal.endpointErasedResidualSumTerminalCore π hleft hright p

The genuine terminal residual-sum density is exactly its four actual signed boundary legs times the endpoint-free, complete primitive-sum core.

Exact integration of the genuine four boundary legs

noncomputable def Anderson4D.R324TwoHalfTerminalData.leftBoundaryModeIntegrand {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hleft : terminal.left.state.active.Nonempty) (α β : Z4) (vl : terminal.left.SurvivingCoordinate → T4) (x y : T4) : ℂ

The two genuine left-half boundary legs with their external Fourier characters. The kernels are read from the terminal edge state rather than replaced by raw Green kernels.

Equations

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

noncomputable def Anderson4D.R324TwoHalfTerminalData.rightBoundaryModeIntegrand {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hright : terminal.right.state.active.Nonempty) (α β : Z4) (vr : terminal.right.SurvivingCoordinate → T4) (z w : T4) : ℂ

The two genuine right-half boundary legs in the mode order (-α,-β) of paper (4.18).

Equations

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

noncomputable def Anderson4D.R324TwoHalfTerminalData.leftBoundaryModeCoefficient {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hleft : terminal.left.state.active.Nonempty) (α β : Z4) (vl : terminal.left.SurvivingCoordinate → T4) : ℂ

Fourier coefficient of the two actual boundary legs of the completed left half.

Equations

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

noncomputable def Anderson4D.R324TwoHalfTerminalData.rightBoundaryModeCoefficient {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hright : terminal.right.state.active.Nonempty) (α β : Z4) (vr : terminal.right.SurvivingCoordinate → T4) : ℂ

Fourier coefficient of the two actual boundary legs of the completed right half.

Equations

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

noncomputable def Anderson4D.R324TwoHalfTerminalData.externalModeResidualSumIntegrand {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (α β : Z4) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) (x y z w : T4) : ℂ

The full external-mode terminal density before endpoint integration.

Equations

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

theorem Anderson4D.R324TwoHalfTerminalData.externalModeResidualSumIntegrand_eq_boundary_mul_core {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (α β : Z4) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) (x y z w : T4) : terminal.externalModeResidualSumIntegrand π α β p x y z w = terminal.leftBoundaryModeIntegrand hleft α β p.1 x y * terminal.rightBoundaryModeIntegrand hright α β p.2 z w * terminal.endpointErasedResidualSumTerminalCore π hleft hright p

Pointwise separation into the two genuine boundary-mode payloads and one endpoint-free complete residual core.

noncomputable def Anderson4D.R324TwoHalfTerminalData.endpointIntegratedResidualDensity {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (α β : Z4) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) : ℂ

Density on the terminal product carrier after all four external variables have been integrated. This is the object that may enter the nested two-connector reduction.

Equations

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

theorem Anderson4D.R324TwoHalfTerminalData.integral_externalModeResidualSumIntegrand {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (α β : Z4) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) : ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), terminal.externalModeResidualSumIntegrand π α β p x y z w ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure = terminal.endpointIntegratedResidualDensity π hleft hright α β p

Exact endpoint-first identity at each fixed terminal internal coordinate. The complete primitive sum remains inside the last factor. This theorem does not interchange the endpoint integrals with the internal coordinate integral of the frozen moment term.

theorem Anderson4D.R324TwoHalfTerminalData.norm_endpointIntegratedResidualDensity {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (α β : Z4) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) : ‖terminal.endpointIntegratedResidualDensity π hleft hright α β p‖ = ‖terminal.leftBoundaryModeCoefficient hleft α β p.1‖ * ‖terminal.rightBoundaryModeCoefficient hright α β p.2‖ * ‖terminal.endpointErasedResidualSumTerminalCore π hleft hright p‖

Exact norm ledger after endpoint integration. No triangle inequality has been applied to the complete primitive residual core.

theorem Anderson4D.R324TwoHalfTerminalData.norm_endpointIntegratedResidualDensity_le {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (α β : Z4) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) (leftMajorant rightMajorant : ℝ) (hleftMajorant : ‖terminal.leftBoundaryModeCoefficient hleft α β p.1‖ ≤ leftMajorant) (hrightMajorant : ‖terminal.rightBoundaryModeCoefficient hright α β p.2‖ ≤ rightMajorant) : ‖terminal.endpointIntegratedResidualDensity π hleft hright α β p‖ ≤ leftMajorant * rightMajorant * ‖terminal.endpointErasedResidualSumTerminalCore π hleft hright p‖

Abstract majorant interface for the endpoint Fourier step. It keeps the complete residual core grouped and isolates the two coefficient estimates which must be supplied from exact reachable outer-Green structure or from a stronger Fourier certificate; the current inverse-square edge certificate is not sufficient.

Transport to the initial nested-cross carrier

noncomputable def Anderson4D.R324TwoHalfTerminalData.initialNestedEndpointIntegratedResidualDensity {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (α β : Z4) (v : terminal.NestedCoordinate π → T4) : ℂ

Endpoint-integrated density on the literal initial nested coordinate carrier.

Equations

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

@[simp]

theorem Anderson4D.R324TwoHalfTerminalData.initialNestedEndpointIntegratedResidualDensity_reindex {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (α β : Z4) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) : terminal.initialNestedEndpointIntegratedResidualDensity π hleft hright α β ((terminal.terminalProductPiMeasurableEquivNested π) p) = terminal.endpointIntegratedResidualDensity π hleft hright α β p

theorem Anderson4D.R324TwoHalfTerminalData.integral_endpointIntegratedResidualDensity_eq_initialNested {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (α β : Z4) : ∫ (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)), terminal.endpointIntegratedResidualDensity π hleft hright α β p ∂(MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure) = ∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedEndpointIntegratedResidualDensity π hleft hright α β v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure

Measure-preserving transport of the endpoint-integrated density to the exact carrier consumed by the nested-cross reduction.