Slot-zero-erased residual cores carrying an incoming Fourier phase

After the incoming endpoint has been Fourier integrated, production slot zero no longer contributes an ordinary edge factor. Its Fourier character is instead carried by incomingPhaseAnchor. This file records that representation pointwise.

The erased core is also evaluated against an arbitrary family of named edges. The corresponding congruence theorem makes precise that the value does not inspect edge slot zero. For an ordinary later head, whose predecessor is not slot zero, the usual local/outer factorization survives verbatim after erasing slot zero.

A slot-zero-free evaluator

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

One sparse-chain factor evaluated with an arbitrary named-edge family.

Equations

• res.residualChainEdgeFactorWithEdges edges x y v edge = if edge ∈ res.activeEdgeSlots then if edge ∈ res.remainingOutgoingSlots then 1 else edges edge (res.edgeDisplacement x y v edge) else 1

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

The ordinary sparse-chain product with production slot zero deleted.

Equations

• res.incomingErasedResidualChainProductWithEdges edges x y v = ∏ edge ∈ Finset.univ.erase 0, res.residualChainEdgeFactorWithEdges edges x y v edge

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.residualStepDifferenceWithEdges {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (edges : Fin (m + 1) → T4 → ℝ) (x y : T4) (v : Fin m → T4) (step : R322ExtractionStep m) : ℝ

One remaining signed difference evaluated with an arbitrary named-edge family.

Equations

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

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

Product of all remaining signed differences, evaluated with an arbitrary named-edge family.

Equations

• res.residualDifferenceProductWithEdges edges x y v = (List.map (res.residualStepDifferenceWithEdges edges x y v) res.remaining).prod

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

Complete slot-zero-erased residual core evaluated with an arbitrary named-edge family.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.r324InternalVertexEdgeSlot_ne_zero {m : ℕ} (i : Fin m) : r324InternalVertexEdgeSlot i ≠ 0

Slot zero is not an internal-vertex edge slot.

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingErasedResidualIntegrandWithEdges_congr {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (edges edges' : Fin (m + 1) → T4 → ℝ) (hoff : ∀ (edge : Fin (m + 1)), edge ≠ 0 → edges edge = edges' edge) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : Fin m → T4) : res.incomingErasedResidualIntegrandWithEdges edges ρ' ε' x y v = res.incomingErasedResidualIntegrandWithEdges edges' ρ' ε' x y v

The erased evaluator only inspects named edges away from slot zero.

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingErasedResidualIntegrandWithEdges_update_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (edges : Fin (m + 1) → T4 → ℝ) (replacement : T4 → ℝ) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : Fin m → T4) : res.incomingErasedResidualIntegrandWithEdges (Function.update edges 0 replacement) ρ' ε' x y v = res.incomingErasedResidualIntegrandWithEdges edges ρ' ε' x y v

In particular, replacing the named edge at slot zero has no effect on the erased residual core.

The actual reachable-state core

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

The ordinary residual chain with its incoming production slot deleted.

Equations

• res.incomingErasedResidualChainProduct x y v = ∏ edge ∈ Finset.univ.erase 0, res.residualChainEdgeFactor x y v edge

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

The complete reachable-state residual integrand after deleting the ordinary factor at production slot zero.

Equations

• res.incomingErasedResidualIntegrand ρ' ε' x y v = res.incomingErasedResidualChainProduct x y v * res.residualDifferenceProduct x y v * res.residualPrimitiveProduct ρ' ε' v

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingErasedResidualIntegrand_eq_withEdges {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : Fin m → T4) : res.incomingErasedResidualIntegrand ρ' ε' x y v = res.incomingErasedResidualIntegrandWithEdges res.state.edges ρ' ε' x y v

