Structural consumers for direct R-324 boundary branches

The completed two-half package already records that each within-half analytic schedule has been fully processed. This file combines that certificate with the structural direct-boundary geometry:

• a direct outgoing edge supplies a canonical nonempty terminal carrier and the one-leg coefficient factorization;
• if the first internal vertex also survives, the incoming edge is still the free Green kernel and the full direct/direct coefficient follows.

No raw-Green edge equality or active-carrier witness is added as an interface hypothesis.

Canonical active witnesses in the direct outgoing branches

theorem Anderson4D.R324TwoHalfTerminalData.leftDirectOutgoingActive {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hm : 0 < m) (hdirect : Fin.last m ∉ extractedRightEdges κp) : terminal.left.state.active.Nonempty

The left direct-outgoing condition canonically supplies the nonempty terminal carrier required by the boundary-coefficient definitions.

theorem Anderson4D.R324TwoHalfTerminalData.rightDirectOutgoingActive {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hm : 0 < m) (hdirect : Fin.last m ∉ extractedRightEdges κm) : terminal.right.state.active.Nonempty

Right-copy counterpart of leftDirectOutgoingActive.

Left half

theorem Anderson4D.R324TwoHalfTerminalData.leftBoundaryModeCoefficient_eq_oneLeg_of_directOutgoing {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hm : 0 < m) (hdirect : Fin.last m ∉ extractedRightEdges κp) (α β : Z4) (vl : terminal.left.SurvivingCoordinate → T4) : terminal.leftBoundaryModeCoefficient ⋯ α β vl = (∫ (x : T4), charT4 α x * ↑(terminal.left.incomingBoundaryFactor x 0 (terminal.left.reconstruct vl)) ∂paperMeasure) * translatedGreenMode β (terminal.left.terminalOutgoingAnchor ⋯ (terminal.left.reconstruct vl))

A completed left direct-outgoing branch automatically satisfies the one-leg exact factorization. The incoming boundary integral is retained literally.

theorem Anderson4D.R324TwoHalfTerminalData.norm_leftBoundaryModeCoefficient_eq_oneLeg_of_directOutgoing {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hm : 0 < m) (hdirect : Fin.last m ∉ extractedRightEdges κp) (α β : Z4) (vl : terminal.left.SurvivingCoordinate → T4) : ‖terminal.leftBoundaryModeCoefficient ⋯ α β vl‖ = ‖∫ (x : T4), charT4 α x * ↑(terminal.left.incomingBoundaryFactor x 0 (terminal.left.reconstruct vl)) ∂paperMeasure‖ * paperSecondOrderModeDecay β

Norm form of the structurally discharged left one-leg branch.

theorem Anderson4D.R324TwoHalfTerminalData.leftBoundaryModeCoefficient_eq_of_directBoundary {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hm : 0 < m) (hdirect : Fin.last m ∉ extractedRightEdges κp) (hfirst : ⟨0, hm⟩ ∈ finalActive κp) (α β : Z4) (vl : terminal.left.SurvivingCoordinate → T4) : terminal.leftBoundaryModeCoefficient ⋯ α β vl = translatedGreenMode α (terminal.left.terminalIncomingAnchor (terminal.left.reconstruct vl)) * translatedGreenMode β (terminal.left.terminalOutgoingAnchor ⋯ (terminal.left.reconstruct vl))

If the first left internal vertex also survives the completed schedule, both actual boundary slots are direct Green edges.

theorem Anderson4D.R324TwoHalfTerminalData.norm_leftBoundaryModeCoefficient_eq_of_directBoundary {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hm : 0 < m) (hdirect : Fin.last m ∉ extractedRightEdges κp) (hfirst : ⟨0, hm⟩ ∈ finalActive κp) (α β : Z4) (vl : terminal.left.SurvivingCoordinate → T4) : ‖terminal.leftBoundaryModeCoefficient ⋯ α β vl‖ = paperSecondOrderModeDecay α * paperSecondOrderModeDecay β

Norm form of the completed left direct/direct branch.

Right half

theorem Anderson4D.R324TwoHalfTerminalData.rightBoundaryModeCoefficient_eq_oneLeg_of_directOutgoing {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hm : 0 < m) (hdirect : Fin.last m ∉ extractedRightEdges κm) (α β : Z4) (vr : terminal.right.SurvivingCoordinate → T4) : terminal.rightBoundaryModeCoefficient ⋯ α β vr = (∫ (z : T4), charT4 (-α) z * ↑(terminal.right.incomingBoundaryFactor z 0 (terminal.right.reconstruct vr)) ∂paperMeasure) * translatedGreenMode (-β) (terminal.right.terminalOutgoingAnchor ⋯ (terminal.right.reconstruct vr))

A completed right direct-outgoing branch automatically satisfies the one-leg exact factorization, with the literal (-α,-β) modes.

theorem Anderson4D.R324TwoHalfTerminalData.norm_rightBoundaryModeCoefficient_eq_oneLeg_of_directOutgoing {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hm : 0 < m) (hdirect : Fin.last m ∉ extractedRightEdges κm) (α β : Z4) (vr : terminal.right.SurvivingCoordinate → T4) : ‖terminal.rightBoundaryModeCoefficient ⋯ α β vr‖ = ‖∫ (z : T4), charT4 (-α) z * ↑(terminal.right.incomingBoundaryFactor z 0 (terminal.right.reconstruct vr)) ∂paperMeasure‖ * paperSecondOrderModeDecay β

Norm form of the structurally discharged right one-leg branch.

theorem Anderson4D.R324TwoHalfTerminalData.rightBoundaryModeCoefficient_eq_of_directBoundary {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hm : 0 < m) (hdirect : Fin.last m ∉ extractedRightEdges κm) (hfirst : ⟨0, hm⟩ ∈ finalActive κm) (α β : Z4) (vr : terminal.right.SurvivingCoordinate → T4) : terminal.rightBoundaryModeCoefficient ⋯ α β vr = translatedGreenMode (-α) (terminal.right.terminalIncomingAnchor (terminal.right.reconstruct vr)) * translatedGreenMode (-β) (terminal.right.terminalOutgoingAnchor ⋯ (terminal.right.reconstruct vr))

If the first right internal vertex also survives the completed schedule, both actual boundary slots are direct Green edges.

theorem Anderson4D.R324TwoHalfTerminalData.norm_rightBoundaryModeCoefficient_eq_of_directBoundary {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hm : 0 < m) (hdirect : Fin.last m ∉ extractedRightEdges κm) (hfirst : ⟨0, hm⟩ ∈ finalActive κm) (α β : Z4) (vr : terminal.right.SurvivingCoordinate → T4) : ‖terminal.rightBoundaryModeCoefficient ⋯ α β vr‖ = paperSecondOrderModeDecay α * paperSecondOrderModeDecay β

Norm form of the completed right direct/direct branch.