Closed direct-left exact transforms for paper Step 4(A)

The direct incoming Fourier identity leaves the opposite half untouched. For a direct outgoing endpoint the only premise not already carried by the physical-root entrance is joint integrability on the completed left carrier. This file supplies exactly that premise from the two existing paper facts:

• the completed left Green chain is jointly L¹ under its terminal edge certificate; and
• the untouched right initial residual is jointly L¹.

The complete residual primitive sum is kept as one bounded measurable factor. No norm is taken before either within-half removal.

The terminal-left / initial-right product regroup

def Anderson4D.R324WithinHalfResidualPrefix.r324PaperLeftTerminalRightInitialMeasurableEquiv (Y : Type u_1) (Rest : Type u_2) (U : Type u_3) [MeasurableSpace Y] [MeasurableSpace Rest] [MeasurableSpace U] : (Y × Rest) × U ≃ᵐ (Y × U) × Rest

Reorder ((y, (zw, vr)), u) as ((y, u), (zw, vr)). This is the literal parameter order needed to multiply the completed left chain with the untouched right initial residual.

Equations

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

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.r324PaperLeftTerminalRightInitialMeasurableEquiv_apply {Y : Type u_1} {Rest : Type u_2} {U : Type u_3} [MeasurableSpace Y] [MeasurableSpace Rest] [MeasurableSpace U] (q : (Y × Rest) × U) : (r324PaperLeftTerminalRightInitialMeasurableEquiv Y Rest U) q = ((q.1.1, q.2), q.1.2)

theorem Anderson4D.R324WithinHalfResidualPrefix.measurePreserving_r324PaperLeftTerminalRightInitialMeasurableEquiv {Y : Type u_1} {Rest : Type u_2} {U : Type u_3} [MeasurableSpace Y] [MeasurableSpace Rest] [MeasurableSpace U] (muY : MeasureTheory.Measure Y) (muRest : MeasureTheory.Measure Rest) (muU : MeasureTheory.Measure U) [MeasureTheory.SFinite muY] [MeasureTheory.SFinite muRest] [MeasureTheory.SFinite muU] : MeasureTheory.MeasurePreserving (⇑(r324PaperLeftTerminalRightInitialMeasurableEquiv Y Rest U)) ((muY.prod muRest).prod muU) ((muY.prod muU).prod muRest)

The regroup preserves the corresponding product measures.

Joint integrability of the completed direct-left density

theorem Anderson4D.R324WithinHalfResidualPrefix.integrable_leftDirectTerminalCanonicalDensity {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {α β : Z4} (left : R324WithinHalfResidualPrefix ρ lam ε κp) (hleftRemaining : left.remaining = []) (leftScale : Fin (m + 1) → ℝ) (hleftCertificate : R324WithinHalfEdgeCertificate left.state leftScale) (hε : 0 < ε) (hε1 : ε ≤ 1) (multiplier : ℂ) (π : ↥κp.singles ≃ ↥κm.singles) : MeasureTheory.Integrable (fun (q : (T4 × R324PaperLeftOuterParameter ρ lam ε κm) × (left.SurvivingCoordinate → T4)) => left.incomingPhasedResidualDensity (charT4 β q.1.1 * (multiplier * (↑(paperSecondOrderModeDecay α) * left.r324PaperLeftCanonicalCoefficient α β π q.1.2 q.2))) α ρ ε 0 q.1.1 q.2) ((paperMeasure.prod (r324PaperLeftOuterParameterMeasure ρ lam ε κm)).prod (MeasureTheory.Measure.pi fun (x : left.SurvivingCoordinate) => paperMeasure))

The exact terminal density required by the direct/direct left transform is integrable. The proof multiplies the two already established half-chain L¹ facts and only then attaches the still-grouped bounded covariance sum and the unit-modulus Fourier characters.

Closed direct/direct physical transform

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

The direct/direct left transform with every analytic premise discharged from the physical entrance and the two paper L¹ producers above.

Closed direct/exceptional physical transform

theorem Anderson4D.R324WithinHalfResidualPrefix.leftDirectExceptional_exactTransform_and_source_eq_physical_closed_with_targetIntegrable {ρ : SmoothCutoff} {C lam ε K A : ℝ} {m : ℕ} {α : Z4} (p : R324RefinedScheduleIndex m) (e0 : MomentContraction m) (he0 : e0 ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) {providers : R324PaperHalfRouteProviders e0.fst α} (data : R324PaperHalfDirectExceptionalRoute providers) (β : Z4) : ∃ (transform : (R324PaperHalfEndpointUniformBound.ofDirectExceptional data).ExactTransform (r324PaperLeftOuterParameterMeasure ρ lam ε e0.snd.fst) (fun (s : R324PaperLeftOuterParameter ρ lam ε e0.snd.fst) (v : (R324PaperHalfEndpointUniformBound.ofDirectExceptional data).carrier.SurvivingCoordinate → T4) => data.outgoing.terminalPost.r324PaperLeftCanonicalCoefficient α β e0.snd.snd s v) β), transform.source = r324RefinedPhysicalIntegral ρ ε m α β p ∧ MeasureTheory.Integrable (fun (q : R324PaperLeftOuterParameter ρ lam ε e0.snd.fst × (data.outgoing.terminalPost.SurvivingCoordinate → T4)) => (R324PaperHalfEndpointUniformBound.ofDirectExceptional data).density (fun (v : (R324PaperHalfEndpointUniformBound.ofDirectExceptional data).carrier.SurvivingCoordinate → T4) => data.outgoing.terminalPost.r324PaperLeftCanonicalCoefficient α β e0.snd.snd q.1 v) β q.2) ((r324PaperLeftOuterParameterMeasure ρ lam ε e0.snd.fst).prod (MeasureTheory.Measure.pi fun (x : data.outgoing.terminalPost.SurvivingCoordinate) => paperMeasure))

The direct/exceptional left transform with its three analytic premises discharged from the physical entrance and the parameter-carrying endpoint transport. The Fourier character at the untouched endpoint is removed by its inverse before the endpoint operation; no absolute value is taken.

theorem Anderson4D.R324WithinHalfResidualPrefix.leftDirectExceptional_exactTransform_and_source_eq_physical_closed {ρ : SmoothCutoff} {C lam ε K A : ℝ} {m : ℕ} {α : Z4} (p : R324RefinedScheduleIndex m) (e0 : MomentContraction m) (he0 : e0 ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) {providers : R324PaperHalfRouteProviders e0.fst α} (data : R324PaperHalfDirectExceptionalRoute providers) (β : Z4) : ∃ (transform : (R324PaperHalfEndpointUniformBound.ofDirectExceptional data).ExactTransform (r324PaperLeftOuterParameterMeasure ρ lam ε e0.snd.fst) (fun (s : R324PaperLeftOuterParameter ρ lam ε e0.snd.fst) (v : (R324PaperHalfEndpointUniformBound.ofDirectExceptional data).carrier.SurvivingCoordinate → T4) => data.outgoing.terminalPost.r324PaperLeftCanonicalCoefficient α β e0.snd.snd s v) β), transform.source = r324RefinedPhysicalIntegral ρ ε m α β p

Compatibility wrapper retaining the original exact-transform API.