One direct boundary leg at a completed R-324 half

When only the outgoing boundary slot is known to carry the free Green kernel, the inner endpoint integral can still be evaluated exactly. The incoming boundary factor is kept literal and is integrated only in the outer endpoint variable. Thus no Fubini exchange and no Fourier claim about the possibly updated incoming edge is used.

Left half

theorem Anderson4D.R324TwoHalfTerminalData.leftBoundaryModeCoefficient_eq_incomingIntegral_mul_translatedGreenMode {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hleft : terminal.left.state.active.Nonempty) (houtgoing : terminal.left.state.edges (terminal.left.terminalOutgoingEdgeSlot hleft) = greenFn) (α β : Z4) (vl : terminal.left.SurvivingCoordinate → T4) : terminal.leftBoundaryModeCoefficient hleft α β vl = (∫ (x : T4), charT4 α x * ↑(terminal.left.incomingBoundaryFactor x 0 (terminal.left.reconstruct vl)) ∂paperMeasure) * translatedGreenMode β (terminal.left.terminalOutgoingAnchor hleft (terminal.left.reconstruct vl))

Exact left-half factorization with only the outgoing terminal edge assumed to be a direct Green leg. The incoming integral remains the literal coefficient of the actual stored boundary kernel.

theorem Anderson4D.R324TwoHalfTerminalData.norm_leftBoundaryModeCoefficient_eq_incomingIntegral_mul_decay {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hleft : terminal.left.state.active.Nonempty) (houtgoing : terminal.left.state.edges (terminal.left.terminalOutgoingEdgeSlot hleft) = greenFn) (α β : Z4) (vl : terminal.left.SurvivingCoordinate → T4) : ‖terminal.leftBoundaryModeCoefficient hleft α β vl‖ = ‖∫ (x : T4), charT4 α x * ↑(terminal.left.incomingBoundaryFactor x 0 (terminal.left.reconstruct vl)) ∂paperMeasure‖ * paperSecondOrderModeDecay β

Exact norm ledger for the preceding one-direct-leg factorization.

theorem Anderson4D.R324TwoHalfTerminalData.norm_leftBoundaryModeCoefficient_le_incomingBound_mul_decay {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hleft : terminal.left.state.active.Nonempty) (houtgoing : terminal.left.state.edges (terminal.left.terminalOutgoingEdgeSlot hleft) = greenFn) (α β : Z4) (vl : terminal.left.SurvivingCoordinate → T4) (incomingBound : ℝ) (hincoming : ‖∫ (x : T4), charT4 α x * ↑(terminal.left.incomingBoundaryFactor x 0 (terminal.left.reconstruct vl)) ∂paperMeasure‖ ≤ incomingBound) : ‖terminal.leftBoundaryModeCoefficient hleft α β vl‖ ≤ incomingBound * paperSecondOrderModeDecay β

Any quantitative bound for the actual incoming boundary coefficient combines monotonically with the direct outgoing Green decay.

Right half

theorem Anderson4D.R324TwoHalfTerminalData.rightBoundaryModeCoefficient_eq_incomingIntegral_mul_translatedGreenMode {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hright : terminal.right.state.active.Nonempty) (houtgoing : terminal.right.state.edges (terminal.right.terminalOutgoingEdgeSlot hright) = greenFn) (α β : Z4) (vr : terminal.right.SurvivingCoordinate → T4) : terminal.rightBoundaryModeCoefficient hright α β vr = (∫ (z : T4), charT4 (-α) z * ↑(terminal.right.incomingBoundaryFactor z 0 (terminal.right.reconstruct vr)) ∂paperMeasure) * translatedGreenMode (-β) (terminal.right.terminalOutgoingAnchor hright (terminal.right.reconstruct vr))

Exact right-half factorization with only the outgoing terminal edge assumed to be a direct Green leg. The literal right-half modes are (-α,-β).

theorem Anderson4D.R324TwoHalfTerminalData.norm_rightBoundaryModeCoefficient_eq_incomingIntegral_mul_decay {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hright : terminal.right.state.active.Nonempty) (houtgoing : terminal.right.state.edges (terminal.right.terminalOutgoingEdgeSlot hright) = greenFn) (α β : Z4) (vr : terminal.right.SurvivingCoordinate → T4) : ‖terminal.rightBoundaryModeCoefficient hright α β vr‖ = ‖∫ (z : T4), charT4 (-α) z * ↑(terminal.right.incomingBoundaryFactor z 0 (terminal.right.reconstruct vr)) ∂paperMeasure‖ * paperSecondOrderModeDecay β

Exact norm ledger for the right one-direct-leg factorization, with sign invariance used only on the explicit outgoing Green mode.

theorem Anderson4D.R324TwoHalfTerminalData.norm_rightBoundaryModeCoefficient_le_incomingBound_mul_decay {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hright : terminal.right.state.active.Nonempty) (houtgoing : terminal.right.state.edges (terminal.right.terminalOutgoingEdgeSlot hright) = greenFn) (α β : Z4) (vr : terminal.right.SurvivingCoordinate → T4) (incomingBound : ℝ) (hincoming : ‖∫ (z : T4), charT4 (-α) z * ↑(terminal.right.incomingBoundaryFactor z 0 (terminal.right.reconstruct vr)) ∂paperMeasure‖ ≤ incomingBound) : ‖terminal.rightBoundaryModeCoefficient hright α β vr‖ ≤ incomingBound * paperSecondOrderModeDecay β

Any quantitative bound for the actual right incoming coefficient combines monotonically with the direct outgoing Green decay.