The exceptional-incoming left endpoint transforms

This is the remaining left-half part of paper Step 4(A). It packages the existing physical-root ED and EE splices directly as common endpoint transforms. In particular the exceptional head, every intervening interval, and the outgoing endpoint operation are those of the paper proof; no new summation or estimate is introduced here.

The canonical opposite-half coefficient

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingExceptionalRefinedRootPostOuter_eq_char_mul_leftCanonical {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly kappaP initialScale) (outgoing : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324PaperOutgoingEndpointTerminal) (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (y : T4) (s : R324PaperLeftOuterParameter rho lam eps kappaM) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) : data.incomingExceptionalRefinedRootPostOuter alpha beta pi ((y, s.1), s.2) v = charT4 beta y * outgoing.terminalPost.r324PaperLeftCanonicalCoefficient alpha beta pi s ((outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv outgoing.terminalData.terminal [] ⋯) (outgoing.endpoint.projection v)).2

On an exceptional-incoming/exceptional-outgoing half, the refined-root outer coefficient is the free outgoing character times the same canonical opposite-half coefficient used by the common endpoint interface. This is only the two already-proved projection identities, before any norm.

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingExceptionalRefinedRootOutgoingPostCoefficient_eq_mul_leftCanonical {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly kappaP initialScale) (outgoing : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324PaperOutgoingEndpointTerminal) (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (s : R324PaperLeftOuterParameter rho lam eps kappaM) (v : outgoing.terminalPost.SurvivingCoordinate → T4) : data.incomingExceptionalRefinedRootOutgoingPostCoefficient outgoing alpha beta pi s v = outgoing.endpoint.multiplier alpha * (↑(paperSecondOrderModeDecay alpha) ^ 2 * incomingExceptionalPrimitiveDefect rho lam eps (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges alpha * outgoing.terminalPost.r324PaperLeftCanonicalCoefficient alpha beta pi s v)

After the outgoing exceptional terminal has been removed, the remaining coefficient is precisely its Fourier multiplier, the two second-order factors, the incoming primitive defect, and the canonical untouched opposite-half coefficient.

The exceptional source has one additional incoming endpoint in front of the physical root parameter. The following reassociation is the literal coordinate change used in paper Step 4(A); it changes no variable and no integrand, but only moves parentheses so that the common one-half interface sees the free outgoing endpoint followed by the opposite-half parameter.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.r324PaperLeftExceptionalParameterMeasurableEquiv (rho : SmoothCutoff) (lam eps : ℝ) {m : ℕ} (kappaM : PartialPairing (Fin m)) (L : Type u_1) [MeasurableSpace L] : (T4 × R324IncomingExceptionalRootParameter rho lam eps kappaM) × L ≃ᵐ (T4 × T4 × R324PaperLeftOuterParameter rho lam eps kappaM) × L

Equations

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

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.r324PaperLeftExceptionalParameterMeasurableEquiv_apply (rho : SmoothCutoff) (lam eps : ℝ) {m : ℕ} (kappaM : PartialPairing (Fin m)) {L : Type u_1} [MeasurableSpace L] (q : (T4 × R324IncomingExceptionalRootParameter rho lam eps kappaM) × L) : (r324PaperLeftExceptionalParameterMeasurableEquiv rho lam eps kappaM L) q = ((q.1.1, q.1.2.1.1, q.1.2.1.2, q.1.2.2), q.2)

theorem Anderson4D.R324WithinHalfResidualPrefix.measurePreserving_r324PaperLeftExceptionalParameterMeasurableEquiv (rho : SmoothCutoff) (lam eps : ℝ) {m : ℕ} (kappaM : PartialPairing (Fin m)) {L : Type u_1} [MeasurableSpace L] (muL : MeasureTheory.Measure L) [MeasureTheory.SFinite muL] : MeasureTheory.MeasurePreserving (⇑(r324PaperLeftExceptionalParameterMeasurableEquiv rho lam eps kappaM L)) ((paperMeasure.prod (r324IncomingExceptionalRootParameterMeasure rho lam eps kappaM)).prod muL) ((paperMeasure.prod (paperMeasure.prod (r324PaperLeftOuterParameterMeasure rho lam eps kappaM))).prod muL)

Exceptional/direct

theorem Anderson4D.R324WithinHalfResidualPrefix.leftExceptionalDirect_exactTransform_and_source_eq_physical {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {alpha : Z4} (p : R324RefinedScheduleIndex m) (e0 : MomentContraction m) (he0 : e0 ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) {providers : R324PaperHalfRouteProviders e0.fst alpha} (houtgoing : Fin.last m ∉ extractedRightEdges e0.fst) (data : R324PaperHalfExceptionalDirectRoute providers) (beta : Z4) : ∃ (transform : (R324PaperHalfEndpointUniformBound.ofExceptionalDirect houtgoing data).ExactTransform (r324PaperLeftOuterParameterMeasure rho lam eps e0.snd.fst) (fun (s : R324PaperLeftOuterParameter rho lam eps e0.snd.fst) (v : (R324PaperHalfEndpointUniformBound.ofExceptionalDirect houtgoing data).carrier.SurvivingCoordinate → T4) => data.transport.final.r324PaperLeftCanonicalCoefficient alpha beta e0.snd.snd s v) beta), transform.source = r324RefinedPhysicalIntegral rho eps m alpha beta p

The genuine paired-incoming physical root is the source of the literal left ED transform. This is only the already proved physical splice read through the common endpoint interface.

Exceptional/exceptional

theorem Anderson4D.R324WithinHalfResidualPrefix.leftExceptionalExceptional_exactTransform_and_source_eq_physical_with_targetIntegrable {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {alpha : Z4} (p : R324RefinedScheduleIndex m) (e0 : MomentContraction m) (he0 : e0 ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) {providers : R324PaperHalfRouteProviders e0.fst alpha} (hsingles : e0.fst.singles.Nonempty) (data : R324PaperHalfExceptionalExceptionalRoute providers) (beta : Z4) : ∃ (transform : (R324PaperHalfEndpointUniformBound.ofExceptionalExceptional hsingles data).ExactTransform (r324PaperLeftOuterParameterMeasure rho lam eps e0.snd.fst) (fun (s : R324PaperLeftOuterParameter rho lam eps e0.snd.fst) (v : (R324PaperHalfEndpointUniformBound.ofExceptionalExceptional hsingles data).carrier.SurvivingCoordinate → T4) => data.outgoing.terminalPost.r324PaperLeftCanonicalCoefficient alpha beta e0.snd.snd s v) beta), transform.source = r324RefinedPhysicalIntegral rho eps m alpha beta p ∧ MeasureTheory.Integrable (fun (q : R324PaperLeftOuterParameter rho lam eps e0.snd.fst × (data.outgoing.terminalPost.SurvivingCoordinate → T4)) => (R324PaperHalfEndpointUniformBound.ofExceptionalExceptional hsingles data).density (fun (v : (R324PaperHalfEndpointUniformBound.ofExceptionalExceptional hsingles data).carrier.SurvivingCoordinate → T4) => data.outgoing.terminalPost.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 : data.outgoing.terminalPost.SurvivingCoordinate) => paperMeasure))

The paired-incoming physical root is the source of the literal left EE transform. Joint integrability at the retained outgoing terminal is transported by the endpoint witness itself; this is the paper's Fubini handover, not an additional estimate.

theorem Anderson4D.R324WithinHalfResidualPrefix.leftExceptionalExceptional_exactTransform_and_source_eq_physical {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {alpha : Z4} (p : R324RefinedScheduleIndex m) (e0 : MomentContraction m) (he0 : e0 ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) {providers : R324PaperHalfRouteProviders e0.fst alpha} (hsingles : e0.fst.singles.Nonempty) (data : R324PaperHalfExceptionalExceptionalRoute providers) (beta : Z4) : ∃ (transform : (R324PaperHalfEndpointUniformBound.ofExceptionalExceptional hsingles data).ExactTransform (r324PaperLeftOuterParameterMeasure rho lam eps e0.snd.fst) (fun (s : R324PaperLeftOuterParameter rho lam eps e0.snd.fst) (v : (R324PaperHalfEndpointUniformBound.ofExceptionalExceptional hsingles data).carrier.SurvivingCoordinate → T4) => data.outgoing.terminalPost.r324PaperLeftCanonicalCoefficient alpha beta e0.snd.snd s v) beta), transform.source = r324RefinedPhysicalIntegral rho eps m alpha beta p

Compatibility wrapper retaining the original exact-transform API.