Endpoint independence after the R-324 Phase-A boundary split

After the incoming and outgoing slots of a completed within-half chain have been erased, both endpoints of every remaining production edge are internal variables. This file records that statement at the literal sparse-chain level and deduces endpoint independence of the signed interior product.

For the two terminal half states, the two endpoint-erased products are then packaged as one signed, endpoint-free core. The product of the two full terminal chains is exactly the four external boundary factors times that core. No absolute value is taken and no nested-cross reduction is started here.

theorem Anderson4D.R324WithinHalfResidualPrefix.mem_activeEdgeSlots_of_mem_endpointErased {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) {edge : Fin (m + 1)} (hedge : edge ∈ res.endpointErasedActiveEdgeSlots hactive) : edge ∈ res.activeEdgeSlots

An endpoint-erased slot is still an active production-chain slot.

theorem Anderson4D.R324WithinHalfResidualPrefix.ne_zero_of_mem_endpointErased {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) {edge : Fin (m + 1)} (hedge : edge ∈ res.endpointErasedActiveEdgeSlots hactive) : edge ≠ 0

An endpoint-erased slot is not the incoming external slot.

theorem Anderson4D.R324WithinHalfResidualPrefix.ne_terminalOutgoingEdgeSlot_of_mem_endpointErased {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) {edge : Fin (m + 1)} (hedge : edge ∈ res.endpointErasedActiveEdgeSlots hactive) : edge ≠ res.terminalOutgoingEdgeSlot hactive

An endpoint-erased slot is not the outgoing external slot.

theorem Anderson4D.R324WithinHalfResidualPrefix.exists_sourceInternalIndex_of_mem_endpointErased {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) {edge : Fin (m + 1)} (hedge : edge ∈ res.endpointErasedActiveEdgeSlots hactive) : ∃ (i : Fin m), edge.castSucc = varIdx i

The source of every endpoint-erased edge is an internal assembled coordinate.

theorem Anderson4D.R324WithinHalfResidualPrefix.exists_targetInternalIndex_of_mem_endpointErased {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) {edge : Fin (m + 1)} (hedge : edge ∈ res.endpointErasedActiveEdgeSlots hactive) : ∃ (i : Fin m), res.edgeSuccessor edge = varIdx i

The target of every endpoint-erased edge is an internal assembled coordinate. Removing the maximal active slot is exactly what rules out the terminal external vertex as the sparse successor.

theorem Anderson4D.R324WithinHalfResidualPrefix.edgeDisplacement_eq_zeroEndpoints_of_mem_endpointErased {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) (x y : T4) (v : Fin m → T4) {edge : Fin (m + 1)} (hedge : edge ∈ res.endpointErasedActiveEdgeSlots hactive) : res.edgeDisplacement x y v edge = res.edgeDisplacement 0 0 v edge

Every endpoint-erased edge reads the same displacement after both external endpoints are replaced by zero.

theorem Anderson4D.R324WithinHalfResidualPrefix.residualChainEdgeFactor_eq_zeroEndpoints_of_mem_endpointErased {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) (x y : T4) (v : Fin m → T4) {edge : Fin (m + 1)} (hedge : edge ∈ res.endpointErasedActiveEdgeSlots hactive) : res.residualChainEdgeFactor x y v edge = res.residualChainEdgeFactor 0 0 v edge

Each signed chain factor on an endpoint-erased slot is independent of the two external endpoints.

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

The complete signed endpoint-erased chain is independent of its two external endpoint arguments.

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

Endpoint-erased chains agree for any two choices of external endpoints.

The endpoint-free signed core of two terminal half states

theorem Anderson4D.R324TwoHalfTerminalData.left_active_nonempty_of_selected {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (selected : R324ResidualCovarianceSlot κp) : terminal.left.state.active.Nonempty

The selected left single witnesses that the left certified terminal half still has an active internal vertex.

theorem Anderson4D.R324TwoHalfTerminalData.right_active_nonempty_of_selected {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) : terminal.right.state.active.Nonempty

The matched right single witnesses that the right certified terminal half still has an active internal vertex.

noncomputable def Anderson4D.R324TwoHalfTerminalData.endpointErasedSignedTerminalCore {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (vl : terminal.left.SurvivingCoordinate → T4) (vr : terminal.right.SurvivingCoordinate → T4) : ℝ

Product of the two signed terminal half-chain interiors, evaluated with all four external endpoints erased. In the certified route, terminal is ofCertifiedTraces leftTrace rightTrace.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.R324TwoHalfTerminalData.terminalChainProducts_eq_fourBoundary_mul_endpointErasedCore {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (x y z w : T4) (vl : terminal.left.SurvivingCoordinate → T4) (vr : terminal.right.SurvivingCoordinate → T4) : terminal.left.residualChainProduct x y (terminal.left.reconstruct vl) * terminal.right.residualChainProduct z w (terminal.right.reconstruct vr) = terminal.left.incomingBoundaryFactor x y (terminal.left.reconstruct vl) * terminal.left.outgoingBoundaryFactor ⋯ x y (terminal.left.reconstruct vl) * terminal.right.incomingBoundaryFactor z w (terminal.right.reconstruct vr) * terminal.right.outgoingBoundaryFactor ⋯ z w (terminal.right.reconstruct vr) * terminal.endpointErasedSignedTerminalCore π selected vl vr

Exact signed two-half terminal decomposition: the two full production chains are the four external boundary factors times one endpoint-free interior core.