Endpoint-erased Phase-A boundary for R-324

Paper (4.19) integrates the four external variables before the nested cross-cut reductions which produce (4.20). Accordingly, this file only separates the two boundary slots of each completed within-half production chain from its endpoint-independent interior slots.

No absolute value is taken here. The signed kernels produced by the within-half Proposition 4.1 iteration remain untouched.

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.terminalScale {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : res.R324WithinHalfCertifiedAnalyticTrace scale) : Fin (m + 1) → ℝ

The actual scale family stored at the terminal constructor of a certified Phase-A trace.

Equations

• (Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.terminal res scale hremaining certificate).terminalScale = scale
• (Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.step res head tail hremaining scale internal nextScale nextCertificate next).terminalScale = next.terminalScale

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.terminalCertificate {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : res.R324WithinHalfCertifiedAnalyticTrace scale) : R324WithinHalfEdgeCertificate trace.terminalPrefix.state trace.terminalScale

The terminal edge certificate carried by a certified Phase-A trace.

def Anderson4D.R324WithinHalfResidualPrefix.terminalOutgoingEdgeSlot {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) : Fin (m + 1)

The active slot leaving the last surviving internal vertex. This is the outgoing external boundary slot of a completed half-chain.

Equations

• res.terminalOutgoingEdgeSlot hactive = Anderson4D.r324InternalVertexEdgeSlot (res.state.active.max' hactive)

theorem Anderson4D.R324WithinHalfResidualPrefix.terminalOutgoingEdgeSlot_ne_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) : res.terminalOutgoingEdgeSlot hactive ≠ 0

theorem Anderson4D.R324WithinHalfResidualPrefix.terminalOutgoingEdgeSlot_mem_activeEdgeSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) : res.terminalOutgoingEdgeSlot hactive ∈ res.activeEdgeSlots

def Anderson4D.R324WithinHalfResidualPrefix.endpointErasedActiveEdgeSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) : Finset (Fin (m + 1))

Active signed chain slots after deleting the incoming and outgoing external boundary slots.

Equations

• res.endpointErasedActiveEdgeSlots hactive = (res.activeEdgeSlots.erase 0).erase (res.terminalOutgoingEdgeSlot hactive)

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.endpointErasedSignedChain {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) (x y : T4) (v : Fin m → T4) : ℝ

The signed terminal interior chain. Its slot set contains neither external boundary edge. Endpoint independence of the displayed displacements is proved separately from this multiplicative ledger.

Equations

• res.endpointErasedSignedChain hactive x y v = ∏ edge ∈ res.endpointErasedActiveEdgeSlots hactive, res.residualChainEdgeFactor x y v edge

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.incomingBoundaryFactor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (x y : T4) (v : Fin m → T4) : ℝ

Incoming signed boundary factor of one completed half-chain.

Equations

• res.incomingBoundaryFactor x y v = res.residualChainEdgeFactor x y v 0

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.outgoingBoundaryFactor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) (x y : T4) (v : Fin m → T4) : ℝ

Outgoing signed boundary factor of one completed half-chain.

Equations

• res.outgoingBoundaryFactor hactive x y v = res.residualChainEdgeFactor x y v (res.terminalOutgoingEdgeSlot hactive)

theorem Anderson4D.R324WithinHalfResidualPrefix.residualChainProduct_eq_boundary_mul_endpointErased {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) (x y : T4) (v : Fin m → T4) : res.residualChainProduct x y v = res.incomingBoundaryFactor x y v * res.outgoingBoundaryFactor hactive x y v * res.endpointErasedSignedChain hactive x y v

Exact signed decomposition of a completed half-chain into its two external boundary factors and the endpoint-erased interior product.

def Anderson4D.R324WithinHalfResidualPrefix.endpointErasedScaleProduct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) (scale : Fin (m + 1) → ℝ) : ℝ

Product of the certified scales on the endpoint-erased active slots.

Equations

• res.endpointErasedScaleProduct hactive scale = ∏ edge ∈ res.endpointErasedActiveEdgeSlots hactive, scale edge

theorem Anderson4D.R324WithinHalfResidualPrefix.activeEdgeScaleProduct_eq_boundary_mul_endpointErased {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) (scale : Fin (m + 1) → ℝ) : ∏ edge ∈ res.activeEdgeSlots, scale edge = scale 0 * scale (res.terminalOutgoingEdgeSlot hactive) * res.endpointErasedScaleProduct hactive scale

The scale ledger uses exactly the same two-boundary slot partition as the signed chain identity.