Exact final-head geometry for a full R-324 pairing

After all proper within-half blocks have been collapsed, a full pairing retains one terminal block. This module identifies the complete sparse geometry of that last head before any endpoint estimate is applied.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminal_block_eq_active {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) : data.terminalData.terminal.2 = data.trace.stopPrefix.state.active

The retained terminal block is exactly the active carrier at the singleton stop.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminal_predecessorSlot_eq_zero {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) : r324WithinHalfPredecessorSlot data.trace.stopPrefix.state data.terminalData.terminal = 0

At the singleton stop, the terminal head has no surviving internal vertex strictly to its left. Its sparse predecessor is therefore the incoming external slot.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminal_outgoingSlot_eq_last {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) : (data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).outgoingSlot = Fin.last (2 * q)

The terminal head leaves through the last edge slot of the internal chain.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminal_edgeSuccessor_outgoing_eq_last {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) : data.trace.stopPrefix.edgeSuccessor (data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).outgoingSlot = Fin.last (2 * q + 1)

The sparse successor after the terminal outgoing slot is the external right endpoint.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminal_headPredecessorPoint_eq_left {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) (x y : T4) (v : (data.trace.stopPrefix.afterHead data.terminalData.terminal [] ⋯).SurvivingCoordinate → T4) : data.trace.stopPrefix.headPredecessorPoint data.terminalData.terminal [] ⋯ x y v = x

The predecessor point of the final local block is the external left endpoint.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminal_headSuccessorPoint_eq_right {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) (x y : T4) (v : (data.trace.stopPrefix.afterHead data.terminalData.terminal [] ⋯).SurvivingCoordinate → T4) : data.trace.stopPrefix.headSuccessorPoint data.terminalData.terminal [] ⋯ x y v = y

The successor point of the final local block is the external right endpoint.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminal_outgoingEdge_eq_greenFn {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) : data.trace.stopPrefix.state.edges (data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).outgoingSlot = greenFn

The named edge leaving the retained terminal head is still the free Green kernel.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminal_afterHead_active_eq_empty {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) : (data.trace.stopPrefix.afterHead data.terminalData.terminal [] ⋯).state.active = ∅

Once the retained terminal block is removed, no internal vertex survives.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminal_afterHead_activeEdgeSlots_eq_singleton {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) : (data.trace.stopPrefix.afterHead data.terminalData.terminal [] ⋯).activeEdgeSlots = {0}

After deleting the final block, the only active sparse edge slot is the incoming external slot.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminal_headOuterChainProductAfter_eq_one {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) (x y : T4) (v : Fin (2 * q) → T4) : data.trace.stopPrefix.headOuterChainProductAfter data.terminalData.terminal [] ⋯ x y v = 1

No ordinary outer sparse-chain factor remains outside the final local head.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminal_headOuterFactor_eq_one {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) (x y : T4) (v : (data.trace.stopPrefix.afterHead data.terminalData.terminal [] ⋯).SurvivingCoordinate → T4) : data.trace.stopPrefix.headOuterFactor data.terminalData.terminal [] ⋯ ρ ε x y v = 1

At the terminal singleton stop, every factor outside the genuine final local block is exactly one.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.terminal_residualIntegrand_reconstruct_split_eq_rawLocal {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) (x y : T4) (t : Fin (2 * residualBlockOrder data.terminalData.terminal.2) → T4) (v : (data.trace.stopPrefix.afterHead data.terminalData.terminal [] ⋯).SurvivingCoordinate → T4) : data.trace.stopPrefix.residualIntegrand ρ ε x y (data.trace.stopPrefix.reconstruct ((data.trace.stopPrefix.splitSurvivingPiMeasurableEquiv data.terminalData.terminal [] ⋯).symm (t, v))) = (data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder (data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯).step.2)) => t j - y

Exact final-head reduction: after all proper blocks have been consumed, the whole singleton-stop residual integrand is the translated raw local integrand joining the two external endpoints. No absolute value or endpoint estimate has been taken.