Cross-factor projection at an exceptional incoming stop

The cross-cut primitive factor reads only the final residual carrier. Hence, when the left within-half trace stops immediately before an exceptional incoming head, that factor may already be read on the coordinates surviving after the retained head. The right half remains at its literal initial carrier.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.r324ResidualPrimitiveSumProduct_eq_afterHeadProjection {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κp initialScale) (π : ↥κp.singles ≃ ↥κm.singles) (vl : (initial ρ lam ε κp).SurvivingCoordinate → T4) (vr : (initial ρ lam ε κm).SurvivingCoordinate → T4) : r324ResidualPrimitiveSumProduct ρ ε κp κm π (r324TwoHalfRootDoubledReconstruct (initial ρ lam ε κp) (initial ρ lam ε κm) (vl, vr)) = r324ResidualPrimitiveSumProduct ρ ε κp κm π (r324TwoHalfRootDoubledReconstruct (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯) (initial ρ lam ε κm) (((data.trace.stopPrefix.splitSurvivingPiMeasurableEquiv data.terminal data.suffix ⋯) (data.trace.stopProjection vl)).2, vr))

Projecting the left initial tuple through a certified incoming stop and then discarding the retained head does not change the cross-cut primitive sum. This is the one-sided analogue of terminal projection: the right half is untouched, while the retained left head is harmless because every final residual vertex lies outside every extraction block.