The right exceptional-incoming source after the completed left half

This is the product-measure reassociation used between the two halves in paper Step 4(A) when the right incoming endpoint is exceptional. The completed signed left density is kept as one untouched coefficient of the right initial residual density. No absolute value, endpoint estimate, or new summation occurs here.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.rightExceptionalPostOuter {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha : Z4} {leftRoute : R324PaperHalfCompletedRoute kappaP alpha} (left : R324PaperHalfEndpointUniformBound leftRoute) (beta : Z4) {rightScale : Fin (m + 1) → ℝ} (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (projectedCoefficient : (left.carrier.SurvivingCoordinate → T4) → ((rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (omega : T4 × (left.carrier.SurvivingCoordinate → T4)) (post : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).SurvivingCoordinate → T4) : ℂ

The completed left half, still signed, as the post-stop coefficient of the exceptional right incoming endpoint. The right post-stop carrier is deliberately abstract: the concrete ED and EE routes supply respectively their alternating-transport and outgoing-terminal projections.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.integrable_and_integral_completedLeft_eq_rightExceptionalInitialSource {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha : Z4} {leftRoute : R324PaperHalfCompletedRoute kappaP alpha} (left : R324PaperHalfEndpointUniformBound leftRoute) (beta : Z4) {rightScale : Fin (m + 1) → ℝ} (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (projectedCoefficient : (left.carrier.SurvivingCoordinate → T4) → ((rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (hlinear : ∀ (a : ℂ) (coefficient : (left.carrier.SurvivingCoordinate → T4) → ℂ) (outgoingMode : Z4) (v : left.carrier.SurvivingCoordinate → T4), left.density (fun (u : left.carrier.SurvivingCoordinate → T4) => a * coefficient u) outgoingMode v = a * left.density coefficient outgoingMode v) (hproject : ∀ (s : R324PaperLeftOuterParameter rho lam eps kappaM) (v : left.carrier.SurvivingCoordinate → T4), ↑(r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi (r324TwoHalfRootDoubledReconstruct left.carrier (initial rho lam eps kappaM) (v, s.2))) = projectedCoefficient v ((rightData.trace.stopPrefix.splitSurvivingPiMeasurableEquiv rightData.terminal rightData.suffix ⋯) (rightData.trace.stopProjection s.2)).2) (hleft : MeasureTheory.Integrable (fun (q : R324PaperLeftOuterParameter rho lam eps kappaM × (left.carrier.SurvivingCoordinate → T4)) => left.density (fun (v : left.carrier.SurvivingCoordinate → T4) => left.carrier.r324PaperLeftCanonicalCoefficient alpha beta pi q.1 v) beta q.2) ((r324PaperLeftOuterParameterMeasure rho lam eps kappaM).prod (MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure))) : MeasureTheory.Integrable (rightData.incomingExceptionalInitialSourceDensity (-alpha) (fun (omega : T4 × (left.carrier.SurvivingCoordinate → T4)) => omega.1) (left.rightExceptionalPostOuter beta rightData projectedCoefficient)) ((paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure))).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaM).SurvivingCoordinate) => paperMeasure)) ∧ left.transformTarget (r324PaperLeftOuterParameterMeasure rho lam eps kappaM) (fun (s : R324PaperLeftOuterParameter rho lam eps kappaM) (v : left.carrier.SurvivingCoordinate → T4) => left.carrier.r324PaperLeftCanonicalCoefficient alpha beta pi s v) beta = ∫ (p : (T4 × T4 × (left.carrier.SurvivingCoordinate → T4)) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)), rightData.incomingExceptionalInitialSourceDensity (-alpha) (fun (omega : T4 × (left.carrier.SurvivingCoordinate → T4)) => omega.1) (left.rightExceptionalPostOuter beta rightData projectedCoefficient) p ∂(paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure))).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaM).SurvivingCoordinate) => paperMeasure)

The paper's exact right-incoming regroup for an arbitrary completed left endpoint route.

hlinear is the literal scalar linearity of the completed left density; the four canonical constructors prove it by their already established pointwise formulas. hproject is only the existing coordinate identity which reads the primitive cross factor on the right post-stop carrier. Thus the conclusion supplies precisely the source integrability and source equality consumed by both right ED and right EE transforms, before any norm is taken.