The concrete erased core is the arbitrary-edge evaluator at the reachable state's named-edge family.

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingErasedResidualIntegrand_eq_withEdges_of_eq_off_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (edges : Fin (m + 1) → T4 → ℝ) (hoff : ∀ (edge : Fin (m + 1)), edge ≠ 0 → edges edge = res.state.edges edge) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : Fin m → T4) : res.incomingErasedResidualIntegrandWithEdges edges ρ' ε' x y v = res.incomingErasedResidualIntegrand ρ' ε' x y v

Usable extensional form of independence from state.edges 0.

theorem Anderson4D.R324WithinHalfResidualPrefix.residualChainProduct_eq_zero_mul_incomingErased {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (x y : T4) (v : Fin m → T4) : res.residualChainProduct x y v = res.residualChainEdgeFactor x y v 0 * res.incomingErasedResidualChainProduct x y v

Exact product erasure at slot zero.

theorem Anderson4D.R324WithinHalfResidualPrefix.residualIntegrand_eq_zero_mul_incomingErased {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : Fin m → T4) : res.residualIntegrand ρ' ε' x y v = res.residualChainEdgeFactor x y v 0 * res.incomingErasedResidualIntegrand ρ' ε' x y v

The full residual integrand is the slot-zero edge factor times the slot-zero-erased core.

Fourier phase carried by the erased core

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.incomingPhasedResidualDensity {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (coefficient : ℂ) (k : Z4) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : res.SurvivingCoordinate → T4) : ℂ

A coefficient times the transported incoming Fourier character and the slot-zero-erased residual core.

Equations

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

Ordinary heads preserve the erased representation

theorem Anderson4D.R324WithinHalfResidualPrefix.zero_not_mem_headChainSlots_of_predecessor_ne_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head ≠ 0) : 0 ∉ res.headChainSlots head tail hremaining

If the current predecessor is not slot zero, every local ordinary-chain slot is retained by erase 0.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.incomingErasedHeadOuterChainProductAfter {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (x y : T4) (v : Fin m → T4) : ℝ

The outer chain after an ordinary head, with slot zero still erased.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.incomingErasedHeadOuterFactor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : ℝ

All post-head factors outside an ordinary local head, with slot zero deleted from the ordinary-chain part.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingErasedHeadOuterChainProductBefore_reconstruct_split {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : ∏ edge ∈ (Finset.univ \ res.headChainSlots head tail hremaining).erase 0, res.residualChainEdgeFactor x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) edge = res.incomingErasedHeadOuterChainProductAfter head tail hremaining x y ((res.afterHead head tail hremaining).reconstruct v)

The erased outer chain is independent of the head coordinates and is unchanged by an ordinary head collapse.

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingErasedHeadOuterChainProductAfter_eq_headOuter_of_eq_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head = 0) (x y : T4) (v : Fin m → T4) : res.incomingErasedHeadOuterChainProductAfter head tail hremaining x y v = res.headOuterChainProductAfter head tail hremaining x y v

When the current predecessor is slot zero, the already-outer chain does not contain slot zero, so erasing it once more is vacuous.

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingErasedHeadOuterFactor_eq_headOuterFactor_of_eq_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head = 0) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : res.incomingErasedHeadOuterFactor head tail hremaining ρ' ε' x y v = res.headOuterFactor head tail hremaining ρ' ε' x y v

Consequently the erased and ordinary outer factors coincide at a head fed by slot zero.

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingErasedResidualChainProduct_reconstruct_split_of_ne_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head ≠ 0) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : res.incomingErasedResidualChainProduct x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) = res.residualChainEdgeFactor x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) (r324WithinHalfPredecessorSlot res.state head) * res.headInternalChainProduct head tail hremaining x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) * res.incomingErasedHeadOuterChainProductAfter head tail hremaining x y ((res.afterHead head tail hremaining).reconstruct v)

Pointwise ordinary-head factorization of the erased pre-head chain.

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingErasedResidualChainProduct_reconstruct_split_of_eq_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head = 0) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : res.incomingErasedResidualChainProduct x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) = res.headInternalChainProduct head tail hremaining x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) * res.incomingErasedHeadOuterChainProductAfter head tail hremaining x y ((res.afterHead head tail hremaining).reconstruct v)

