The actual Step 4(A) endpoint collapse

This module connects the genuine refined physical root to the four literal endpoint routes. It follows paper §4.2: the right initial residual and the primitive cross factor remain one signed coefficient while the two endpoint operations of the left half are performed; the completed left density then remains one signed coefficient while the right half is performed.

The declarations below name only that canonical coefficient and its two direct-incoming projection identities. No endpoint norm is taken here.

@[reducible, inline]

abbrev Anderson4D.R324WithinHalfResidualPrefix.R324PaperLeftOuterParameter (rho : SmoothCutoff) (lam eps : ℝ) {m : ℕ} (kappaM : PartialPairing (Fin m)) : Type

The untouched variables opposite the left endpoint half: the two right boundary points and the right initial residual carrier.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.r324PaperLeftOuterParameterMeasure (rho : SmoothCutoff) (lam eps : ℝ) {m : ℕ} (kappaM : PartialPairing (Fin m)) : MeasureTheory.Measure (R324PaperLeftOuterParameter rho lam eps kappaM)

Product Haar on the untouched opposite-half variables.

Equations

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

instance Anderson4D.R324WithinHalfResidualPrefix.instSFiniteR324PaperLeftOuterParameterMeasure (rho : SmoothCutoff) (lam eps : ℝ) {m : ℕ} (kappaM : PartialPairing (Fin m)) : MeasureTheory.SFinite (r324PaperLeftOuterParameterMeasure rho lam eps kappaM)

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

Reassociate the physical root parameter as the free left outgoing endpoint followed by the untouched opposite-half parameter.

Equations

• Anderson4D.R324WithinHalfResidualPrefix.r324PaperLeftOuterParameterMeasurableEquiv rho lam eps kappaM L = MeasurableEquiv.prodAssoc.prodCongr (MeasurableEquiv.refl L)

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.r324PaperLeftOuterParameterMeasurableEquiv_apply (rho : SmoothCutoff) (lam eps : ℝ) {m : ℕ} (kappaM : PartialPairing (Fin m)) {L : Type u_1} [MeasurableSpace L] (q : R324IncomingExceptionalRootParameter rho lam eps kappaM × L) : (r324PaperLeftOuterParameterMeasurableEquiv rho lam eps kappaM L) q = ((q.1.1.1, q.1.1.2, q.1.2), q.2)

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

The reassociation preserves the literal product Haar measure.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.r324PaperLeftCanonicalCoefficient {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (left : R324WithinHalfResidualPrefix rho lam eps kappaP) (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (s : R324PaperLeftOuterParameter rho lam eps kappaM) (v : left.SurvivingCoordinate → T4) : ℂ

The literal coefficient carried through the left half: the two right characters, the right initial residual, and the still-signed primitive cross factor read on the current left carrier.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.r324PaperLeftDirectInitialSourceDensity {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (q : (T4 × R324PaperLeftOuterParameter rho lam eps kappaM) × ((initial rho lam eps kappaP).SurvivingCoordinate → T4)) : ℂ

The direct-incoming left source in the parameter order consumed by the one-half endpoint transform.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.directIncomingRefinedRootOuter_eq_char_mul_leftCanonical {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (y : T4) (s : R324PaperLeftOuterParameter rho lam eps kappaM) (v : (initial rho lam eps kappaP).SurvivingCoordinate → T4) : directIncomingRefinedRootOuter rho lam eps kappaP kappaM alpha beta pi ((y, s.1.1, s.1.2), s.2) v = charT4 beta y * (initial rho lam eps kappaP).r324PaperLeftCanonicalCoefficient alpha beta pi s v

Before any left transport, the genuine root outer factor is exactly the free left outgoing character times the canonical untouched coefficient.

theorem Anderson4D.R324WithinHalfResidualPrefix.integrable_and_integral_directIncomingSource_eq_leftInitial {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hsource : MeasureTheory.Integrable (directIncomingRefinedInitialSourceDensity rho lam eps kappaP kappaM alpha beta pi) ((r324IncomingExceptionalRootParameterMeasure rho lam eps kappaM).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaP).SurvivingCoordinate) => paperMeasure))) : MeasureTheory.Integrable (r324PaperLeftDirectInitialSourceDensity alpha beta pi) ((paperMeasure.prod (r324PaperLeftOuterParameterMeasure rho lam eps kappaM)).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaP).SurvivingCoordinate) => paperMeasure)) ∧ ∫ (q : R324IncomingExceptionalRootParameter rho lam eps kappaM × ((initial rho lam eps kappaP).SurvivingCoordinate → T4)), directIncomingRefinedInitialSourceDensity rho lam eps kappaP kappaM alpha beta pi q ∂(r324IncomingExceptionalRootParameterMeasure rho lam eps kappaM).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaP).SurvivingCoordinate) => paperMeasure) = ∫ (q : (T4 × R324PaperLeftOuterParameter rho lam eps kappaM) × ((initial rho lam eps kappaP).SurvivingCoordinate → T4)), r324PaperLeftDirectInitialSourceDensity alpha beta pi q ∂(paperMeasure.prod (r324PaperLeftOuterParameterMeasure rho lam eps kappaM)).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaP).SurvivingCoordinate) => paperMeasure)

