Direct two-leg Fourier coefficients at a completed R-324 half #
When both boundary slots of one completed half-chain still carry the free Green kernel, the two external Fourier integrations factor exactly into two translated Green modes. This supplies the direct/direct boundary case without taking a norm of the endpoint-erased residual core.
theorem
Anderson4D.R324TwoHalfTerminalData.leftBoundaryModeCoefficient_eq_translatedGreenModes_of_direct
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
(hleft : terminal.left.state.active.Nonempty)
(hincoming : terminal.left.state.edges 0 = greenFn)
(houtgoing : terminal.left.state.edges (terminal.left.terminalOutgoingEdgeSlot hleft) = greenFn)
(α β : Z4)
(vl : terminal.left.SurvivingCoordinate → T4)
:
terminal.leftBoundaryModeCoefficient hleft α β vl = translatedGreenMode α (terminal.left.terminalIncomingAnchor (terminal.left.reconstruct vl)) * translatedGreenMode β (terminal.left.terminalOutgoingAnchor hleft (terminal.left.reconstruct vl))
Exact two-leg coefficient on the left completed half when both actual boundary slots are direct Green edges.
theorem
Anderson4D.R324TwoHalfTerminalData.norm_leftBoundaryModeCoefficient_eq_of_direct
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
(hleft : terminal.left.state.active.Nonempty)
(hincoming : terminal.left.state.edges 0 = greenFn)
(houtgoing : terminal.left.state.edges (terminal.left.terminalOutgoingEdgeSlot hleft) = greenFn)
(α β : Z4)
(vl : terminal.left.SurvivingCoordinate → T4)
:
‖terminal.leftBoundaryModeCoefficient hleft α β vl‖ = paperSecondOrderModeDecay α * paperSecondOrderModeDecay β
Norm of the preceding exact coefficient.
theorem
Anderson4D.R324TwoHalfTerminalData.rightBoundaryModeCoefficient_eq_translatedGreenModes_of_direct
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
(hright : terminal.right.state.active.Nonempty)
(hincoming : terminal.right.state.edges 0 = greenFn)
(houtgoing : terminal.right.state.edges (terminal.right.terminalOutgoingEdgeSlot hright) = greenFn)
(α β : Z4)
(vr : terminal.right.SurvivingCoordinate → T4)
:
terminal.rightBoundaryModeCoefficient hright α β vr = translatedGreenMode (-α) (terminal.right.terminalIncomingAnchor (terminal.right.reconstruct vr)) * translatedGreenMode (-β) (terminal.right.terminalOutgoingAnchor hright (terminal.right.reconstruct vr))
Exact two-leg coefficient on the right completed half. Its modes are
the literal (-α,-β) modes from paper (4.18).
theorem
Anderson4D.R324TwoHalfTerminalData.norm_rightBoundaryModeCoefficient_eq_of_direct
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
(hright : terminal.right.state.active.Nonempty)
(hincoming : terminal.right.state.edges 0 = greenFn)
(houtgoing : terminal.right.state.edges (terminal.right.terminalOutgoingEdgeSlot hright) = greenFn)
(α β : Z4)
(vr : terminal.right.SurvivingCoordinate → T4)
:
‖terminal.rightBoundaryModeCoefficient hright α β vr‖ = paperSecondOrderModeDecay α * paperSecondOrderModeDecay β
Norm of the direct right-half coefficient, simplified using frequency sign invariance of the Green multiplier.