At a head fed by slot zero, erasure removes precisely the predecessor factor and leaves the internal local chain followed by the erased outer chain.

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingErasedHeadLocalCore_reconstruct_split {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : ↑(res.headInternalChainProduct head tail hremaining x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) * res.residualStepDifference x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) head * r322ExtractionBlockPrimitiveSum ρ' ε' pairing (res.headContext head tail hremaining).blockIndex (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v)))) = (res.headContext head tail hremaining).incomingErasedTranslatedRawLocalCore ρ' ε' (res.headSuccessorPoint head tail hremaining x y v) t

The three retained local factors at a slot-zero head are exactly the existing translated incoming-erased raw local core.

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingErasedResidualIntegrand_reconstruct_split_of_eq_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head = 0) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : ↑(res.incomingErasedResidualIntegrand ρ' ε' x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v)))) = (res.headContext head tail hremaining).incomingErasedTranslatedRawLocalCore ρ' ε' (res.headSuccessorPoint head tail hremaining x y v) t * ↑(res.headOuterFactor head tail hremaining ρ' ε' x y v)

Exact pointwise entry interface for the exceptional branch: after slot-zero erasure, the retained head is the translated erased raw local core and every post-head factor is the ordinary outer factor.

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingErasedResidualIntegrand_reconstruct_split_of_ne_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head ≠ 0) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : res.incomingErasedResidualIntegrand ρ' ε' x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) = res.headLocalFactor head tail hremaining ρ' ε' x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) * res.incomingErasedHeadOuterFactor head tail hremaining ρ' ε' x y v

Pointwise ordinary-head split of the complete erased pre-head core.

theorem Anderson4D.R324WithinHalfResidualPrefix.afterHead_incomingErasedResidualIntegrand_of_ne_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head ≠ 0) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : (res.afterHead head tail hremaining).incomingErasedResidualIntegrand ρ' ε' x y ((res.afterHead head tail hremaining).reconstruct v) = (res.afterHead head tail hremaining).residualChainEdgeFactor x y ((res.afterHead head tail hremaining).reconstruct v) (r324WithinHalfPredecessorSlot res.state head) * res.incomingErasedHeadOuterFactor head tail hremaining ρ' ε' x y v

Pointwise factorization of the complete erased post-head core.

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingPhasedResidualDensity_reconstruct_split_of_ne_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head ≠ 0) (coefficient : ℂ) (k : Z4) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : res.incomingPhasedResidualDensity coefficient k ρ' ε' x y ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v)) = coefficient * charT4 k ((res.afterHead head tail hremaining).incomingPhaseAnchor x y v) * ↑(res.headLocalFactor head tail hremaining ρ' ε' x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v)))) * ↑(res.incomingErasedHeadOuterFactor head tail hremaining ρ' ε' x y v)

The phase and the erased core both have the ordinary local/outer pointwise split.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalStopFourierDensity_eq_incomingPhasedResidualDensity {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {C K : ℝ} {initialScale : Fin (m + 1) → ℝ} {Ω : Type u_1} (data : R324IncomingExceptionalStopTraceAssembly pairing initialScale) (k : Z4) (y : Ω → T4) (postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (ω : Ω) (t : Fin (2 * residualBlockOrder data.terminal.2) → T4) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) : data.incomingExceptionalStopFourierDensity k y postOuter (ω, t, v) = data.trace.stopPrefix.incomingPhasedResidualDensity (↑(paperSecondOrderModeDecay k) * postOuter ω v) k ρ ε 0 (y ω) ((data.trace.stopPrefix.splitSurvivingPiMeasurableEquiv data.terminal data.suffix ⋯).symm (t, v))

The exact exceptional-stop Fourier density is the phased, slot-zero- erased residual density. The arbitrary post factor is absorbed into the pointwise scalar coefficient; the retained head and the complete suffix remain uncollapsed.