Common exact output of the second endpoint half

The source equality is the single signed Fubini handoff between the two halves. endpoint_integrable is retained solely for the final product-Haar regroup. Neither field contains an estimate.

structure Anderson4D.R324WithinHalfResidualPrefix.R324PaperRightRouteExactPackage {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {alpha beta : Z4} {p : R324RefinedScheduleIndex m} {e0 : MomentContraction m} {leftProviders : R324PaperHalfRouteProviders e0.fst alpha} {rightProviders : R324PaperHalfRouteProviders e0.snd.fst (-alpha)} {leftRoute : R324PaperHalfEndpointRoute leftProviders} (left : R324PaperLeftRouteExactPackage p e0 leftRoute beta) (rightRoute : R324PaperHalfEndpointRoute rightProviders) : Type

The completed right transform and the exact source/target seams needed by exactCollapse_to_nested_of_transforms.

• bound : R324PaperHalfEndpointUniformBound rightRoute.completedRoute
• transform : self.bound.ExactTransform (MeasureTheory.Measure.pi fun (x : left.bound.carrier.SurvivingCoordinate) => paperMeasure) (fun (leftPost : left.bound.carrier.SurvivingCoordinate → T4) (rightPost : self.bound.carrier.SurvivingCoordinate → T4) => left.bound.density (fun (x : left.bound.carrier.SurvivingCoordinate → T4) => left.bound.crossCoefficient self.bound e0.snd.snd leftPost rightPost) beta leftPost) (-beta)
• source_eq_left_target : self.transform.source = left.bound.transformTarget (r324PaperLeftOuterParameterMeasure rho lam eps e0.snd.fst) (fun (s : R324PaperLeftOuterParameter rho lam eps e0.snd.fst) (v : left.bound.carrier.SurvivingCoordinate → T4) => left.bound.carrier.r324PaperLeftCanonicalCoefficient alpha beta e0.snd.snd s v) beta
• endpoint_integrable : MeasureTheory.Integrable (left.bound.endpointProductDensity self.bound beta e0.snd.snd) ((MeasureTheory.Measure.pi fun (x : left.bound.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : self.bound.carrier.SurvivingCoordinate) => paperMeasure))
• density_mul (a : ℂ) (coefficient : (self.bound.carrier.SurvivingCoordinate → T4) → ℂ) (outgoingMode : Z4) (v : self.bound.carrier.SurvivingCoordinate → T4) : self.bound.density (fun (u : self.bound.carrier.SurvivingCoordinate → T4) => a * coefficient u) outgoingMode v = a * self.bound.density coefficient outgoingMode v
• density_congr_at (leftCoefficient rightCoefficient : (self.bound.carrier.SurvivingCoordinate → T4) → ℂ) (outgoingMode : Z4) (v : self.bound.carrier.SurvivingCoordinate → T4) : leftCoefficient v = rightCoefficient v → self.bound.density leftCoefficient outgoingMode v = self.bound.density rightCoefficient outgoingMode v

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperRightRouteExactPackage.exactCollapse_to_nested {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {alpha beta : Z4} {p : R324RefinedScheduleIndex m} {e0 : MomentContraction m} {leftProviders : R324PaperHalfRouteProviders e0.fst alpha} {rightProviders : R324PaperHalfRouteProviders e0.snd.fst (-alpha)} {leftRoute : R324PaperHalfEndpointRoute leftProviders} {rightRoute : R324PaperHalfEndpointRoute rightProviders} (left : R324PaperLeftRouteExactPackage p e0 leftRoute beta) (right : R324PaperRightRouteExactPackage left rightRoute) : ↑(lamEps lam eps) ^ (2 * ((initial rho lam eps e0.fst).remainingOrder + (initial rho lam eps e0.snd.fst).remainingOrder)) * r324RefinedPhysicalIntegral rho eps m alpha beta p = ∫ (v : (left.bound.twoHalfTerminal right.bound).NestedCoordinate e0.snd.snd → T4), left.bound.nestedEndpointProductDensity right.bound beta e0.snd.snd v ∂MeasureTheory.Measure.pi fun (x : (left.bound.twoHalfTerminal right.bound).NestedCoordinate e0.snd.snd) => paperMeasure

With both half packages in hand, the complete four-endpoint signed collapse is exactly the already proved common two-half composition.