The completed left endpoint half, in all four literal cases

This is the paper Step 4(A) case split for the first half only. Each branch uses its existing exact signed transform and its existing joint L¹ handoff. No estimate and no absolute value occurs here.

Common-translation geometry of a completed terminal half

theorem Anderson4D.R324WithinHalfResidualPrefix.reconstruct_commonTranslate_of_active {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix rho lam eps pairing) (v : res.SurvivingCoordinate → T4) (a : T4) (i : Fin m) (hi : i ∈ res.state.active) : res.reconstruct (fun (j : res.SurvivingCoordinate) => v j + a) i = res.reconstruct v i + a

Reconstruction of a surviving terminal coordinate commutes with a common translation.

structure Anderson4D.R324WithinHalfResidualPrefix.R324PaperLeftRouteExactPackage {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {alpha : Z4} (p : R324RefinedScheduleIndex m) (e0 : MomentContraction m) {routeProviders : R324PaperHalfRouteProviders e0.fst alpha} (route : R324PaperHalfEndpointRoute routeProviders) (beta : Z4) : Type

Common exact output of the four possible left endpoint routes.

• bound : R324PaperHalfEndpointUniformBound route.completedRoute
• transform : self.bound.ExactTransform (r324PaperLeftOuterParameterMeasure rho lam eps e0.snd.fst) (fun (s : R324PaperLeftOuterParameter rho lam eps e0.snd.fst) (v : self.bound.carrier.SurvivingCoordinate → T4) => self.bound.carrier.r324PaperLeftCanonicalCoefficient alpha beta e0.snd.snd s v) beta
• source_eq_physical : self.transform.source = r324RefinedPhysicalIntegral rho eps m alpha beta p
• target_integrable : MeasureTheory.Integrable (fun (q : R324PaperLeftOuterParameter rho lam eps e0.snd.fst × (self.bound.carrier.SurvivingCoordinate → T4)) => self.bound.density (fun (v : self.bound.carrier.SurvivingCoordinate → T4) => self.bound.carrier.r324PaperLeftCanonicalCoefficient alpha beta e0.snd.snd q.1 v) beta q.2) ((r324PaperLeftOuterParameterMeasure rho lam eps e0.snd.fst).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
• unit_commonTranslate (a : T4) (v : self.bound.carrier.SurvivingCoordinate → T4) : (self.bound.density (fun (x : self.bound.carrier.SurvivingCoordinate → T4) => 1) beta fun (i : self.bound.carrier.SurvivingCoordinate) => v i + a) = charT4 (alpha + beta) a * self.bound.density (fun (x : self.bound.carrier.SurvivingCoordinate → T4) => 1) beta v

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperLeftRouteExactPackage.exists_of_route {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {alpha : Z4} {p : R324RefinedScheduleIndex m} {e0 : MomentContraction m} {providers : R324PaperHalfRouteProviders e0.fst alpha} (he0 : e0 ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (hsingles : e0.fst.singles.Nonempty) (route : R324PaperHalfEndpointRoute providers) (beta : Z4) : Nonempty (R324PaperLeftRouteExactPackage p e0 route beta)

Literal four-case constructor. Every branch is an already closed producer; this theorem only forgets the branch witness after using it.