Cross-factor projection for a direct incoming half #
These are the two coordinate identities used by the direct-incoming branches of paper Step 4(A). The residual primitive factor is supported on final singles, so it is unchanged first by the complete alternating transport and, in the retained-outgoing case, by the endpoint stop followed by removal of the terminal block.
No integral, norm, or estimate occurs here.
theorem
Anderson4D.R324WithinHalfResidualPrefix.r324ResidualPrimitiveSumProduct_eq_leftDirectDriverProjection
{rho : SmoothCutoff}
{lam eps : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
(transport : (initial rho lam eps kappaP).R324WithinHalfAlternatingTransport)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(vl : (initial rho lam eps kappaP).SurvivingCoordinate → T4)
(vr : (initial rho lam eps kappaM).SurvivingCoordinate → T4)
:
r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi
(r324TwoHalfRootDoubledReconstruct (initial rho lam eps kappaP) (initial rho lam eps kappaM) (vl, vr)) = r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi
(r324TwoHalfRootDoubledReconstruct transport.final (initial rho lam eps kappaM) (transport.projection vl, vr))
A complete alternating transport of the left initial carrier preserves the cross primitive factor.
theorem
Anderson4D.R324WithinHalfResidualPrefix.r324ResidualPrimitiveSumProduct_eq_leftDirectOutgoingTerminalPost
{rho : SmoothCutoff}
{lam eps : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
(outgoing : (initial rho lam eps kappaP).R324PaperOutgoingEndpointTerminal)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(vl : (initial rho lam eps kappaP).SurvivingCoordinate → T4)
(vr : (initial rho lam eps kappaM).SurvivingCoordinate → T4)
:
r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi
(r324TwoHalfRootDoubledReconstruct (initial rho lam eps kappaP) (initial rho lam eps kappaM) (vl, vr)) = r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi
(r324TwoHalfRootDoubledReconstruct outgoing.terminalPost (initial rho lam eps kappaM)
(((outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv outgoing.terminalData.terminal [] ⋯)
(outgoing.endpoint.projection vl)).2, vr))
A retained outgoing terminal of the left direct-incoming half preserves the cross primitive factor after both its stop projection and its terminal tuple split.