The terminal half chain, bounded leg by leg

Paper: R-324 — §4.2 Step 3, the chain side of the one-head factorization

At a terminal within-half prefix every scheduled subinterval has been removed, so no outgoing slot is reserved and the chain product is the plain product of the current edge kernels over the active slots. The slotwise certificate R324WithinHalfEdgeCertificate bounds each of those kernels by scale · |z|⁻², so the whole chain is bounded by a scale product times a product of |z|⁻² legs.

That product of legs is precisely what the nested one-head factorization needs on the chain side: the block's own edges plus the two boundary edges of ctx.connector, with the cut edge absent and compensated by the central gap factor (R324PaperCentralGap).

theorem Anderson4D.R324WithinHalfResidualPrefix.residualChainEdgeFactor_terminal {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hterminal : res.remaining = []) (x y : T4) (v : Fin m → T4) {edge : Fin (m + 1)} (hedge : edge ∈ res.activeEdgeSlots) : res.residualChainEdgeFactor x y v edge = res.state.edges edge (res.edgeDisplacement x y v edge)

At a terminal prefix no outgoing slot is reserved, so every active chain slot carries its current edge kernel.

theorem Anderson4D.R324WithinHalfResidualPrefix.residualChainProduct_terminal {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hterminal : res.remaining = []) (x y : T4) (v : Fin m → T4) : res.residualChainProduct x y v = ∏ edge ∈ res.activeEdgeSlots, res.state.edges edge (res.edgeDisplacement x y v edge)

The terminal chain product is the plain product over the active slots.

theorem Anderson4D.R324WithinHalfResidualPrefix.abs_residualChainProduct_le {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) {scale : Fin (m + 1) → ℝ} (cert : R324WithinHalfEdgeCertificate res.state scale) (hterminal : res.remaining = []) (x y : T4) (v : Fin m → T4) (hne : ∀ edge ∈ res.activeEdgeSlots, res.edgeDisplacement x y v edge ≠ 0) : |res.residualChainProduct x y v| ≤ (∏ edge ∈ res.activeEdgeSlots, scale edge) * ∏ edge ∈ res.activeEdgeSlots, invSqKer (res.edgeDisplacement x y v edge)

The terminal half chain, bounded leg by leg.

Every active slot's kernel obeys the slotwise certificate, so the chain product is dominated by the product of the slot scales times the product of the |z|⁻² legs at the corresponding displacements. The displacement hypothesis is the off-diagonal one the certificate needs.

theorem Anderson4D.R324WithinHalfResidualPrefix.abs_endpointErasedSignedChain_le {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) {scale : Fin (m + 1) → ℝ} (cert : R324WithinHalfEdgeCertificate res.state scale) (hterminal : res.remaining = []) (x y : T4) (v : Fin m → T4) (hne : ∀ edge ∈ res.endpointErasedActiveEdgeSlots hactive, res.edgeDisplacement x y v edge ≠ 0) : |res.endpointErasedSignedChain hactive x y v| ≤ res.endpointErasedScaleProduct hactive scale * ∏ edge ∈ res.endpointErasedActiveEdgeSlots hactive, invSqKer (res.edgeDisplacement x y v edge)

The endpoint-erased terminal half chain, bounded leg by leg.

Paper Step 3 starts only after the two external boundary slots of each half have been integrated out. On the resulting endpoint-erased slot set the same terminal edge certificate therefore gives the precise product bound needed by the nested cross-shell partition, without carrying either external endpoint edge into a connector.