Reindexing the genuine direct-incoming source gives exactly the parameterized left source above. Joint integrability is transported at the same time, so later endpoint operations need no new Fubini assumption.

theorem Anderson4D.R324WithinHalfResidualPrefix.integrable_and_r324RefinedPhysicalIntegral_eq_leftDirectInitial {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} (p : R324RefinedScheduleIndex m) (e0 : MomentContraction m) (he0 : e0 ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (heps : 0 < eps) (heps1 : eps ≤ 1) (alpha beta : Z4) : MeasureTheory.Integrable (r324PaperLeftDirectInitialSourceDensity alpha beta e0.snd.snd) ((paperMeasure.prod (r324PaperLeftOuterParameterMeasure rho lam eps e0.snd.fst)).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps e0.fst).SurvivingCoordinate) => paperMeasure)) ∧ r324RefinedPhysicalIntegral rho eps m alpha beta p = ∫ (q : (T4 × R324PaperLeftOuterParameter rho lam eps e0.snd.fst) × ((initial rho lam eps e0.fst).SurvivingCoordinate → T4)), r324PaperLeftDirectInitialSourceDensity alpha beta e0.snd.snd q ∂(paperMeasure.prod (r324PaperLeftOuterParameterMeasure rho lam eps e0.snd.fst)).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps e0.fst).SurvivingCoordinate) => paperMeasure)

Direct-incoming physical-root entrance in the exact parameter order of the left one-half transform.

theorem Anderson4D.R324WithinHalfResidualPrefix.directIncomingRefinedRootOuter_eq_char_mul_leftDirectDriver {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (transport : (initial rho lam eps kappaP).R324WithinHalfAlternatingTransport) (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (y : T4) (s : R324PaperLeftOuterParameter rho lam eps kappaM) (v : (initial rho lam eps kappaP).SurvivingCoordinate → T4) : directIncomingRefinedRootOuter rho lam eps kappaP kappaM alpha beta pi ((y, s.1.1, s.1.2), s.2) v = charT4 beta y * transport.final.r324PaperLeftCanonicalCoefficient alpha beta pi s (transport.projection v)

In a DD left half the same coefficient is read on the terminal driver carrier through its coordinate projection.

theorem Anderson4D.R324WithinHalfResidualPrefix.directIncomingRefinedRootOuter_eq_char_mul_leftDirectOutgoing {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (outgoing : (initial rho lam eps kappaP).R324PaperOutgoingEndpointTerminal) (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (y : T4) (s : R324PaperLeftOuterParameter rho lam eps kappaM) (v : (initial rho lam eps kappaP).SurvivingCoordinate → T4) : directIncomingRefinedRootOuter rho lam eps kappaP kappaM alpha beta pi ((y, s.1.1, s.1.2), 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

In a DE left half the same coefficient is read on the post-terminal carrier after the endpoint projection and literal terminal-tuple split.