Discharge of the driver-terminal joint integrability (R-324, gap (a))

R324DriverClosure expresses joint integrability for the terminal y-Fourier evaluation as the Prop DriverTerminalJointIntegrable. This file proves it for every alternating transport whose terminal edge state carries a slotwise quantitative certificate, and in particular for the canonical driver transport afterHeadAlternatingTransport, whose terminal certificate is extracted from the of_localBlockProvider recursion.

The three analytic ingredients are

• the slot-zero-erased terminal chain is jointly L¹ in the outgoing endpoint and all surviving coordinates (a heterogeneous Haar-path argument; the corresponding machinery in R324TerminalJointIntegrabilityProducer is private and is reproved here in the erased form);
• the untouched right initial residual is jointly L¹ in its two endpoints and all initial sparse coordinates (renormalized Green skeleton times a bounded primitive block product);
• the residual cross-cut primitive sum is a bounded measurable factor.

The product-measure regrouping is the public r324DriverTerminalRegroupMeasurableEquiv of the driver closure.

Reproved heterogeneous Haar-path lemmas

theorem Anderson4D.r324TJIE_integrable_kernel_sub_mul_lift {Y : Type u_1} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} [MeasureTheory.SFinite ν] (K : T4 → ℝ) (f : Y → ℝ) (shift : Y → T4) (hK : MeasureTheory.Integrable K paperMeasure) (hKmeas : Measurable K) (hf : MeasureTheory.Integrable f ν) (hshift : Measurable shift) : MeasureTheory.Integrable (fun (p : T4 × Y) => K (p.1 - shift p.2) * f p.2) (paperMeasure.prod ν)

One integrable kernel read against a measurable shift, times an integrable lift: jointly integrable on the product. Reproof of the private producer lemma.

noncomputable def Anderson4D.r324TJIE_terminalWeightedKernelPath {n : ℕ} (K : Fin n → T4 → ℝ) (terminalWeight : T4 → ℝ) (x : Fin (n + 1) → T4) : ℝ

A heterogeneous kernel path with a terminal weight, on n + 1 ordered coordinates carrying n kernels. Reproof of the private producer definition.

Equations

• Anderson4D.r324TJIE_terminalWeightedKernelPath K terminalWeight x = (∏ i : Fin n, K i (x i.castSucc - x i.succ)) * terminalWeight (x (Fin.last n))

theorem Anderson4D.r324TJIE_integrable_terminalWeightedKernelPath {n : ℕ} (K : Fin n → T4 → ℝ) (terminalWeight : T4 → ℝ) : (∀ (i : Fin n), MeasureTheory.Integrable (K i) paperMeasure) → (∀ (i : Fin n), Measurable (K i)) → MeasureTheory.Integrable terminalWeight paperMeasure → MeasureTheory.Integrable (r324TJIE_terminalWeightedKernelPath K terminalWeight) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)

Joint integrability of the terminal-weighted heterogeneous kernel path. Reproof of the private producer theorem.

theorem Anderson4D.r324TJIE_integrable_of_offDiagonal_bound {K : T4 → ℝ} {C : ℝ} (hKmeas : Measurable K) (hC : 0 ≤ C) (hbound : ∀ (z : T4), z ≠ 0 → |K z| ≤ C * invSqKer z) : MeasureTheory.Integrable K paperMeasure

Off-diagonal inverse-square domination gives integrability. Reproof of the private producer lemma.

The ordered sparse chain of a completed half, reproved

def Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_activeOrder {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : Fin res.state.active.card ≃o ↥res.state.active

Order the surviving internal vertices. Reproof of the private producer definition.

Equations

• res.r324TJIE_activeOrder = res.state.active.orderIsoOfFin ⋯

def Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_edgeSlot {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (i : Fin (res.state.active.card + 1)) : Fin (m + 1)

The zeroth sparse edge is the incoming edge; every later sparse edge starts at the correspondingly ordered surviving internal vertex.

Equations

• res.r324TJIE_edgeSlot i = if hi : ↑i = 0 then 0 else Anderson4D.r324InternalVertexEdgeSlot ↑(res.r324TJIE_activeOrder ⟨↑i - 1, ⋯⟩)

theorem Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_edgeSlot_mem {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (i : Fin (res.state.active.card + 1)) : res.r324TJIE_edgeSlot i ∈ res.activeEdgeSlots

theorem Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_edgeSlot_strictMono {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : StrictMono res.r324TJIE_edgeSlot

theorem Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_edgeSlot_injective {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : Function.Injective res.r324TJIE_edgeSlot

theorem Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_edgeSlot_surjective {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : Function.Surjective fun (i : Fin (res.state.active.card + 1)) => ⟨res.r324TJIE_edgeSlot i, ⋯⟩

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_activeEdgeEquiv {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : Fin (res.state.active.card + 1) ≃ ↥res.activeEdgeSlots

The ordered enumeration of the active edge slots.

Equations

• res.r324TJIE_activeEdgeEquiv = Equiv.ofBijective (fun (i : Fin (res.state.active.card + 1)) => ⟨res.r324TJIE_edgeSlot i, ⋯⟩) ⋯

def Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_orderedVertices {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (x y : T4) (v : res.SurvivingCoordinate → T4) : Fin (res.state.active.card + 2) → T4

The ordered point corresponding to a terminal half-chain.

Equations

• res.r324TJIE_orderedVertices x y v = Anderson4D.assemble x y fun (j : Fin res.state.active.card) => v (res.r324TJIE_activeOrder j)

def Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_orderedKernel {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (i : Fin (res.state.active.card + 1)) : T4 → ℝ

The ordered named kernels of the terminal state.

Equations

• res.r324TJIE_orderedKernel i = res.state.edges (res.r324TJIE_edgeSlot i)

theorem Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_edgeSlot_lt_target {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (i : Fin (res.state.active.card + 1)) (hi : ↑i < res.state.active.card) : ↑(res.r324TJIE_edgeSlot i) < ↑(varIdx ↑(res.r324TJIE_activeOrder ⟨↑i, hi⟩))

theorem Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_index_le_of_edgeSlot_lt_varIdx {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (i : Fin (res.state.active.card + 1)) (a : res.SurvivingCoordinate) (h : ↑(res.r324TJIE_edgeSlot i) < ↑(varIdx ↑a)) : ↑i ≤ ↑(res.r324TJIE_activeOrder.symm a)

theorem Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_edgeSuccessor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (i : Fin (res.state.active.card + 1)) : res.edgeSuccessor (res.r324TJIE_edgeSlot i) = if hi : ↑i < res.state.active.card then varIdx ↑(res.r324TJIE_activeOrder ⟨↑i, hi⟩) else Fin.last (m + 1)

The successor selected by the sparse state is exactly the next ordered surviving vertex, or the terminal external point after the last edge.

theorem Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_edgeSource {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (x y : T4) (v : res.SurvivingCoordinate → T4) (i : Fin (res.state.active.card + 1)) : assemble x y (res.reconstruct v) (res.r324TJIE_edgeSlot i).castSucc = res.r324TJIE_orderedVertices x y v i.castSucc

theorem Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_edgeTarget {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (x y : T4) (v : res.SurvivingCoordinate → T4) (i : Fin (res.state.active.card + 1)) : assemble x y (res.reconstruct v) (res.edgeSuccessor (res.r324TJIE_edgeSlot i)) = res.r324TJIE_orderedVertices x y v i.succ

theorem Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_orderedEdge_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (x y : T4) (v : res.SurvivingCoordinate → T4) (i : Fin (res.state.active.card + 1)) : res.state.edges (res.r324TJIE_edgeSlot i) (res.edgeDisplacement x y (res.reconstruct v) (res.r324TJIE_edgeSlot i)) = res.r324TJIE_orderedKernel i (res.r324TJIE_orderedVertices x y v i.castSucc - res.r324TJIE_orderedVertices x y v i.succ)

The slot-zero-erased ordered chain

def Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_erasedOrderedTuple {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (y : T4) (v : res.SurvivingCoordinate → T4) : Fin (res.state.active.card + 1) → T4

The ordered tuple carrying the erased chain: the ordered surviving internal vertices followed by the outgoing endpoint. The incoming endpoint does not appear.

Equations

• res.r324TJIE_erasedOrderedTuple y v = Fin.snoc (fun (j : Fin res.state.active.card) => v (res.r324TJIE_activeOrder j)) y

theorem Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_orderedVertices_succ {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (x y : T4) (v : res.SurvivingCoordinate → T4) (k : Fin (res.state.active.card + 1)) : res.r324TJIE_orderedVertices x y v k.succ = res.r324TJIE_erasedOrderedTuple y v k

Away from the incoming endpoint, the ordered vertices are the erased ordered tuple, independently of the incoming endpoint.

theorem Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_incomingErasedChainProduct_eq_path {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hremaining : res.remaining = []) (x y : T4) (v : res.SurvivingCoordinate → T4) : res.incomingErasedResidualChainProduct x y (res.reconstruct v) = r324TJIE_terminalWeightedKernelPath (fun (j : Fin res.state.active.card) => res.r324TJIE_orderedKernel j.succ) (fun (x : T4) => 1) (res.r324TJIE_erasedOrderedTuple y v)

The erased chain is a heterogeneous kernel path. At an empty suffix the slot-zero-erased residual chain is the path of the ordered kernels past the incoming edge, read on the erased ordered tuple; the incoming endpoint has disappeared.

theorem Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_residualDifferenceProduct_eq_one_of_nil {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hremaining : res.remaining = []) (x y : T4) (v : Fin m → T4) : res.residualDifferenceProduct x y v = 1

At an empty suffix there are no remaining signed differences.

theorem Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_residualPrimitiveProduct_eq_one_of_nil {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hremaining : res.remaining = []) (ρ' : SmoothCutoff) (ε' : ℝ) (v : Fin m → T4) : res.residualPrimitiveProduct ρ' ε' v = 1

At an empty suffix there are no remaining primitive blocks.

theorem Anderson4D.R324WithinHalfResidualPrefix.r324TJIE_incomingErasedResidualIntegrand_eq_chain_of_nil {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hremaining : res.remaining = []) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : Fin m → T4) : res.incomingErasedResidualIntegrand ρ' ε' x y v = res.incomingErasedResidualChainProduct x y v

At an empty suffix the erased residual core is the erased chain.

theorem Anderson4D.R324WithinHalfResidualPrefix.integrable_terminal_incomingErasedResidualIntegrand {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hremaining : res.remaining = []) (ρ' : SmoothCutoff) (ε' : ℝ) (scale : Fin (m + 1) → ℝ) (hcert : R324WithinHalfEdgeCertificate res.state scale) : MeasureTheory.Integrable (fun (p : T4 × (res.SurvivingCoordinate → T4)) => res.incomingErasedResidualIntegrand ρ' ε' 0 p.1 (res.reconstruct p.2)) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))

Erased-chain joint L¹ (gap (a), ingredient (i)). At an empty suffix, under a slotwise quantitative certificate, the slot-zero-erased residual core is jointly integrable in the outgoing endpoint and all surviving coordinates. The pinned incoming endpoint does not occur.

Joint L¹ of the untouched initial residual

theorem Anderson4D.integrable_initial_residualIntegrand_pair (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (κ : PartialPairing (Fin m)) : MeasureTheory.Integrable (fun (p : (T4 × T4) × ((R324WithinHalfResidualPrefix.initial ρ lam ε κ).SurvivingCoordinate → T4)) => (R324WithinHalfResidualPrefix.initial ρ lam ε κ).residualIntegrand ρ ε p.1.1 p.1.2 ((R324WithinHalfResidualPrefix.initial ρ lam ε κ).reconstruct p.2)) ((paperMeasure.prod paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (R324WithinHalfResidualPrefix.initial ρ lam ε κ).SurvivingCoordinate) => paperMeasure))

Right-half initial residual joint L¹ (gap (a), ingredient (iii)). The complete initial within-half residual is jointly integrable in its two endpoints and all initial sparse coordinates: renormalized Green skeleton times a uniformly bounded measurable primitive block product.

Measurability of the doubled root reconstruction

theorem Anderson4D.measurable_r324TwoHalfRootDoubledReconstruct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (leftRes : R324WithinHalfResidualPrefix ρ lam ε κp) (rightRes : R324WithinHalfResidualPrefix ρ lam ε κm) : Measurable (r324TwoHalfRootDoubledReconstruct leftRes rightRes)

The doubled ambient tuple assembled from two sparse carriers is jointly measurable.

The terminal certificate of the alternating driver

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfAlternatingTransport.exists_final_edgeCertificate_of_localBlockProvider_of_le {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K pairing) (N : ℕ) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : res.remaining.length ≤ N → ∀ (scale : Fin (m + 1) → ℝ) (certificate : R324WithinHalfEdgeCertificate res.state scale), ∃ (finalScale : Fin (m + 1) → ℝ), R324WithinHalfEdgeCertificate (of_localBlockProvider hε hε1 provider res scale certificate).final.state finalScale

Bounded-length form of the terminal-certificate extraction along the alternating driver recursion.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfAlternatingTransport.exists_final_edgeCertificate_of_localBlockProvider {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K pairing) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (scale : Fin (m + 1) → ℝ) (certificate : R324WithinHalfEdgeCertificate res.state scale) : ∃ (finalScale : Fin (m + 1) → ℝ), R324WithinHalfEdgeCertificate (of_localBlockProvider hε hε1 provider res scale certificate).final.state finalScale

Terminal certificate of the alternating driver. The driver built from a local block provider carries a slotwise quantitative certificate on its terminal edge state.

Discharge of the driver-terminal joint integrability

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.driverTerminalJointIntegrable_of_terminal_certificate {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κp initialScale) (t : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (α β : Z4) (π : ↥κp.singles ≃ ↥κm.singles) (hε : 0 < ε) (hε1 : ε ≤ 1) (finalScale : Fin (m + 1) → ℝ) (hcert : R324WithinHalfEdgeCertificate t.final.state finalScale) : data.DriverTerminalJointIntegrable t α β π

Gap (a) discharged from a terminal certificate. Any alternating transport whose terminal edge state carries a slotwise quantitative certificate satisfies the driver-terminal joint integrability: the phased density is the product of the L¹ erased terminal chain in (y, u), the L¹ untouched right initial residual in (zw, vr), the bounded measurable cross-cut primitive factor, and a unimodular phase with constant amplitude.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.driverTerminalJointIntegrable_afterHeadAlternatingTransport {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κp initialScale) (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K κp) (α β : Z4) (π : ↥κp.singles ≃ ↥κm.singles) : data.DriverTerminalJointIntegrable (data.afterHeadAlternatingTransport hε hε1 provider) α β π

Gap (a) discharged for the canonical driver transport. The alternating transport constructed by the driver from the local block provider satisfies the driver-terminal joint integrability; its terminal certificate is extracted from the of_localBlockProvider recursion.