Paper Step 4(A): structural two-half endpoint splice #

This file records two facts used when the four external Fourier variables are integrated only after the signed within-half removals.

On a residual half, the exceptional incoming block and an exceptional outgoing block cannot be the same analytic step. If they were, that step would span the whole current carrier and, being the last step, would leave no final single. Thus the same-block case belongs to the full/full Step-1 branch.
When both endpoints of both residual halves are direct, the genuine terminal density factors exactly through four translated Green modes. The displayed norm identity is taken only after this signed four-endpoint identity; the complete cross-covariance core is never split.

The one-endpoint ordinary-to-inserted integral bridge #

source

theorem Anderson4D.integral_primitiveKernelMajorant_le_endpointSacrifice_mul_inserted (C lam supportConstant : ℝ) (n : ℕ) {eps : ℝ} (heps : 0 < eps) :

∫ (z : T4), primitiveKernelMajorant C lam eps supportConstant n z ∂paperMeasure ≤ SmoothCutoff.r324EndpointPrimitiveSacrifice eps SmoothCutoff.R324EndpointReductionCase.insertedSacrifice * ∫ (z : T4), primitiveInsertedMajorant C lam eps supportConstant n z ∂paperMeasure

Integrated form of the paper's one exceptional-endpoint sacrifice.

This lemma is deliberately applied only after the corresponding signed endpoint identity has been completed. It turns the ordinary primitive majorant produced by that identity into the inserted majorant, charging exactly the single eps^-2 cost prescribed in Step 4(A).

The retained outgoing terminal, jointly in its endpoint variables #

source

def Anderson4D.r324OutgoingTerminalJointRegroupMeasurableEquiv (Y : Type u_1) (T : Type u_2) (V : Type u_3) [MeasurableSpace Y] [MeasurableSpace T] [MeasurableSpace V] :

Y × T × V ≃ᵐ V × T × Y

Regroup the free outgoing variable, the retained primitive tuple, and the post-terminal carrier in the paper order (y,(t,v)) ↦ (v,(t,y)).

Equations

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

Instances For

source

@[simp]

theorem Anderson4D.r324OutgoingTerminalJointRegroupMeasurableEquiv_apply {Y : Type u_1} {T : Type u_2} {V : Type u_3} [MeasurableSpace Y] [MeasurableSpace T] [MeasurableSpace V] (q : Y × T × V) :

(r324OutgoingTerminalJointRegroupMeasurableEquiv Y T V) q = (q.2.2, q.2.1, q.1)

source

theorem Anderson4D.measurePreserving_r324OutgoingTerminalJointRegroupMeasurableEquiv {Y : Type u_1} {T : Type u_2} {V : Type u_3} [MeasurableSpace Y] [MeasurableSpace T] [MeasurableSpace V] (muY : MeasureTheory.Measure Y) (muT : MeasureTheory.Measure T) (muV : MeasureTheory.Measure V) [MeasureTheory.SFinite muY] [MeasureTheory.SFinite muT] [MeasureTheory.SFinite muV] :

MeasureTheory.MeasurePreserving (⇑(r324OutgoingTerminalJointRegroupMeasurableEquiv Y T V)) (muY.prod (muT.prod muV)) (muV.prod (muT.prod muY))

The endpoint/primitive/post regroup preserves the corresponding product measures.

source

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.outgoingEndpointDefectDensity {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) (coefficient : (data.terminalPost.SurvivingCoordinate → T4) → ℂ) (incomingMode outgoingMode : Z4) (x : T4) (v : data.terminalPost.SurvivingCoordinate → T4) (first : T4) :

ℂ

The signed post-terminal density after the retained primitive tuple and outgoing Fourier variable have both been evaluated.

Equations

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

Instances For

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.lamEps_pow_integral_stop_outgoingEndpoint_eq_defect {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) (hpred : r324WithinHalfPredecessorSlot data.endpoint.stop.state data.terminalData.terminal ≠ 0) (hactive : data.terminalPost.state.active.Nonempty) (coefficient : (data.terminalPost.SurvivingCoordinate → T4) → ℂ) (incomingMode outgoingMode : Z4) (x : T4) (hsource : MeasureTheory.Integrable (fun (q : T4 × (data.endpoint.stop.SurvivingCoordinate → T4)) => data.endpoint.stop.incomingPhasedResidualDensity (coefficient ((data.endpoint.stop.splitSurvivingPiMeasurableEquiv data.terminalData.terminal [] ⋯) q.2).2) incomingMode rho eps x q.1 q.2) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : data.endpoint.stop.SurvivingCoordinate) => paperMeasure))) (hint : ∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder data.terminalData.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder data.terminalData.terminal.2) (↑kappaB) data.terminalContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminalData.terminal.2) ⋯ first (first - gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2)) => paperMeasure)) :

↑(lamEps lam eps) ^ (2 * data.endpoint.stop.remainingOrder) * ∫ (q : T4 × (data.endpoint.stop.SurvivingCoordinate → T4)), charT4 outgoingMode q.1 * data.endpoint.stop.incomingPhasedResidualDensity (coefficient ((data.endpoint.stop.splitSurvivingPiMeasurableEquiv data.terminalData.terminal [] ⋯) q.2).2) incomingMode rho eps x q.1 q.2 ∂paperMeasure.prod (MeasureTheory.Measure.pi fun (x : data.endpoint.stop.SurvivingCoordinate) => paperMeasure) = ∫ (v : data.terminalPost.SurvivingCoordinate → T4), ∫ (first : T4), data.outgoingEndpointDefectDensity coefficient incomingMode outgoingMode x v first ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : data.terminalPost.SurvivingCoordinate) => paperMeasure

Joint stop-carrier form of the retained outgoing operation. This is the consumer used after an exceptional incoming endpoint has already been collapsed and transported to the stop immediately before the distinct outgoing terminal.

source

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointTerminalGeometry.paperOutgoingTerminal {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (data : R324WithinHalfEndpointTerminalGeometry pairing) :

(initial rho lam eps pairing).R324PaperOutgoingEndpointTerminal

View the canonical endpoint-terminal geometry as the arbitrary-prefix terminal package used by the exact outgoing Fourier calculation.

Equations

data.paperOutgoingTerminal = { terminalData := data.terminalData, endpoint := data.transport }

Instances For

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointTerminalGeometry.incomingErasedHeadOuterFactor_eq_terminalPost_endpointErasedSignedChain {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (data : R324WithinHalfEndpointTerminalGeometry pairing) (hpred : r324WithinHalfPredecessorSlot data.transport.stop.state data.terminalData.terminal ≠ 0) (hactive : (data.transport.stop.afterHead data.terminalData.terminal [] ⋯).state.active.Nonempty) (x y : T4) (v : (data.transport.stop.afterHead data.terminalData.terminal [] ⋯).SurvivingCoordinate → T4) :

data.transport.stop.incomingErasedHeadOuterFactor data.terminalData.terminal [] ⋯ rho eps x y v = (data.transport.stop.afterHead data.terminalData.terminal [] ⋯).endpointErasedSignedChain hactive x y ((data.transport.stop.afterHead data.terminalData.terminal [] ⋯).reconstruct v)

After the retained outgoing head is removed, its erased outer factor is exactly the completed post-terminal chain with both genuine boundary slots deleted. This is the pointwise seam needed to Fourier-integrate a direct incoming Green leg after the outgoing ordinary-J operation.

source

Exact joint outgoing-endpoint operation, starting at the initial residual half. The proper prefix is transported while the expression is still signed; the terminal primitive tuple and the outgoing endpoint are then regrouped and integrated in the paper order. The norm is nowhere taken.

source

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointTerminalGeometry.outgoingEndpointDefectDensity {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (data : R324WithinHalfEndpointTerminalGeometry pairing) (coefficient : (data.paperOutgoingTerminal.terminalPost.SurvivingCoordinate → T4) → ℂ) (incomingMode outgoingMode : Z4) (x : T4) (v : data.paperOutgoingTerminal.terminalPost.SurvivingCoordinate → T4) (first : T4) :

ℂ

The signed density exposed after the retained outgoing primitive tuple and external endpoint have both been integrated.

Equations

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

Instances For

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointTerminalGeometry.norm_outgoingEndpointDefectDensity_le_scaled {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {C supportConstant : ℝ} (data : R324WithinHalfEndpointTerminalGeometry pairing) (coefficient : (data.paperOutgoingTerminal.terminalPost.SurvivingCoordinate → T4) → ℂ) (incomingMode outgoingMode : Z4) (x : T4) (v : data.paperOutgoingTerminal.terminalPost.SurvivingCoordinate → T4) (first : T4) (heps : 0 < eps) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hprop : ∀ (H : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput (residualBlockOrder data.terminalData.terminal.2) H → MemEClassT4 (primitiveKernelDiff rho lam eps (residualBlockOrder data.terminalData.terminal.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff rho lam eps (residualBlockOrder data.terminalData.terminal.2) ⋯ H) ∧ PrimitiveKernelBounds rho lam eps (residualBlockOrder data.terminalData.terminal.2) ⋯ H supportConstant C) :

‖data.outgoingEndpointDefectDensity coefficient incomingMode outgoingMode x v first‖ ≤ |data.paperOutgoingTerminal.terminalContext.state.edges (r324WithinHalfPredecessorSlot data.paperOutgoingTerminal.terminalContext.state data.paperOutgoingTerminal.terminalContext.step) (data.paperOutgoingTerminal.terminalPredecessorPoint x v - first)| * paperSecondOrderModeDecay outgoingMode * (2 * r324WithinHalfInternalEdgeScaleProduct data.paperOutgoingTerminal.terminalContext data.transport.stopScale * ∫ (gap : T4), primitiveKernelMajorant C lam eps supportConstant (residualBlockOrder data.terminalData.terminal.2) gap ∂paperMeasure) * ‖data.paperOutgoingTerminal.terminalSplitOuter (fun (v : data.paperOutgoingTerminal.terminalPost.SurvivingCoordinate → T4) => data.transport.multiplier incomingMode * coefficient v) incomingMode x v‖

Quantitative form of the local outgoing endpoint operation. The norm is taken only after the ordinary primitive phase defect has been formed; the retained terminal is then charged by its transported edge certificate.

source

↑(lamEps lam eps) ^ (2 * (initial rho lam eps pairing).remainingOrder) * ∫ (q : U × T4 × ((initial rho lam eps pairing).SurvivingCoordinate → T4)), charT4 outgoingMode q.2.1 * (initial rho lam eps pairing).incomingPhasedResidualDensity (coefficient q.1 ((data.transport.stop.splitSurvivingPiMeasurableEquiv data.terminalData.terminal [] ⋯) (data.transport.projection q.2.2)).2) incomingMode rho eps (x q.1) q.2.1 q.2.2 ∂muU.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure)) = ∫ (u : U), ∫ (v : data.paperOutgoingTerminal.terminalPost.SurvivingCoordinate → T4), ∫ (first : T4), data.outgoingEndpointDefectDensity (coefficient u) incomingMode outgoingMode (x u) v first ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : data.paperOutgoingTerminal.terminalPost.SurvivingCoordinate) => paperMeasure ∂muU

Parameter-carrier form of the retained outgoing endpoint operation. An already completed opposite half may be carried in U; the terminal tuple and endpoint are still integrated sectionwise before the parameter integral and before any norm.

Exact root regrouping for a direct outgoing endpoint #

source

theorem Anderson4D.integral_rootProd_incomingPhasedResidualDensity_eq_directOutgoing {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix rho lam eps pairing) (hnil : res.remaining = []) (hactive : res.state.active.Nonempty) (hedge : res.state.edges (res.terminalOutgoingEdgeSlot hactive) = greenFn) {ZW : Type u_1} {VR : Type u_2} [MeasurableSpace ZW] [MeasurableSpace VR] (muZW : MeasureTheory.Measure ZW) (muVR : MeasureTheory.Measure VR) [MeasureTheory.SFinite muZW] [MeasureTheory.SFinite muVR] (red : ZW → VR → (res.SurvivingCoordinate → T4) → ℂ) (beta k : Z4) (hjoint : MeasureTheory.Integrable (fun (q : ((T4 × ZW) × VR) × (res.SurvivingCoordinate → T4)) => res.incomingPhasedResidualDensity (charT4 beta q.1.1.1 * red q.1.1.2 q.1.2 q.2) k rho eps 0 q.1.1.1 q.2) (((paperMeasure.prod muZW).prod muVR).prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))) :

∫ (q : ((T4 × ZW) × VR) × (res.SurvivingCoordinate → T4)), res.incomingPhasedResidualDensity (charT4 beta q.1.1.1 * red q.1.1.2 q.1.2 q.2) k rho eps 0 q.1.1.1 q.2 ∂((paperMeasure.prod muZW).prod muVR).prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = ∫ (s : ZW × VR), ∫ (u : res.SurvivingCoordinate → T4), red s.1 s.2 u * charT4 k (res.terminalIncomingAnchor (res.reconstruct u)) * ↑(res.endpointErasedSignedChain hactive 0 0 (res.reconstruct u)) * translatedGreenMode beta (res.terminalOutgoingAnchor hactive (res.reconstruct u)) ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure ∂muZW.prod muVR

Exact, signed version of the outgoing-endpoint regroup used in paper Step 4(A). The free outgoing variable is moved next to the completed half, its Green leg is Fourier-integrated, and the untouched opposite half and cross-covariance factor stay inside the outer integral. In particular, there is no triangle inequality in this statement.

The same terminal regrouping with one arbitrary untouched carrier.

source

def Anderson4D.r324SingleParameterTerminalRegroupMeasurableEquiv (Y : Type u_1) (U : Type u_2) (V : Type u_3) [MeasurableSpace Y] [MeasurableSpace U] [MeasurableSpace V] :

(Y × U) × V ≃ᵐ U × Y × V

Move the outgoing endpoint next to the terminal coordinates while leaving one arbitrary parameter carrier outside.

Equations

Anderson4D.r324SingleParameterTerminalRegroupMeasurableEquiv Y U V = MeasurableEquiv.prodAssoc.trans (Anderson4D.r324IncomingExceptionalHeadPullMeasurableEquiv Y U V)

Instances For

source

@[simp]

theorem Anderson4D.r324SingleParameterTerminalRegroupMeasurableEquiv_apply {Y : Type u_1} {U : Type u_2} {V : Type u_3} [MeasurableSpace Y] [MeasurableSpace U] [MeasurableSpace V] (q : (Y × U) × V) :

(r324SingleParameterTerminalRegroupMeasurableEquiv Y U V) q = (q.1.2, q.1.1, q.2)

source

@[simp]

theorem Anderson4D.r324SingleParameterTerminalRegroupMeasurableEquiv_symm_apply {Y : Type u_1} {U : Type u_2} {V : Type u_3} [MeasurableSpace Y] [MeasurableSpace U] [MeasurableSpace V] (q : U × Y × V) :

(r324SingleParameterTerminalRegroupMeasurableEquiv Y U V).symm q = ((q.2.1, q.1), q.2.2)

source

theorem Anderson4D.measurePreserving_r324SingleParameterTerminalRegroupMeasurableEquiv {Y : Type u_1} {U : Type u_2} {V : Type u_3} [MeasurableSpace Y] [MeasurableSpace U] [MeasurableSpace V] (muY : MeasureTheory.Measure Y) (muU : MeasureTheory.Measure U) (muV : MeasureTheory.Measure V) [MeasureTheory.SFinite muY] [MeasureTheory.SFinite muU] [MeasureTheory.SFinite muV] :

MeasureTheory.MeasurePreserving (⇑(r324SingleParameterTerminalRegroupMeasurableEquiv Y U V)) ((muY.prod muU).prod muV) (muU.prod (muY.prod muV))

The one-parameter terminal regroup preserves product measure.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.lamEps_pow_integral_singleParameter_stop_outgoingEndpoint_eq_defect {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) (hpred : r324WithinHalfPredecessorSlot data.endpoint.stop.state data.terminalData.terminal ≠ 0) (hactive : data.terminalPost.state.active.Nonempty) {U : Type u_1} [MeasurableSpace U] (muU : MeasureTheory.Measure U) [MeasureTheory.SFinite muU] (coefficient : U → (data.terminalPost.SurvivingCoordinate → T4) → ℂ) (incomingMode outgoingMode : Z4) (x : U → T4) (hsource : MeasureTheory.Integrable (fun (q : (T4 × U) × (data.endpoint.stop.SurvivingCoordinate → T4)) => data.endpoint.stop.incomingPhasedResidualDensity (coefficient q.1.2 ((data.endpoint.stop.splitSurvivingPiMeasurableEquiv data.terminalData.terminal [] ⋯) q.2).2) incomingMode rho eps (x q.1.2) q.1.1 q.2) ((paperMeasure.prod muU).prod (MeasureTheory.Measure.pi fun (x : data.endpoint.stop.SurvivingCoordinate) => paperMeasure))) (hint : ∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder data.terminalData.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder data.terminalData.terminal.2) (↑kappaB) data.terminalContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminalData.terminal.2) ⋯ first (first - gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2)) => paperMeasure)) :

↑(lamEps lam eps) ^ (2 * data.endpoint.stop.remainingOrder) * ∫ (q : (T4 × U) × (data.endpoint.stop.SurvivingCoordinate → T4)), charT4 outgoingMode q.1.1 * data.endpoint.stop.incomingPhasedResidualDensity (coefficient q.1.2 ((data.endpoint.stop.splitSurvivingPiMeasurableEquiv data.terminalData.terminal [] ⋯) q.2).2) incomingMode rho eps (x q.1.2) q.1.1 q.2 ∂(paperMeasure.prod muU).prod (MeasureTheory.Measure.pi fun (x : data.endpoint.stop.SurvivingCoordinate) => paperMeasure) = ∫ (u : U), ∫ (v : data.terminalPost.SurvivingCoordinate → T4), ∫ (first : T4), data.outgoingEndpointDefectDensity (coefficient u) incomingMode outgoingMode (x u) v first ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : data.terminalPost.SurvivingCoordinate) => paperMeasure ∂muU

Parameterized joint stop-carrier form of the retained outgoing operation. The untouched carrier is placed outside only after the signed endpoint integrand has been formed. This is the exact Fubini seam needed when the opposite half has already been collapsed by the exceptional incoming operation.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.norm_outgoingEndpointDefectDensity_le_scaled_of_certificate {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) (scale : Fin (m + 1) → ℝ) (hcertificate : R324WithinHalfEdgeCertificate data.terminalContext.state scale) (coefficient : (data.terminalPost.SurvivingCoordinate → T4) → ℂ) (incomingMode outgoingMode : Z4) (x : T4) (v : data.terminalPost.SurvivingCoordinate → T4) (first : T4) {primitiveConstant supportConstant : ℝ} (heps : 0 < eps) (hprimitive : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (hprop : ∀ (H : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput (residualBlockOrder data.terminalData.terminal.2) H → MemEClassT4 (primitiveKernelDiff rho lam eps (residualBlockOrder data.terminalData.terminal.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff rho lam eps (residualBlockOrder data.terminalData.terminal.2) ⋯ H) ∧ PrimitiveKernelBounds rho lam eps (residualBlockOrder data.terminalData.terminal.2) ⋯ H supportConstant primitiveConstant) :

‖data.outgoingEndpointDefectDensity coefficient incomingMode outgoingMode x v first‖ ≤ |data.terminalContext.state.edges (r324WithinHalfPredecessorSlot data.terminalContext.state data.terminalContext.step) (data.terminalPredecessorPoint x v - first)| * paperSecondOrderModeDecay outgoingMode * (2 * r324WithinHalfInternalEdgeScaleProduct data.terminalContext scale * ∫ (gap : T4), primitiveKernelMajorant primitiveConstant lam eps supportConstant (residualBlockOrder data.terminalData.terminal.2) gap ∂paperMeasure) * ‖data.terminalSplitOuter coefficient incomingMode x v‖

Certificate-ready bound for the generic retained outgoing defect. The exact ordinary primitive phase defect has already been formed, so this is the first point where its norm is taken.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.norm_integral_outgoingEndpointDefectDensity_le_scaled_of_certificate {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) (scale : Fin (m + 1) → ℝ) (hcertificate : R324WithinHalfEdgeCertificate data.terminalContext.state scale) (coefficient : (data.terminalPost.SurvivingCoordinate → T4) → ℂ) (incomingMode outgoingMode : Z4) (x : T4) (v : data.terminalPost.SurvivingCoordinate → T4) {primitiveConstant supportConstant : ℝ} (heps : 0 < eps) (hprimitive : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (hprop : ∀ (H : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput (residualBlockOrder data.terminalData.terminal.2) H → MemEClassT4 (primitiveKernelDiff rho lam eps (residualBlockOrder data.terminalData.terminal.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff rho lam eps (residualBlockOrder data.terminalData.terminal.2) ⋯ H) ∧ PrimitiveKernelBounds rho lam eps (residualBlockOrder data.terminalData.terminal.2) ⋯ H supportConstant primitiveConstant) :

‖∫ (first : T4), data.outgoingEndpointDefectDensity coefficient incomingMode outgoingMode x v first ∂paperMeasure‖ ≤ scale (r324WithinHalfPredecessorSlot data.terminalContext.state data.terminalContext.step) * invSqKerMass * paperSecondOrderModeDecay outgoingMode * (2 * r324WithinHalfInternalEdgeScaleProduct data.terminalContext scale * ∫ (gap : T4), primitiveKernelMajorant primitiveConstant lam eps supportConstant (residualBlockOrder data.terminalData.terminal.2) gap ∂paperMeasure) * ‖data.terminalSplitOuter coefficient incomingMode x v‖

Integrating the remaining predecessor endpoint preserves the outgoing Fourier decay and costs exactly the L¹ mass of that certified named edge. The triangle inequality is used only after the complete signed terminal defect has been formed.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.norm_integral_outgoingEndpointDefectDensity_le_inserted_of_certificate {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) (scale : Fin (m + 1) → ℝ) (hcertificate : R324WithinHalfEdgeCertificate data.terminalContext.state scale) (coefficient : (data.terminalPost.SurvivingCoordinate → T4) → ℂ) (incomingMode outgoingMode : Z4) (x : T4) (v : data.terminalPost.SurvivingCoordinate → T4) {primitiveConstant supportConstant : ℝ} (heps : 0 < eps) (hprimitive : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (hprop : ∀ (H : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput (residualBlockOrder data.terminalData.terminal.2) H → MemEClassT4 (primitiveKernelDiff rho lam eps (residualBlockOrder data.terminalData.terminal.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff rho lam eps (residualBlockOrder data.terminalData.terminal.2) ⋯ H) ∧ PrimitiveKernelBounds rho lam eps (residualBlockOrder data.terminalData.terminal.2) ⋯ H supportConstant primitiveConstant) :

‖∫ (first : T4), data.outgoingEndpointDefectDensity coefficient incomingMode outgoingMode x v first ∂paperMeasure‖ ≤ scale (r324WithinHalfPredecessorSlot data.terminalContext.state data.terminalContext.step) * invSqKerMass * paperSecondOrderModeDecay outgoingMode * (2 * r324WithinHalfInternalEdgeScaleProduct data.terminalContext scale * (SmoothCutoff.r324EndpointPrimitiveSacrifice eps SmoothCutoff.R324EndpointReductionCase.insertedSacrifice * ∫ (gap : T4), primitiveInsertedMajorant primitiveConstant lam eps supportConstant (residualBlockOrder data.terminalData.terminal.2) gap ∂paperMeasure)) * ‖data.terminalSplitOuter coefficient incomingMode x v‖

The same completed terminal estimate in the budget's inserted-kernel currency. Exactly one exceptional endpoint sacrifice is introduced; no cost is charged to the direct incoming endpoint carried by coefficient.

source

theorem Anderson4D.integral_singleParameter_incomingPhasedResidualDensity_eq_directOutgoing {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix rho lam eps pairing) (hnil : res.remaining = []) (hactive : res.state.active.Nonempty) (hedge : res.state.edges (res.terminalOutgoingEdgeSlot hactive) = greenFn) {U : Type u_1} [MeasurableSpace U] (muU : MeasureTheory.Measure U) [MeasureTheory.SFinite muU] (red : U → (res.SurvivingCoordinate → T4) → ℂ) (beta k : Z4) (hjoint : MeasureTheory.Integrable (fun (q : (T4 × U) × (res.SurvivingCoordinate → T4)) => res.incomingPhasedResidualDensity (charT4 beta q.1.1 * red q.1.2 q.2) k rho eps 0 q.1.1 q.2) ((paperMeasure.prod muU).prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))) :

∫ (q : (T4 × U) × (res.SurvivingCoordinate → T4)), res.incomingPhasedResidualDensity (charT4 beta q.1.1 * red q.1.2 q.2) k rho eps 0 q.1.1 q.2 ∂(paperMeasure.prod muU).prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = ∫ (s : U), ∫ (u : res.SurvivingCoordinate → T4), red s u * charT4 k (res.terminalIncomingAnchor (res.reconstruct u)) * ↑(res.endpointErasedSignedChain hactive 0 0 (res.reconstruct u)) * translatedGreenMode beta (res.terminalOutgoingAnchor hactive (res.reconstruct u)) ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure ∂muU

One-parameter form of the exact direct-outgoing Fourier regroup. This is the form used when the untouched parameter is the already-completed opposite half.

source

theorem Anderson4D.integrable_singleParameter_directOutgoingResult {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix rho lam eps pairing) (hnil : res.remaining = []) (hactive : res.state.active.Nonempty) (hedge : res.state.edges (res.terminalOutgoingEdgeSlot hactive) = greenFn) {U : Type u_1} [MeasurableSpace U] (muU : MeasureTheory.Measure U) [MeasureTheory.SFinite muU] (red : U → (res.SurvivingCoordinate → T4) → ℂ) (beta k : Z4) (hjoint : MeasureTheory.Integrable (fun (q : (T4 × U) × (res.SurvivingCoordinate → T4)) => res.incomingPhasedResidualDensity (charT4 beta q.1.1 * red q.1.2 q.2) k rho eps 0 q.1.1 q.2) ((paperMeasure.prod muU).prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))) :

MeasureTheory.Integrable (fun (q : U × (res.SurvivingCoordinate → T4)) => red q.1 q.2 * charT4 k (res.terminalIncomingAnchor (res.reconstruct q.2)) * ↑(res.endpointErasedSignedChain hactive 0 0 (res.reconstruct q.2)) * translatedGreenMode beta (res.terminalOutgoingAnchor hactive (res.reconstruct q.2))) (muU.prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))

Joint integrability survives the exact direct-outgoing Fourier evaluation. This is the Fubini license needed to hand a completed first half to the second half; it is derived from the same pre-Fourier joint integrability, not assumed independently.

Reindex the completed left endpoint carrier as the untouched parameter of the right initial source: (((z,w),v),u) ↦ ((z,(w,u)),v).

source

def Anderson4D.r324TwoHalfRightInitialSourceRegroupMeasurableEquiv (Z : Type u_1) (W : Type u_2) (V : Type u_3) (U : Type u_4) [MeasurableSpace Z] [MeasurableSpace W] [MeasurableSpace V] [MeasurableSpace U] :

((Z × W) × V) × U ≃ᵐ (Z × W × U) × V

Equations

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

Instances For

source

@[simp]

theorem Anderson4D.r324TwoHalfRightInitialSourceRegroupMeasurableEquiv_apply {Z : Type u_1} {W : Type u_2} {V : Type u_3} {U : Type u_4} [MeasurableSpace Z] [MeasurableSpace W] [MeasurableSpace V] [MeasurableSpace U] (q : ((Z × W) × V) × U) :

(r324TwoHalfRightInitialSourceRegroupMeasurableEquiv Z W V U) q = ((q.1.1.1, q.1.1.2, q.2), q.1.2)

source

theorem Anderson4D.measurePreserving_r324TwoHalfRightInitialSourceRegroupMeasurableEquiv {Z : Type u_1} {W : Type u_2} {V : Type u_3} {U : Type u_4} [MeasurableSpace Z] [MeasurableSpace W] [MeasurableSpace V] [MeasurableSpace U] (muZ : MeasureTheory.Measure Z) (muW : MeasureTheory.Measure W) (muV : MeasureTheory.Measure V) (muU : MeasureTheory.Measure U) [MeasureTheory.SFinite muZ] [MeasureTheory.SFinite muW] [MeasureTheory.SFinite muV] [MeasureTheory.SFinite muU] :

MeasureTheory.MeasurePreserving (⇑(r324TwoHalfRightInitialSourceRegroupMeasurableEquiv Z W V U)) (((muZ.prod muW).prod muV).prod muU) ((muZ.prod (muW.prod muU)).prod muV)

The paired-incoming/retained-outgoing endpoint coefficient #

source

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalRefinedRootEndpointReducedCoefficient {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} {outgoingTerminal : R322ExtractionStep m} (data : R324IncomingExceptionalStopTraceAssembly kappaP initialScale) (endpoint : R324WithinHalfEndpointStopAtTerminal outgoingTerminal (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯)) (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (s : (T4 × T4) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)) (u : endpoint.stop.SurvivingCoordinate → T4) :

ℂ

The coefficient left after the paired incoming operation, with the free outgoing character removed. The remaining parameter consists of the two opposite-half external variables and its still-signed residual carrier. This is an exact signed object; the ordinary primitive defects at both endpoints are estimated only after the outgoing operation.

Equations

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

Instances For

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.multiplier_mul_incomingExceptionalRefinedRootEndpointCoefficient_eq_char_mul_reduced {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} {outgoingTerminal : R322ExtractionStep m} (data : R324IncomingExceptionalStopTraceAssembly kappaP initialScale) (endpoint : R324WithinHalfEndpointStopAtTerminal outgoingTerminal (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯)) (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (y : T4) (s : (T4 × T4) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)) (u : endpoint.stop.SurvivingCoordinate → T4) :

endpoint.multiplier alpha * data.incomingExceptionalRefinedRootEndpointCoefficient endpoint alpha beta pi ((y, s.1), s.2) u = charT4 beta y * data.incomingExceptionalRefinedRootEndpointReducedCoefficient endpoint alpha beta pi s u

The original endpoint-stop coefficient factors as the free outgoing character times the reduced coefficient. This is precisely the algebraic seam required before the retained outgoing Fourier integration.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingPhasedResidualDensity_endpointCoefficient_eq_char_mul_reduced {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} {outgoingTerminal : R322ExtractionStep m} (data : R324IncomingExceptionalStopTraceAssembly kappaP initialScale) (endpoint : R324WithinHalfEndpointStopAtTerminal outgoingTerminal (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯)) (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (y : T4) (s : (T4 × T4) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)) (u : endpoint.stop.SurvivingCoordinate → T4) :

endpoint.stop.incomingPhasedResidualDensity (endpoint.multiplier alpha * data.incomingExceptionalRefinedRootEndpointCoefficient endpoint alpha beta pi ((y, s.1), s.2) u) alpha rho eps 0 y u = charT4 beta y * endpoint.stop.incomingPhasedResidualDensity (data.incomingExceptionalRefinedRootEndpointReducedCoefficient endpoint alpha beta pi s u) alpha rho eps 0 y u

Pointwise density form of the preceding coefficient factorization. The outgoing character is pulled out by linearity, while the signed stop density itself is left untouched.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.r324ResidualPrimitiveSumProduct_eq_leftOutgoingTerminalPost {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) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (u : outgoing.endpoint.stop.SurvivingCoordinate → T4) (v : (initial rho lam eps kappaM).SurvivingCoordinate → T4) :

r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi (r324TwoHalfRootDoubledReconstruct outgoing.endpoint.stop (initial rho lam eps kappaM) (u, v)) = r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi (r324TwoHalfRootDoubledReconstruct outgoing.terminalPost (initial rho lam eps kappaM) (((outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv outgoing.terminalData.terminal [] ⋯) u).2, v))

Removing the retained outgoing terminal does not change the cross-cut primitive factor: that factor is indexed only by residual singles, hence only by coordinates surviving in the post-terminal carrier.

source

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalRefinedRootOutgoingPostCoefficient {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 : (T4 × T4) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)) (v : outgoing.terminalPost.SurvivingCoordinate → T4) :

ℂ

The post-terminal coefficient used by the retained outgoing theorem. Its only left-half coordinates are the residual singles surviving after the terminal block; the terminal primitive tuple is absent by definition.

Equations

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

Instances For

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalRefinedRootEndpointReducedCoefficient_eq_post {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 : (T4 × T4) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)) (u : outgoing.endpoint.stop.SurvivingCoordinate → T4) :

data.incomingExceptionalRefinedRootEndpointReducedCoefficient outgoing.endpoint alpha beta pi s u = data.incomingExceptionalRefinedRootOutgoingPostCoefficient outgoing alpha beta pi s ((outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv outgoing.terminalData.terminal [] ⋯) u).2

The reduced stop coefficient factors literally through the post-terminal projection used by the outgoing primitive split.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_r324RefinedPhysicalIntegral_eq_incomingExceptional_outgoingExceptional {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {initialScale : Fin (m + 1) → ℝ} (p : R324RefinedScheduleIndex m) (e0 : MomentContraction m) (he0 : e0 ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (data : R324IncomingExceptionalStopTraceAssembly e0.fst initialScale) (outgoing : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324PaperOutgoingEndpointTerminal) (hm : 0 < m) (heps : 0 < eps) (heps1 : eps ≤ 1) (hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j)) (hincoming : ∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder data.terminal.2) (↑kappaB) data.stopContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure)) (hpred : r324WithinHalfPredecessorSlot outgoing.endpoint.stop.state outgoing.terminalData.terminal ≠ 0) (hactive : outgoing.terminalPost.state.active.Nonempty) (houtgoing : ∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder outgoing.terminalData.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder outgoing.terminalData.terminal.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder outgoing.terminalData.terminal.2) (↑kappaB) outgoing.terminalContext.internalEdges (primitiveAssemble (residualBlockOrder outgoing.terminalData.terminal.2) ⋯ first (first - gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder outgoing.terminalData.terminal.2 - 2)) => paperMeasure)) (alpha beta : Z4) (hsource : MeasureTheory.Integrable (fun (q : (T4 × (T4 × T4) × ((initial rho lam eps e0.snd.fst).SurvivingCoordinate → T4)) × (outgoing.endpoint.stop.SurvivingCoordinate → T4)) => outgoing.endpoint.stop.incomingPhasedResidualDensity (data.incomingExceptionalRefinedRootOutgoingPostCoefficient outgoing alpha beta e0.snd.snd q.1.2 ((outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv outgoing.terminalData.terminal [] ⋯) q.2).2) alpha rho eps 0 q.1.1 q.2) ((paperMeasure.prod ((paperMeasure.prod paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps e0.snd.fst).SurvivingCoordinate) => paperMeasure))).prod (MeasureTheory.Measure.pi fun (x : outgoing.endpoint.stop.SurvivingCoordinate) => paperMeasure))) :

↑(lamEps lam eps) ^ (2 * (initial rho lam eps e0.fst).remainingOrder) * r324RefinedPhysicalIntegral rho eps m alpha beta p = ∫ (s : (T4 × T4) × ((initial rho lam eps e0.snd.fst).SurvivingCoordinate → T4)), ∫ (v : outgoing.terminalPost.SurvivingCoordinate → T4), ∫ (first : T4), outgoing.outgoingEndpointDefectDensity (data.incomingExceptionalRefinedRootOutgoingPostCoefficient outgoing alpha beta e0.snd.snd s) alpha beta 0 v first ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : outgoing.terminalPost.SurvivingCoordinate) => paperMeasure ∂(paperMeasure.prod paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps e0.snd.fst).SurvivingCoordinate) => paperMeasure)

Exact paired-incoming/retained-outgoing splice at the genuine refined root. The incoming exceptional head and every proper-prefix interval are removed first. The root parameters are then only reassociated, and the retained terminal's primitive tuple and outgoing endpoint are integrated by the paper's ordinary-J operation. No norm occurs in this theorem.

The right-half cross-factor projection #

The pre-existing exceptional-stop projection theorem is stated for the first half of the doubled carrier. The paper uses the same operation on the second half after the first half has already been reduced. The next two lemmas are the literal right-half mirror and its composition with the complete after-head alternating transport. They are signed coordinate identities; no estimate is made here.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.r324ResidualPrimitiveSumProduct_eq_rightAfterHeadProjection {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (left : R324WithinHalfResidualPrefix rho lam eps kappaP) (data : R324IncomingExceptionalStopTraceAssembly kappaM initialScale) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (vl : left.SurvivingCoordinate → T4) (vr : (initial rho lam eps kappaM).SurvivingCoordinate → T4) :

r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi (r324TwoHalfRootDoubledReconstruct left (initial rho lam eps kappaM) (vl, vr)) = r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi (r324TwoHalfRootDoubledReconstruct left (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯) (vl, ((data.trace.stopPrefix.splitSurvivingPiMeasurableEquiv data.terminal data.suffix ⋯) (data.trace.stopProjection vr)).2))

Projecting the right initial tuple through its exceptional incoming stop and discarding the retained head does not change the cross-cut primitive factor. The already-completed left half is untouched.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.r324ResidualPrimitiveSumProduct_eq_rightDriverProjection {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (left : R324WithinHalfResidualPrefix rho lam eps kappaP) (data : R324IncomingExceptionalStopTraceAssembly kappaM initialScale) (sub : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (vl : left.SurvivingCoordinate → T4) (vr : (initial rho lam eps kappaM).SurvivingCoordinate → T4) :

r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi (r324TwoHalfRootDoubledReconstruct left (initial rho lam eps kappaM) (vl, vr)) = r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi (r324TwoHalfRootDoubledReconstruct left sub.final (vl, sub.projection ((data.trace.stopPrefix.splitSurvivingPiMeasurableEquiv data.terminal data.suffix ⋯) (data.trace.stopProjection vr)).2))

The same right-half cross factor may be read on the terminal carrier of the complete after-head alternating transport.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integrable_incomingExceptionalStopSourceDensity_of_initial {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {initialScale : Fin (m + 1) → ℝ} {pairing : PartialPairing (Fin m)} {Omega : Type u_1} [MeasurableSpace Omega] (nu : MeasureTheory.Measure Omega) [MeasureTheory.SFinite nu] (data : R324IncomingExceptionalStopTraceAssembly pairing initialScale) (k : Z4) (y : Omega → T4) (postOuter : Omega → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (hcurrent : MeasureTheory.Integrable (data.incomingExceptionalInitialSourceDensity k y postOuter) ((paperMeasure.prod nu).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure))) :

MeasureTheory.Integrable (data.incomingExceptionalStopSourceDensity k y postOuter) ((paperMeasure.prod nu).prod (MeasureTheory.Measure.pi fun (x : data.trace.stopPrefix.SurvivingCoordinate) => paperMeasure))

The initial-source Fubini license propagates to the certified exceptional stop. This is the integrability subproof already present in the trace/Fourier bridge, exposed here so the second half of the paper splice does not carry a redundant hypothesis.

source

↑(lamEps lam eps) ^ (2 * (initial rho lam eps e0.fst).remainingOrder) * r324RefinedPhysicalIntegral rho eps m alpha beta p = ∫ (s : (T4 × T4) × ((initial rho lam eps e0.snd.fst).SurvivingCoordinate → T4)), ∫ (u : transport.final.SurvivingCoordinate → T4), data.incomingExceptionalRefinedRootDriverReducedCoefficient transport alpha beta e0.snd.snd s.1 s.2 u * charT4 alpha (transport.final.terminalIncomingAnchor (transport.final.reconstruct u)) * ↑(transport.final.endpointErasedSignedChain hactive 0 0 (transport.final.reconstruct u)) * translatedGreenMode beta (transport.final.terminalOutgoingAnchor hactive (transport.final.reconstruct u)) ∂MeasureTheory.Measure.pi fun (x : transport.final.SurvivingCoordinate) => paperMeasure ∂(paperMeasure.prod paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps e0.snd.fst).SurvivingCoordinate) => paperMeasure)

The complete signed left-half splice in the incoming-exceptional/outgoing-direct case. The exceptional incoming head and every later left-half interval are removed exactly by the alternating transport. Only then is the free outgoing variable regrouped and Fourier-integrated. The right half and the entire cross-covariance factor remain signed inside the displayed outer integral.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_integral_initialResidual_eq_incomingExceptional_directOutgoing {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {initialScale : Fin (m + 1) → ℝ} {pairing : PartialPairing (Fin m)} (data : R324IncomingExceptionalStopTraceAssembly pairing initialScale) (sub : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) {ZW : Type u_1} {VR : Type u_2} [MeasurableSpace ZW] [MeasurableSpace VR] (muZW : MeasureTheory.Measure ZW) (muVR : MeasureTheory.Measure VR) [MeasureTheory.SFinite muZW] [MeasureTheory.SFinite muVR] (red : ZW → VR → (sub.final.SurvivingCoordinate → T4) → ℂ) (incomingMode outgoingMode : Z4) (hm : 0 < m) (hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j)) (hint : ∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder data.terminal.2) (↑kappaB) data.stopContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure)) (hcurrent : MeasureTheory.Integrable (data.incomingExceptionalInitialSourceDensity incomingMode (fun (omega : (T4 × ZW) × VR) => omega.1.1) fun (omega : (T4 × ZW) × VR) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) => charT4 outgoingMode omega.1.1 * red omega.1.2 omega.2 (sub.projection v)) ((paperMeasure.prod ((paperMeasure.prod muZW).prod muVR)).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure))) (hsource : MeasureTheory.Integrable (data.incomingExceptionalStopSourceDensity incomingMode (fun (omega : (T4 × ZW) × VR) => omega.1.1) fun (omega : (T4 × ZW) × VR) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) => charT4 outgoingMode omega.1.1 * red omega.1.2 omega.2 (sub.projection v)) ((paperMeasure.prod ((paperMeasure.prod muZW).prod muVR)).prod (MeasureTheory.Measure.pi fun (x : data.trace.stopPrefix.SurvivingCoordinate) => paperMeasure))) (hactive : sub.final.state.active.Nonempty) (hedge : sub.final.state.edges (sub.final.terminalOutgoingEdgeSlot hactive) = greenFn) (hterminal : MeasureTheory.Integrable (fun (q : ((T4 × ZW) × VR) × (sub.final.SurvivingCoordinate → T4)) => sub.final.incomingPhasedResidualDensity (charT4 outgoingMode q.1.1.1 * (sub.multiplier incomingMode * (↑(paperSecondOrderModeDecay incomingMode) ^ 2 * incomingExceptionalPrimitiveDefect rho lam eps (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges incomingMode * red q.1.1.2 q.1.2 q.2))) incomingMode rho eps 0 q.1.1.1 q.2) (((paperMeasure.prod muZW).prod muVR).prod (MeasureTheory.Measure.pi fun (x : sub.final.SurvivingCoordinate) => paperMeasure))) :

↑(lamEps lam eps) ^ (2 * (initial rho lam eps pairing).remainingOrder) * ∫ (p : (T4 × (T4 × ZW) × VR) × ((initial rho lam eps pairing).SurvivingCoordinate → T4)), data.incomingExceptionalInitialSourceDensity incomingMode (fun (omega : (T4 × ZW) × VR) => omega.1.1) (fun (omega : (T4 × ZW) × VR) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) => charT4 outgoingMode omega.1.1 * red omega.1.2 omega.2 (sub.projection v)) p ∂(paperMeasure.prod ((paperMeasure.prod muZW).prod muVR)).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure) = ∫ (s : ZW × VR), ∫ (u : sub.final.SurvivingCoordinate → T4), sub.multiplier incomingMode * (↑(paperSecondOrderModeDecay incomingMode) ^ 2 * incomingExceptionalPrimitiveDefect rho lam eps (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges incomingMode * red s.1 s.2 u) * charT4 incomingMode (sub.final.terminalIncomingAnchor (sub.final.reconstruct u)) * ↑(sub.final.endpointErasedSignedChain hactive 0 0 (sub.final.reconstruct u)) * translatedGreenMode outgoingMode (sub.final.terminalOutgoingAnchor hactive (sub.final.reconstruct u)) ∂MeasureTheory.Measure.pi fun (x : sub.final.SurvivingCoordinate) => paperMeasure ∂muZW.prod muVR

Generic signed two-endpoint splice for one half. It is the reusable paper Step-4(A) operation needed on the right copy: first transport the all-Green initial half to its exceptional incoming head, then collapse that head and every later half-block, and finally Fourier-integrate a direct outgoing Green leg. All parameters in ZW and VR remain untouched.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_integral_initialResidual_eq_singleParameter_incomingExceptional_directOutgoing {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {initialScale : Fin (m + 1) → ℝ} {pairing : PartialPairing (Fin m)} (data : R324IncomingExceptionalStopTraceAssembly pairing initialScale) (sub : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) {U : Type u_1} [MeasurableSpace U] (muU : MeasureTheory.Measure U) [MeasureTheory.SFinite muU] (red : U → (sub.final.SurvivingCoordinate → T4) → ℂ) (incomingMode outgoingMode : Z4) (hm : 0 < m) (hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j)) (hint : ∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder data.terminal.2) (↑kappaB) data.stopContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure)) (hcurrent : MeasureTheory.Integrable (data.incomingExceptionalInitialSourceDensity incomingMode (fun (omega : T4 × U) => omega.1) fun (omega : T4 × U) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) => charT4 outgoingMode omega.1 * red omega.2 (sub.projection v)) ((paperMeasure.prod (paperMeasure.prod muU)).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure))) (hsource : MeasureTheory.Integrable (data.incomingExceptionalStopSourceDensity incomingMode (fun (omega : T4 × U) => omega.1) fun (omega : T4 × U) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) => charT4 outgoingMode omega.1 * red omega.2 (sub.projection v)) ((paperMeasure.prod (paperMeasure.prod muU)).prod (MeasureTheory.Measure.pi fun (x : data.trace.stopPrefix.SurvivingCoordinate) => paperMeasure))) (hactive : sub.final.state.active.Nonempty) (hedge : sub.final.state.edges (sub.final.terminalOutgoingEdgeSlot hactive) = greenFn) (hterminal : MeasureTheory.Integrable (fun (q : (T4 × U) × (sub.final.SurvivingCoordinate → T4)) => sub.final.incomingPhasedResidualDensity (charT4 outgoingMode q.1.1 * (sub.multiplier incomingMode * (↑(paperSecondOrderModeDecay incomingMode) ^ 2 * incomingExceptionalPrimitiveDefect rho lam eps (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges incomingMode * red q.1.2 q.2))) incomingMode rho eps 0 q.1.1 q.2) ((paperMeasure.prod muU).prod (MeasureTheory.Measure.pi fun (x : sub.final.SurvivingCoordinate) => paperMeasure))) :

↑(lamEps lam eps) ^ (2 * (initial rho lam eps pairing).remainingOrder) * ∫ (p : (T4 × T4 × U) × ((initial rho lam eps pairing).SurvivingCoordinate → T4)), data.incomingExceptionalInitialSourceDensity incomingMode (fun (omega : T4 × U) => omega.1) (fun (omega : T4 × U) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) => charT4 outgoingMode omega.1 * red omega.2 (sub.projection v)) p ∂(paperMeasure.prod (paperMeasure.prod muU)).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure) = ∫ (s : U), ∫ (u : sub.final.SurvivingCoordinate → T4), sub.multiplier incomingMode * (↑(paperSecondOrderModeDecay incomingMode) ^ 2 * incomingExceptionalPrimitiveDefect rho lam eps (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges incomingMode * red s u) * charT4 incomingMode (sub.final.terminalIncomingAnchor (sub.final.reconstruct u)) * ↑(sub.final.endpointErasedSignedChain hactive 0 0 (sub.final.reconstruct u)) * translatedGreenMode outgoingMode (sub.final.terminalOutgoingAnchor hactive (sub.final.reconstruct u)) ∂MeasureTheory.Measure.pi fun (x : sub.final.SurvivingCoordinate) => paperMeasure ∂muU

Single-parameter form of the complete exceptional-incoming/direct- outgoing half splice. Its untouched parameter will be the terminal coordinate of the opposite half, so no dummy product carrier is needed in the two-half paper assembly.

Pointwise splice of the two exceptional-incoming/direct-outgoing halves #

source

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalTwoHalfDirectReducedCoefficient {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftSub : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324WithinHalfAlternatingTransport) (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (rightSub : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).R324WithinHalfAlternatingTransport) (hleft : leftSub.final.state.active.Nonempty) (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (u : leftSub.final.SurvivingCoordinate → T4) (v : rightSub.final.SurvivingCoordinate → T4) :

ℂ

The untouched coefficient carried from the completed left half while the right exceptional incoming endpoint is processed. It contains the left incoming defect, both exact left boundary coefficients, and the still-signed cross-cut primitive product on the two terminal carriers.

Equations

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

Instances For

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalLeftDirectIntegrand_eq_rightInitialSource {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftSub : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324WithinHalfAlternatingTransport) (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (rightSub : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).R324WithinHalfAlternatingTransport) (hleft : leftSub.final.state.active.Nonempty) (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (z w : T4) (vr : (initial rho lam eps kappaM).SurvivingCoordinate → T4) (u : leftSub.final.SurvivingCoordinate → T4) :

leftData.incomingExceptionalRefinedRootDriverReducedCoefficient leftSub alpha beta pi (z, w) vr u * charT4 alpha (leftSub.final.terminalIncomingAnchor (leftSub.final.reconstruct u)) * ↑(leftSub.final.endpointErasedSignedChain hleft 0 0 (leftSub.final.reconstruct u)) * translatedGreenMode beta (leftSub.final.terminalOutgoingAnchor hleft (leftSub.final.reconstruct u)) = rightData.incomingExceptionalInitialSourceDensity (-alpha) (fun (omega : T4 × (leftSub.final.SurvivingCoordinate → T4)) => omega.1) (fun (omega : T4 × (leftSub.final.SurvivingCoordinate → T4)) (v : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).SurvivingCoordinate → T4) => charT4 (-beta) omega.1 * leftData.incomingExceptionalTwoHalfDirectReducedCoefficient leftSub rightData rightSub hleft alpha beta pi omega.2 (rightSub.projection v)) ((z, w, u), vr)

The signed integrand left by the completed left half is literally the right half's exceptional-incoming initial source after projecting the cross factor through the right trace. This is the paper's two-half splice before the right endpoint integrations and before any norm.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integrable_incomingExceptionalLeftDirectIntegrand {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly kappaP initialScale) (sub : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (hm : 0 < m) (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hjoint : data.DriverTerminalJointIntegrable sub alpha beta pi) (hactive : sub.final.state.active.Nonempty) (hdirect : r324OutgoingIsShortcut kappaP = false) :

MeasureTheory.Integrable (fun (q : ((T4 × T4) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)) × (sub.final.SurvivingCoordinate → T4)) => data.incomingExceptionalRefinedRootDriverReducedCoefficient sub alpha beta pi q.1.1 q.1.2 q.2 * charT4 alpha (sub.final.terminalIncomingAnchor (sub.final.reconstruct q.2)) * ↑(sub.final.endpointErasedSignedChain hactive 0 0 (sub.final.reconstruct q.2)) * translatedGreenMode beta (sub.final.terminalOutgoingAnchor hactive (sub.final.reconstruct q.2))) (((paperMeasure.prod paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaM).SurvivingCoordinate) => paperMeasure)).prod (MeasureTheory.Measure.pi fun (x : sub.final.SurvivingCoordinate) => paperMeasure))

The completed left-half integrand is jointly integrable in the two right boundary variables, the right initial carrier, and the left terminal carrier. This is obtained by marginalizing the left outgoing Fourier variable from the already available driver-terminal joint integrability.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integrable_terminalDirectBoundaryCoefficient {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix rho lam eps pairing) (hnil : res.remaining = []) (hactive : res.state.active.Nonempty) (hedge : res.state.edges (res.terminalOutgoingEdgeSlot hactive) = greenFn) (scale : Fin (m + 1) → ℝ) (hcert : R324WithinHalfEdgeCertificate res.state scale) (incomingMode outgoingMode : Z4) :

MeasureTheory.Integrable (fun (u : res.SurvivingCoordinate → T4) => charT4 incomingMode (res.terminalIncomingAnchor (res.reconstruct u)) * ↑(res.endpointErasedSignedChain hactive 0 0 (res.reconstruct u)) * translatedGreenMode outgoingMode (res.terminalOutgoingAnchor hactive (res.reconstruct u))) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)

A terminal half with both boundary Green legs direct has an integrable two-endpoint Fourier coefficient after the outgoing variable is evaluated. The proof is the terminal-certificate L1 theorem followed by the exact Fourier identity, so it introduces no majorant into the signed chain.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integrable_twoIncomingExceptional_twoDirectTerminal_of_certificates {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftSub : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324WithinHalfAlternatingTransport) (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (rightSub : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).R324WithinHalfAlternatingTransport) (hm : 0 < m) (heps : 0 < eps) (heps1 : eps ≤ 1) (hleft : leftSub.final.state.active.Nonempty) (hleftDirect : r324OutgoingIsShortcut kappaP = false) (leftFinalScale rightFinalScale : Fin (m + 1) → ℝ) (hleftCert : R324WithinHalfEdgeCertificate leftSub.final.state leftFinalScale) (hrightCert : R324WithinHalfEdgeCertificate rightSub.final.state rightFinalScale) (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) :

have red := leftData.incomingExceptionalTwoHalfDirectReducedCoefficient leftSub rightData rightSub hleft alpha beta pi; MeasureTheory.Integrable (fun (q : (T4 × (leftSub.final.SurvivingCoordinate → T4)) × (rightSub.final.SurvivingCoordinate → T4)) => rightSub.final.incomingPhasedResidualDensity (charT4 (-beta) q.1.1 * (rightSub.multiplier (-alpha) * (↑(paperSecondOrderModeDecay (-alpha)) ^ 2 * incomingExceptionalPrimitiveDefect rho lam eps (residualBlockOrder rightData.terminal.2) ⋯ rightData.stopContext.internalEdges (-alpha) * red q.1.2 q.2))) (-alpha) rho eps 0 q.1.1 q.2) ((paperMeasure.prod (MeasureTheory.Measure.pi fun (x : leftSub.final.SurvivingCoordinate) => paperMeasure)).prod (MeasureTheory.Measure.pi fun (x : rightSub.final.SurvivingCoordinate) => paperMeasure))

Terminal joint integrability for the two-half exceptional-incoming/direct-outgoing splice. A certificate gives L1 for each completed half-chain; the cross primitive factor is bounded and measurable. Hence the only remaining factors are unimodular characters and constant primitive defects.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integrable_and_integral_leftDirect_eq_rightExceptionalInitialSource {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftSub : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324WithinHalfAlternatingTransport) (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (rightSub : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).R324WithinHalfAlternatingTransport) (hleft : leftSub.final.state.active.Nonempty) (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hleftIntegrable : MeasureTheory.Integrable (fun (q : ((T4 × T4) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)) × (leftSub.final.SurvivingCoordinate → T4)) => leftData.incomingExceptionalRefinedRootDriverReducedCoefficient leftSub alpha beta pi q.1.1 q.1.2 q.2 * charT4 alpha (leftSub.final.terminalIncomingAnchor (leftSub.final.reconstruct q.2)) * ↑(leftSub.final.endpointErasedSignedChain hleft 0 0 (leftSub.final.reconstruct q.2)) * translatedGreenMode beta (leftSub.final.terminalOutgoingAnchor hleft (leftSub.final.reconstruct q.2))) (((paperMeasure.prod paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaM).SurvivingCoordinate) => paperMeasure)).prod (MeasureTheory.Measure.pi fun (x : leftSub.final.SurvivingCoordinate) => paperMeasure))) :

Regrouping the completed left half produces exactly the right half's exceptional initial source, and transports integrability with it.

source

have red := leftData.incomingExceptionalTwoHalfDirectReducedCoefficient leftSub rightData rightSub hleftActive alpha beta e0.snd.snd; ↑(lamEps lam eps) ^ (2 * ((initial rho lam eps e0.fst).remainingOrder + (initial rho lam eps e0.snd.fst).remainingOrder)) * r324RefinedPhysicalIntegral rho eps m alpha beta p = ∫ (u : leftSub.final.SurvivingCoordinate → T4), ∫ (v : rightSub.final.SurvivingCoordinate → T4), rightSub.multiplier (-alpha) * (↑(paperSecondOrderModeDecay (-alpha)) ^ 2 * incomingExceptionalPrimitiveDefect rho lam eps (residualBlockOrder rightData.terminal.2) ⋯ rightData.stopContext.internalEdges (-alpha) * red u v) * charT4 (-alpha) (rightSub.final.terminalIncomingAnchor (rightSub.final.reconstruct v)) * ↑(rightSub.final.endpointErasedSignedChain hrightActive 0 0 (rightSub.final.reconstruct v)) * translatedGreenMode (-beta) (rightSub.final.terminalOutgoingAnchor hrightActive (rightSub.final.reconstruct v)) ∂MeasureTheory.Measure.pi fun (x : rightSub.final.SurvivingCoordinate) => paperMeasure ∂MeasureTheory.Measure.pi fun (x : leftSub.final.SurvivingCoordinate) => paperMeasure

Exact two-half paper splice when both incoming endpoints are paired exceptional heads and both outgoing endpoints are direct Green legs. The left half is removed first, its terminal coordinate becomes an untouched parameter of the right trace, and the right half is then removed with modes -alpha,-beta. No norm occurs in the statement or proof.

The actual refined-root endpoint cases #

source

theorem Anderson4D.r324RefinedEndpointReductionCase_direct_iff {m : ℕ} (hm : 0 < m) (p : R324RefinedScheduleIndex m) :

At positive order, the four entries of the canonical endpoint pattern are exactly the four tests appearing in paper Step 4(A): survival of the incoming internal vertex, and absence of an extracted outgoing chain edge, on the left and right halves respectively. Thus directFourier means that the external Green leg is integrated directly; its complementary case is the ordinary-J sacrifice.

This is a definitional classification only. It contains no estimate and, in particular, introduces no modulus before the signed removals.

source

theorem Anderson4D.r324RefinedSchedule_step4A_caseClassification {m : ℕ} (p : R324RefinedScheduleIndex m) :

The actual refined schedule has precisely the paper's branch split: either every contraction in the fibre is full/full (Step 1), or the representative has a residual single and each of its four external endpoints is one of the two Step-4(A) cases. The latter is recorded through the canonical case pattern, so downstream code can eliminate the sixteen combinations without inventing a separate routing interface.

source

theorem Anderson4D.last_mem_extractedRightEdges_of_isFull {m : ℕ} (hm : 0 < m) (pairing : PartialPairing (Fin m)) (hfull : pairing.IsFull) :

Fin.last m ∈ extractedRightEdges pairing

A full within-half pairing necessarily removes the outgoing chain edge. This is the right-endpoint half of the fact that every external endpoint is in the ordinary-J branch of paper Step 1.

source

theorem Anderson4D.r324RefinedEndpointReductionCase_eq_all_inserted_of_isFull {m : ℕ} (hm : 0 < m) (p : R324RefinedScheduleIndex m) (hfull : (r324RefinedScheduleRepresentative p).fst.IsFull ∧ (r324RefinedScheduleRepresentative p).snd.fst.IsFull) :

SmoothCutoff.r324RefinedEndpointReductionCase p = fun (x : Fin 4) => SmoothCutoff.R324EndpointReductionCase.insertedSacrifice

In the full/full branch every one of the four external endpoints is an insertedSacrifice endpoint. This is exactly paper Step 1: both copies are exhausted by fully paired intervals, so neither incoming vertex survives and both outgoing chain edges are removed.

source

theorem Anderson4D.r324EndpointPrimitiveSacrificeProduct_refined_eq_of_isFull {m : ℕ} (hm : 0 < m) (p : R324RefinedScheduleIndex m) (hfull : (r324RefinedScheduleRepresentative p).fst.IsFull ∧ (r324RefinedScheduleRepresentative p).snd.fst.IsFull) (epsilon : ℝ) :

SmoothCutoff.r324EndpointPrimitiveSacrificeProduct epsilon (SmoothCutoff.r324RefinedEndpointReductionCase p) = epsilon⁻¹ ^ 8

Consequently the full/full branch spends exactly the four ordinary-J sacrifices, namely epsilon^{-8}. This is the scalar endpoint ledger that will be multiplied only after the two signed Step-1 halves are assembled.

The residual incoming/outgoing exceptional blocks are distinct #

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.terminal_ne_outgoingTerminal_of_singles_nonempty {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly pairing initialScale) (outgoing : R324ShortcutTerminalSchedule pairing) (hm : 0 < m) (hsingles : pairing.singles.Nonempty) :

data.terminal ≠ outgoing.terminal

If a half has a residual single, its block beginning at the first internal vertex cannot also be the terminal block ending at the last internal vertex. Equality would make the terminal block the entire active carrier, so completing the schedule would leave finalActive = empty.

Exact direct/direct splice of the two completed halves #

source

theorem Anderson4D.R324TwoHalfTerminalData.endpointIntegratedResidualDensity_eq_of_four_direct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hm : 0 < m) (hleftOutgoing : Fin.last m ∉ extractedRightEdges κp) (hleftIncoming : ⟨0, hm⟩ ∈ finalActive κp) (hrightOutgoing : Fin.last m ∉ extractedRightEdges κm) (hrightIncoming : ⟨0, hm⟩ ∈ finalActive κm) (π : ↥κp.singles ≃ ↥κm.singles) (α β : Z4) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) :

terminal.endpointIntegratedResidualDensity π ⋯ ⋯ α β p = translatedGreenMode α (terminal.left.terminalIncomingAnchor (terminal.left.reconstruct p.1)) * translatedGreenMode β (terminal.left.terminalOutgoingAnchor ⋯ (terminal.left.reconstruct p.1)) * (translatedGreenMode (-α) (terminal.right.terminalIncomingAnchor (terminal.right.reconstruct p.2)) * translatedGreenMode (-β) (terminal.right.terminalOutgoingAnchor ⋯ (terminal.right.reconstruct p.2))) * terminal.endpointErasedResidualSumTerminalCore π ⋯ ⋯ p

After all signed within-half removals, four direct external legs give the literal product of their four translated Green modes and the still grouped endpoint-erased residual core.

source

theorem Anderson4D.R324TwoHalfTerminalData.norm_endpointIntegratedResidualDensity_eq_of_four_direct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hm : 0 < m) (hleftOutgoing : Fin.last m ∉ extractedRightEdges κp) (hleftIncoming : ⟨0, hm⟩ ∈ finalActive κp) (hrightOutgoing : Fin.last m ∉ extractedRightEdges κm) (hrightIncoming : ⟨0, hm⟩ ∈ finalActive κm) (π : ↥κp.singles ≃ ↥κm.singles) (α β : Z4) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) :

‖terminal.endpointIntegratedResidualDensity π ⋯ ⋯ α β p‖ = paperFourthOrderModeDecay α * paperFourthOrderModeDecay β * ‖terminal.endpointErasedResidualSumTerminalCore π ⋯ ⋯ p‖

The first norm in the four-direct branch is taken after all four exact Fourier integrations. Its multiplier is precisely <alpha>^-4 <beta>^-4.

Actual refined root, with all four direct endpoints #

source

theorem Anderson4D.lamEps_pow_r324RefinedPhysicalIntegral_eq_initialNestedEndpoint {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftTrace : (R324WithinHalfResidualPrefix.initial ρ lam ε κp).R324WithinHalfCertifiedAnalyticTrace leftScale) (rightTrace : (R324WithinHalfResidualPrefix.initial ρ lam ε κm).R324WithinHalfCertifiedAnalyticTrace rightScale) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : leftTrace.terminalPrefix.state.active.Nonempty) (hright : rightTrace.terminalPrefix.state.active.Nonempty) (α β : Z4) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hs : s ∈ momentContractionSignatures m) (hr : r ∈ momentResidualChainSignaturesAt m s) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (hκp : e₀.fst = κp) (hκm : e₀.snd.fst = κm) (hπ : e₀.snd.snd ≍ π) (hε : 0 < ε) (hε1 : ε ≤ 1) :

let terminal := R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace; ↑(lamEps lam ε) ^ (2 * ((R324WithinHalfResidualPrefix.initial ρ lam ε κp).remainingOrder + (R324WithinHalfResidualPrefix.initial ρ lam ε κm).remainingOrder)) * r324RefinedPhysicalIntegral ρ ε m α β ⟨⟨s, hs⟩, ⟨r, hr⟩⟩ = ∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedEndpointIntegratedResidualDensity π hleft hright α β v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure

Exact signed collapse from the genuine refined physical root to the endpoint-integrated nested carrier. This is the physical-integral form of the Steps 2--3 identity; no norm is introduced by the adapter.

source

theorem Anderson4D.norm_lamEps_pow_r324RefinedPhysicalIntegral_le_of_four_direct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftTrace : (R324WithinHalfResidualPrefix.initial ρ lam ε κp).R324WithinHalfCertifiedAnalyticTrace leftScale) (rightTrace : (R324WithinHalfResidualPrefix.initial ρ lam ε κm).R324WithinHalfCertifiedAnalyticTrace rightScale) (π : ↥κp.singles ≃ ↥κm.singles) (hm : 0 < m) (hleftOutgoing : Fin.last m ∉ extractedRightEdges κp) (hleftIncoming : ⟨0, hm⟩ ∈ finalActive κp) (hrightOutgoing : Fin.last m ∉ extractedRightEdges κm) (hrightIncoming : ⟨0, hm⟩ ∈ finalActive κm) (α β : Z4) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hs : s ∈ momentContractionSignatures m) (hr : r ∈ momentResidualChainSignaturesAt m s) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (hκp : e₀.fst = κp) (hκm : e₀.snd.fst = κm) (hπ : e₀.snd.snd ≍ π) (hε : 0 < ε) (hε1 : ε ≤ 1) :

have terminal := R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace; have hleft := ⋯; have hright := ⋯; |lamEps lam ε| ^ (2 * ((R324WithinHalfResidualPrefix.initial ρ lam ε κp).remainingOrder + (R324WithinHalfResidualPrefix.initial ρ lam ε κm).remainingOrder)) * ‖r324RefinedPhysicalIntegral ρ ε m α β ⟨⟨s, hs⟩, ⟨r, hr⟩⟩‖ ≤ paperFourthOrderModeDecay α * paperFourthOrderModeDecay β * ∫ (v : terminal.NestedCoordinate π → T4), ‖terminal.endpointErasedResidualSumTerminalCore π hleft hright ((terminal.terminalProductPiMeasurableEquivNested π).symm v)‖ ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure

In the four-direct residual branch, the genuine refined root has the paper's ⟨α⟩⁻⁴⟨β⟩⁻⁴ factor before any absolute-value estimate is made on the complete endpoint-erased core.

The four-direct core in complete-run currency #

source

theorem Anderson4D.r324_invSqKerMass_pos :

0 < invSqKerMass

The inverse-square model kernel has strictly positive total mass. This small fact lets the public grouped-to-complete-run identity be cancelled down to its endpoint-erased core, instead of duplicating its coordinate-reindexing proof.

source

let terminal := ofCertifiedTraces leftTrace rightTrace; have hleft := ⋯; have hright := ⋯; ‖terminal.endpointIntegratedResidualDensity pi hleft hright alpha beta p‖ ≤ paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * (leftTrace.terminalPrefix.endpointErasedScaleProduct hleft leftTrace.terminalScale * leftTrace.terminalPrefix.endpointErasedInvSqChainProduct hleft p.1 * (rightTrace.terminalPrefix.endpointErasedScaleProduct hright rightTrace.terminalScale * rightTrace.terminalPrefix.endpointErasedInvSqChainProduct hright p.2) * r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi ((ofCertifiedTraces leftTrace rightTrace).terminalDoubledReconstruct p))

Pointwise four-direct endpoint estimate with only the two endpoint-erased terminal paths majorized.

The four external Green legs have already been Fourier-integrated in norm_endpointIntegratedResidualDensity_eq_of_four_direct, so their exact fourth-order mode weights stay outside. The only subsequent inequalities are the two terminal certificate bounds and the nonnegativity of the still grouped residual primitive sum. This is the paper-order input for the complete nested run: no external endpoint scale or inverse-square mass is introduced.

source

noncomputable def Anderson4D.R324TwoHalfTerminalData.fourDirectEndpointErasedGroupedCore {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam eps kappaP kappaM) (leftScale rightScale : Fin (m + 1) → ℝ) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) :

ℝ

The positive terminal core remaining after four direct Fourier integrations. In contrast to endpointIntegratedGroupedMajorant, the two external scales and four inverse-square endpoint masses are absent.

Equations

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

Instances For

source

theorem Anderson4D.R324TwoHalfTerminalData.ae_norm_endpointIntegratedResidualDensity_le_fourDirectCore {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftInitialScale rightInitialScale : Fin (m + 1) → ℝ} (leftTrace : (R324WithinHalfResidualPrefix.initial rho lam eps kappaP).R324WithinHalfCertifiedAnalyticTrace leftInitialScale) (rightTrace : (R324WithinHalfResidualPrefix.initial rho lam eps kappaM).R324WithinHalfCertifiedAnalyticTrace rightInitialScale) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hm : 0 < m) (hleftOutgoing : Fin.last m ∉ extractedRightEdges kappaP) (hleftIncoming : ⟨0, hm⟩ ∈ finalActive kappaP) (hrightOutgoing : Fin.last m ∉ extractedRightEdges kappaM) (hrightIncoming : ⟨0, hm⟩ ∈ finalActive kappaM) (alpha beta : Z4) :

let terminal := ofCertifiedTraces leftTrace rightTrace; have hleft := ⋯; have hright := ⋯; (fun (p : (leftTrace.terminalPrefix.SurvivingCoordinate → T4) × (rightTrace.terminalPrefix.SurvivingCoordinate → T4)) => ‖terminal.endpointIntegratedResidualDensity pi hleft hright alpha beta p‖) ≤ᵐ[(MeasureTheory.Measure.pi fun (x : leftTrace.terminalPrefix.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : rightTrace.terminalPrefix.SurvivingCoordinate) => paperMeasure)] fun (p : (leftTrace.terminalPrefix.SurvivingCoordinate → T4) × (rightTrace.terminalPrefix.SurvivingCoordinate → T4)) => paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * terminal.fourDirectEndpointErasedGroupedCore leftTrace.terminalScale rightTrace.terminalScale hleft hright pi p

Almost-everywhere terminal-product form of the preceding four-direct estimate. This is the exact boundary consumed by the nested-cross reindexing: the Fourier decay is already outside and all diagonal exceptions have been removed under product Haar measure.

source

noncomputable def Anderson4D.R324TwoHalfTerminalData.initialNestedFourDirectEndpointErasedGroupedCore {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam eps kappaP kappaM) (leftScale rightScale : Fin (m + 1) → ℝ) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (v : terminal.NestedCoordinate pi → T4) :

ℝ

Pull the endpoint-erased four-direct core back to the literal initial nested-cross carrier.

Equations

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

Instances For

source

theorem Anderson4D.R324TwoHalfTerminalData.ae_norm_initialNestedEndpointIntegratedResidualDensity_le_fourDirectCore {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftInitialScale rightInitialScale : Fin (m + 1) → ℝ} (leftTrace : (R324WithinHalfResidualPrefix.initial rho lam eps kappaP).R324WithinHalfCertifiedAnalyticTrace leftInitialScale) (rightTrace : (R324WithinHalfResidualPrefix.initial rho lam eps kappaM).R324WithinHalfCertifiedAnalyticTrace rightInitialScale) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hm : 0 < m) (hleftOutgoing : Fin.last m ∉ extractedRightEdges kappaP) (hleftIncoming : ⟨0, hm⟩ ∈ finalActive kappaP) (hrightOutgoing : Fin.last m ∉ extractedRightEdges kappaM) (hrightIncoming : ⟨0, hm⟩ ∈ finalActive kappaM) (alpha beta : Z4) :

have terminal := ofCertifiedTraces leftTrace rightTrace; have hleft := ⋯; have hright := ⋯; (fun (v : terminal.NestedCoordinate pi → T4) => ‖terminal.initialNestedEndpointIntegratedResidualDensity pi hleft hright alpha beta v‖) ≤ᵐ[MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure] fun (v : terminal.NestedCoordinate pi → T4) => paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * terminal.initialNestedFourDirectEndpointErasedGroupedCore leftTrace.terminalScale rightTrace.terminalScale hleft hright pi v

Initial nested-carrier form of the four-direct endpoint estimate.

source

theorem Anderson4D.R324TwoHalfTerminalData.initialNestedFourDirectEndpointErasedGroupedCore_mul_coupling_eq {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam eps kappaP kappaM) (leftScale rightScale : Fin (m + 1) → ℝ) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (head : R324NestedCrossBlock kappaP kappaM pi) (tail : List (R324NestedCrossBlock kappaP kappaM pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remaining = head :: tail) (v : terminal.NestedCoordinate pi → T4) :

let step := r324InitialNestedCrossStepContext kappaP kappaM pi head tail hremaining; have hleftInitial := ⋯; have hrightInitial := ⋯; lamEps lam eps ^ (2 * step.residual.remainingOrder) * terminal.initialNestedFourDirectEndpointErasedGroupedCore leftScale rightScale hleft hright pi v = terminal.left.endpointErasedScaleProduct hleft leftScale * terminal.right.endpointErasedScaleProduct hright rightScale * terminal.completeNestedRunDensity step hleftInitial hrightInitial v

Exact coupling identity for the four-direct core.

The existing grouped-to-complete-run theorem contains four artificial inverse-square endpoint masses because it was designed for arbitrary terminal kernels. Here all four endpoint kernels have already been Fourier-integrated. We instantiate that theorem with unit scales and cancel its strictly positive inverse-square mass, leaving exactly the two endpoint-erased scale products times the literal complete nested run.

source

theorem Anderson4D.R324TwoHalfTerminalData.ae_coupling_mul_norm_initialNestedEndpointIntegratedResidualDensity_le_fourDirectRun {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftInitialScale rightInitialScale : Fin (m + 1) → ℝ} (leftTrace : (R324WithinHalfResidualPrefix.initial rho lam eps kappaP).R324WithinHalfCertifiedAnalyticTrace leftInitialScale) (rightTrace : (R324WithinHalfResidualPrefix.initial rho lam eps kappaM).R324WithinHalfCertifiedAnalyticTrace rightInitialScale) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hm : 0 < m) (hleftOutgoing : Fin.last m ∉ extractedRightEdges kappaP) (hleftIncoming : ⟨0, hm⟩ ∈ finalActive kappaP) (hrightOutgoing : Fin.last m ∉ extractedRightEdges kappaM) (hrightIncoming : ⟨0, hm⟩ ∈ finalActive kappaM) (head : R324NestedCrossBlock kappaP kappaM pi) (tail : List (R324NestedCrossBlock kappaP kappaM pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remaining = head :: tail) (alpha beta : Z4) :

have terminal := ofCertifiedTraces leftTrace rightTrace; have hleft := ⋯; have hright := ⋯; let step := r324InitialNestedCrossStepContext kappaP kappaM pi head tail hremaining; have hleftInitial := ⋯; have hrightInitial := ⋯; (fun (v : terminal.NestedCoordinate pi → T4) => lamEps lam eps ^ (2 * step.residual.remainingOrder) * ‖terminal.initialNestedEndpointIntegratedResidualDensity pi hleft hright alpha beta v‖) ≤ᵐ[MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure] fun (v : terminal.NestedCoordinate pi → T4) => paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * (terminal.left.endpointErasedScaleProduct hleft leftTrace.terminalScale * terminal.right.endpointErasedScaleProduct hright rightTrace.terminalScale * terminal.completeNestedRunDensity step hleftInitial hrightInitial v)

Paper-order four-direct endpoint estimate in the literal complete-run currency. The coupling power is inserted only after the four exact Fourier operations and the first norm; the preceding exact identity then moves it onto the nested run.

source

theorem Anderson4D.R324TwoHalfTerminalData.integral_coupling_mul_norm_initialNestedEndpointIntegratedResidualDensity_le_fourDirectRun {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftInitialScale rightInitialScale : Fin (m + 1) → ℝ} (leftTrace : (R324WithinHalfResidualPrefix.initial rho lam eps kappaP).R324WithinHalfCertifiedAnalyticTrace leftInitialScale) (rightTrace : (R324WithinHalfResidualPrefix.initial rho lam eps kappaM).R324WithinHalfCertifiedAnalyticTrace rightInitialScale) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hm : 0 < m) (hleftOutgoing : Fin.last m ∉ extractedRightEdges kappaP) (hleftIncoming : ⟨0, hm⟩ ∈ finalActive kappaP) (hrightOutgoing : Fin.last m ∉ extractedRightEdges kappaM) (hrightIncoming : ⟨0, hm⟩ ∈ finalActive kappaM) (head : R324NestedCrossBlock kappaP kappaM pi) (tail : List (R324NestedCrossBlock kappaP kappaM pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remaining = head :: tail) (alpha beta : Z4) (hlam : 0 < lam) (heps : 0 < eps) (heps1 : eps ≤ 1) (hlog : 1 ≤ |Real.log eps|) (hmtrunc : m ≤ truncOrder eps) :

have terminal := ofCertifiedTraces leftTrace rightTrace; have hleft := ⋯; have hright := ⋯; have step := r324InitialNestedCrossStepContext kappaP kappaM pi head tail hremaining; have hleftInitial := ⋯; have hrightInitial := ⋯; (∫ (v : terminal.NestedCoordinate pi → T4), lamEps lam eps ^ (2 * step.residual.remainingOrder) * ‖terminal.initialNestedEndpointIntegratedResidualDensity pi hleft hright alpha beta v‖ ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure) ≤ paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * (terminal.left.endpointErasedScaleProduct hleft leftTrace.terminalScale * terminal.right.endpointErasedScaleProduct hright rightTrace.terminalScale) * ∫ (v : step.SurvivingCoordinate → T4), terminal.completeNestedRunDensity step hleftInitial hrightInitial v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure

Integrated four-direct endpoint estimate. The right-hand side is the literal complete nested run multiplied only by the two endpoint-erased terminal scale products and the exact Fourier weights.

source

theorem Anderson4D.R324TwoHalfTerminalData.integral_coupling_mul_norm_initialNestedEndpointIntegratedResidualDensity_le_fourDirectMajorant {rho : SmoothCutoff} {lam eps B supportConstant : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftInitialScale rightInitialScale : Fin (m + 1) → ℝ} (leftTrace : (R324WithinHalfResidualPrefix.initial rho lam eps kappaP).R324WithinHalfCertifiedAnalyticTrace leftInitialScale) (rightTrace : (R324WithinHalfResidualPrefix.initial rho lam eps kappaM).R324WithinHalfCertifiedAnalyticTrace rightInitialScale) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hm : 0 < m) (hleftOutgoing : Fin.last m ∉ extractedRightEdges kappaP) (hleftIncoming : ⟨0, hm⟩ ∈ finalActive kappaP) (hrightOutgoing : Fin.last m ∉ extractedRightEdges kappaM) (hrightIncoming : ⟨0, hm⟩ ∈ finalActive kappaM) (head : R324NestedCrossBlock kappaP kappaM pi) (tail : List (R324NestedCrossBlock kappaP kappaM pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remaining = head :: tail) (alpha beta : Z4) (hlam : 0 < lam) (heps : 0 < eps) (heps1 : eps ≤ 1) (hlog : 1 ≤ |Real.log eps|) (hmtrunc : m ≤ truncOrder eps) (hrunBound : have terminal := ofCertifiedTraces leftTrace rightTrace; have step := r324InitialNestedCrossStepContext kappaP kappaM pi head tail hremaining; have hleftInitial := ⋯; have hrightInitial := ⋯; (∫ (v : step.SurvivingCoordinate → T4), terminal.completeNestedRunDensity step hleftInitial hrightInitial v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure) ≤ ∫ (z : T4), primitiveInsertedMajorant B lam eps supportConstant step.residual.remainingOrder z ∂paperMeasure) :

have terminal := ofCertifiedTraces leftTrace rightTrace; have hleft := ⋯; have hright := ⋯; have step := r324InitialNestedCrossStepContext kappaP kappaM pi head tail hremaining; (∫ (v : terminal.NestedCoordinate pi → T4), lamEps lam eps ^ (2 * step.residual.remainingOrder) * ‖terminal.initialNestedEndpointIntegratedResidualDensity pi hleft hright alpha beta v‖ ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure) ≤ paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * (terminal.left.endpointErasedScaleProduct hleft leftTrace.terminalScale * terminal.right.endpointErasedScaleProduct hright rightTrace.terminalScale) * ∫ (z : T4), primitiveInsertedMajorant B lam eps supportConstant step.residual.remainingOrder z ∂paperMeasure

Consume the existing complete-run primitive-majorant estimate without changing the four-direct endpoint ledger. In particular, the exact two Fourier decays and the endpoint-erased terminal scale product stay outside the run integral.

source

theorem Anderson4D.R324WithinHalfBudgetScaleReachable.edge_zero_eq_base_of_first_mem_active {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {state : R324WithinHalfEdgeState m} {scale : Fin (m + 1) → ℝ} (hreach : R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A state scale) (hm : 0 < m) (hfirst : ⟨0, hm⟩ ∈ state.active) :

scale 0 = A

Budget counterpart of the direct incoming geometry: if the first internal vertex survives, no literal head can have updated slot zero, so its numerical scale is still the initial Green base.

source

theorem Anderson4D.R324WithinHalfResidualPrefix.R324CompatibleAnalyticBudgetTrace.initial_analytic_endpointErasedScaleProduct_le_closedForm_of_direct {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (data : (initial rho lam eps pairing).R324CompatibleAnalyticBudgetTrace fun (x : Fin (m + 1)) => A) (hA : 1 ≤ A) (hm : 0 < m) (houtgoing : Fin.last m ∉ extractedRightEdges pairing) (hincoming : ⟨0, hm⟩ ∈ finalActive pairing) (hactive : data.analytic.terminalPrefix.state.active.Nonempty) :

data.analytic.terminalPrefix.endpointErasedScaleProduct hactive data.analytic.terminalScale ≤ A ^ (m + 1) * (C * lam) ^ (2 * (initial rho lam eps pairing).remainingOrder) * K ^ data.analytic.terminalPrefix.state.processed.length

In a direct/direct half, deleting the two external scale slots can only decrease the compatible complete budget: both omitted numerical boundary slots are still the initial base A, and A >= 1.

Complete-budget terminal scales, independent of endpoint cases #

source

theorem Anderson4D.r324_twoHalf_reachable_terminalScale_mul_majorant_le {rho : SmoothCutoff} {C K A B lam eps supportConstant : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (hA : 0 ≤ A) (hC : 0 ≤ C) (hK : 0 ≤ K) (hB : 0 ≤ B) (hlam : 0 ≤ lam) (terminal : R324TwoHalfTerminalData rho lam eps kappaP kappaM) (leftScale rightScale : Fin (m + 1) → ℝ) (leftReachable : R324WithinHalfBudgetScaleReachable kappaP rho C lam eps K A terminal.left.state leftScale) (rightReachable : R324WithinHalfBudgetScaleReachable kappaM rho C lam eps K A terminal.right.state rightScale) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hm : 1 ≤ m) (z : T4) :

((∏ edge ∈ terminal.left.activeEdgeSlots, leftScale edge) * ∏ edge ∈ terminal.right.activeEdgeSlots, rightScale edge) * invSqKerMass ^ 4 * primitiveInsertedMajorant B lam eps supportConstant (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remainingOrder z ≤ primitiveInsertedMajorant (r324TwoHalfCompleteAbsorbedBase A C K B) lam eps supportConstant m z

Two completed budget histories, possibly obtained through exceptional endpoint stops rather than the ordinary certified trace, have the same ambient-order scale closure. This is the common numerical consumer for all sixteen endpoint patterns: the endpoint calculation may change the dependent terminal carrier, but it does not change the exact complete budget recurrence.

source

theorem Anderson4D.r324_twoHalf_reachable_terminalScale_mul_integral_majorant_le {rho : SmoothCutoff} {C K A B lam eps supportConstant : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (hA : 0 ≤ A) (hC : 0 ≤ C) (hK : 0 ≤ K) (hB : 0 ≤ B) (hlam : 0 ≤ lam) (heps : 0 < eps) (terminal : R324TwoHalfTerminalData rho lam eps kappaP kappaM) (leftScale rightScale : Fin (m + 1) → ℝ) (leftReachable : R324WithinHalfBudgetScaleReachable kappaP rho C lam eps K A terminal.left.state leftScale) (rightReachable : R324WithinHalfBudgetScaleReachable kappaM rho C lam eps K A terminal.right.state rightScale) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hm : 1 ≤ m) :

((∏ edge ∈ terminal.left.activeEdgeSlots, leftScale edge) * ∏ edge ∈ terminal.right.activeEdgeSlots, rightScale edge) * invSqKerMass ^ 4 * ∫ (z : T4), primitiveInsertedMajorant B lam eps supportConstant (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remainingOrder z ∂paperMeasure ≤ ∫ (z : T4), primitiveInsertedMajorant (r324TwoHalfCompleteAbsorbedBase A C K B) lam eps supportConstant m z ∂paperMeasure

Integrated form of the complete-budget terminal-scale closure. Unlike the direct/direct specialization below, this theorem only asks that each completed half carry a reachable budget scale, so it is available after either direct or exceptional endpoint elimination.

source

def Anderson4D.R324TwoHalfTerminalData.ofAlternatingTransports {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftRes : R324WithinHalfResidualPrefix rho lam eps kappaP} {rightRes : R324WithinHalfResidualPrefix rho lam eps kappaM} (leftTransport : leftRes.R324WithinHalfAlternatingTransport) (rightTransport : rightRes.R324WithinHalfAlternatingTransport) :

R324TwoHalfTerminalData rho lam eps kappaP kappaM

Package the completed carriers of two literal alternating transports. This is the endpoint-pattern analogue of ofCertifiedTraces: exceptional heads may have occurred, but both transports still finish the same paper schedule.

Equations

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

Instances For

source

noncomputable def Anderson4D.R324TwoHalfTerminalData.initialNestedPullback {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam eps kappaP kappaM) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (density : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4) → ℂ) (v : terminal.NestedCoordinate pi → T4) :

ℂ

Pull an arbitrary density on two completed half carriers to the literal initial nested-cross carrier.

Equations

terminal.initialNestedPullback pi density v = density ((terminal.terminalProductPiMeasurableEquivNested pi).symm v)

Instances For

source

@[simp]

theorem Anderson4D.R324TwoHalfTerminalData.initialNestedPullback_reindex {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam eps kappaP kappaM) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (density : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4) → ℂ) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) :

terminal.initialNestedPullback pi density ((terminal.terminalProductPiMeasurableEquivNested pi) p) = density p

source

theorem Anderson4D.R324TwoHalfTerminalData.integral_terminalProduct_eq_integral_initialNestedPullback {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam eps kappaP kappaM) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (density : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4) → ℂ) :

∫ (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)), density p ∂(MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure) = ∫ (v : terminal.NestedCoordinate pi → T4), terminal.initialNestedPullback pi density v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure

The product-terminal and initial nested integrals of an arbitrary density agree exactly.

source

(fun (v : terminal.NestedCoordinate pi → T4) => ‖terminal.initialNestedPullback pi density v‖) ≤ᵐ[MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure] fun (v : terminal.NestedCoordinate pi → T4) => majorant ((terminal.terminalProductPiMeasurableEquivNested pi).symm v)

Pull an a.e. terminal-product bound to the initial nested carrier.

source

theorem Anderson4D.R324TwoHalfTerminalData.ae_coupling_mul_norm_endpointDensity_le_completeNestedRun_of_grouped {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam eps kappaP kappaM) (leftScale rightScale : Fin (m + 1) → ℝ) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (head : R324NestedCrossBlock kappaP kappaM pi) (tail : List (R324NestedCrossBlock kappaP kappaM pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remaining = head :: tail) (endpointWeight : ℝ) (endpointDensity : (terminal.NestedCoordinate pi → T4) → ℂ) (hendpoint : (fun (v : terminal.NestedCoordinate pi → T4) => ‖endpointDensity v‖) ≤ᵐ[MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure] fun (v : terminal.NestedCoordinate pi → T4) => endpointWeight * terminal.initialNestedEndpointIntegratedGroupedMajorant leftScale rightScale hleft hright pi v) :

let step := r324InitialNestedCrossStepContext kappaP kappaM pi head tail hremaining; have hleftInitial := ⋯; have hrightInitial := ⋯; (fun (v : terminal.NestedCoordinate pi → T4) => lamEps lam eps ^ (2 * step.residual.remainingOrder) * ‖endpointDensity v‖) ≤ᵐ[MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure] fun (v : terminal.NestedCoordinate pi → T4) => endpointWeight * (((∏ edge ∈ terminal.left.activeEdgeSlots, leftScale edge) * ∏ edge ∈ terminal.right.activeEdgeSlots, rightScale edge) * invSqKerMass ^ 4 * terminal.completeNestedRunDensity step hleftInitial hrightInitial v)

Common Step 3 consumer for a completed signed endpoint branch. The branch-specific proof is required only to dominate its post-endpoint density by the literal grouped majorant. The coupling power is inserted after that domination and then converted exactly to the complete nested run.

source

theorem Anderson4D.R324TwoHalfTerminalData.integral_coupling_mul_norm_endpointDensity_le_completeNestedRun_of_grouped {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam eps kappaP kappaM) (leftScale rightScale : Fin (m + 1) → ℝ) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (head : R324NestedCrossBlock kappaP kappaM pi) (tail : List (R324NestedCrossBlock kappaP kappaM pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remaining = head :: tail) (endpointWeight : ℝ) (endpointDensity : (terminal.NestedCoordinate pi → T4) → ℂ) (hendpoint : (fun (v : terminal.NestedCoordinate pi → T4) => ‖endpointDensity v‖) ≤ᵐ[MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure] fun (v : terminal.NestedCoordinate pi → T4) => endpointWeight * terminal.initialNestedEndpointIntegratedGroupedMajorant leftScale rightScale hleft hright pi v) (hlam : 0 < lam) (heps : 0 < eps) (heps1 : eps ≤ 1) (hlog : 1 ≤ |Real.log eps|) (hmtrunc : m ≤ truncOrder eps) :

let step := r324InitialNestedCrossStepContext kappaP kappaM pi head tail hremaining; have hleftInitial := ⋯; have hrightInitial := ⋯; (∫ (v : terminal.NestedCoordinate pi → T4), lamEps lam eps ^ (2 * step.residual.remainingOrder) * ‖endpointDensity v‖ ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure) ≤ endpointWeight * (((∏ edge ∈ terminal.left.activeEdgeSlots, leftScale edge) * ∏ edge ∈ terminal.right.activeEdgeSlots, rightScale edge) * invSqKerMass ^ 4 * ∫ (v : step.SurvivingCoordinate → T4), terminal.completeNestedRunDensity step hleftInitial hrightInitial v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure)

Integrated form of the common signed-endpoint consumer. It keeps the literal endpoint weight outside the complete-run integral.

source

theorem Anderson4D.R324TwoHalfTerminalData.integral_coupling_mul_norm_endpointDensity_le_ambientMajorant_of_grouped {rho : SmoothCutoff} {C K A B lam eps supportConstant : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (hA : 0 ≤ A) (hC : 0 ≤ C) (hK : 0 ≤ K) (hB : 0 ≤ B) (hlam : 0 < lam) (terminal : R324TwoHalfTerminalData rho lam eps kappaP kappaM) (leftScale rightScale : Fin (m + 1) → ℝ) (leftReachable : R324WithinHalfBudgetScaleReachable kappaP rho C lam eps K A terminal.left.state leftScale) (rightReachable : R324WithinHalfBudgetScaleReachable kappaM rho C lam eps K A terminal.right.state rightScale) (leftCertificate : R324WithinHalfEdgeCertificate terminal.left.state leftScale) (rightCertificate : R324WithinHalfEdgeCertificate terminal.right.state rightScale) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (head : R324NestedCrossBlock kappaP kappaM pi) (tail : List (R324NestedCrossBlock kappaP kappaM pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remaining = head :: tail) (endpointWeight : ℝ) (hendpointWeight : 0 ≤ endpointWeight) (endpointDensity : (terminal.NestedCoordinate pi → T4) → ℂ) (hendpoint : (fun (v : terminal.NestedCoordinate pi → T4) => ‖endpointDensity v‖) ≤ᵐ[MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure] fun (v : terminal.NestedCoordinate pi → T4) => endpointWeight * terminal.initialNestedEndpointIntegratedGroupedMajorant leftScale rightScale hleft hright pi v) (heps : 0 < eps) (heps1 : eps ≤ 1) (hlog : 1 ≤ |Real.log eps|) (hm : 1 ≤ m) (hmtrunc : m ≤ truncOrder eps) (hrunBound : let step := r324InitialNestedCrossStepContext kappaP kappaM pi head tail hremaining; have hleftInitial := ⋯; have hrightInitial := ⋯; (∫ (v : step.SurvivingCoordinate → T4), terminal.completeNestedRunDensity step hleftInitial hrightInitial v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure) ≤ ∫ (z : T4), primitiveInsertedMajorant B lam eps supportConstant step.residual.remainingOrder z ∂paperMeasure) :

have step := r324InitialNestedCrossStepContext kappaP kappaM pi head tail hremaining; (∫ (v : terminal.NestedCoordinate pi → T4), lamEps lam eps ^ (2 * step.residual.remainingOrder) * ‖endpointDensity v‖ ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure) ≤ endpointWeight * ∫ (z : T4), primitiveInsertedMajorant (r324TwoHalfCompleteAbsorbedBase A C K B) lam eps supportConstant m z ∂paperMeasure

End-to-end numerical consumer for any signed endpoint pattern. The pattern-specific work stops at hendpoint; the existing complete-run estimate and the exact reachable-scale recurrence then place the result in one ambient-order primitive-majorant currency.

source

noncomputable def Anderson4D.r324FourDirectRunInflatedBase (B : ℝ) :

ℝ

Inflate the complete-run primitive constant just enough to replace the four artificial inverse-square endpoint masses by the four exact Fourier integrations of the direct/direct branch.

Equations

Anderson4D.r324FourDirectRunInflatedBase B = max 1 (Anderson4D.invSqKerMass ⁻¹ ^ 2) * B

Instances For

source

theorem Anderson4D.r324FourDirectRunInflatedBase_nonneg {B : ℝ} (hB : 0 ≤ B) :

0 ≤ r324FourDirectRunInflatedBase B

source

theorem Anderson4D.r324FourDirectRunInflatedBase_pos {B : ℝ} (hB : 0 < B) :

0 < r324FourDirectRunInflatedBase B

source

theorem Anderson4D.primitiveInsertedMajorant_le_invSqKerMass_pow_four_mul_fourDirectInflated (B lam eps supportConstant : ℝ) {n : ℕ} (hn : 1 ≤ n) (z : T4) :

primitiveInsertedMajorant B lam eps supportConstant n z ≤ invSqKerMass ^ 4 * primitiveInsertedMajorant (r324FourDirectRunInflatedBase B) lam eps supportConstant n z

The single fixed inflation above compensates the missing four endpoint masses at every nonempty nested-cross order.

source

theorem Anderson4D.r324_twoHalf_initial_fourDirectScale_mul_majorant_le {rho : SmoothCutoff} {C K A B lam eps supportConstant : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (hA : 1 ≤ A) (hC : 0 ≤ C) (hK : 0 ≤ K) (hB : 0 ≤ B) (hlam : 0 ≤ lam) (leftData : (R324WithinHalfResidualPrefix.initial rho lam eps kappaP).R324CompatibleAnalyticBudgetTrace fun (x : Fin (m + 1)) => A) (rightData : (R324WithinHalfResidualPrefix.initial rho lam eps kappaM).R324CompatibleAnalyticBudgetTrace fun (x : Fin (m + 1)) => A) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hm : 1 ≤ m) (hleftOutgoing : Fin.last m ∉ extractedRightEdges kappaP) (hleftIncoming : ⟨0, ⋯⟩ ∈ finalActive kappaP) (hrightOutgoing : Fin.last m ∉ extractedRightEdges kappaM) (hrightIncoming : ⟨0, ⋯⟩ ∈ finalActive kappaM) (head : R324NestedCrossBlock kappaP kappaM pi) (tail : List (R324NestedCrossBlock kappaP kappaM pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remaining = head :: tail) (z : T4) :

have terminal := R324TwoHalfTerminalData.ofCertifiedTraces leftData.analytic rightData.analytic; have hleft := ⋯; have hright := ⋯; terminal.left.endpointErasedScaleProduct hleft leftData.analytic.terminalScale * terminal.right.endpointErasedScaleProduct hright rightData.analytic.terminalScale * primitiveInsertedMajorant B lam eps supportConstant (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remainingOrder z ≤ primitiveInsertedMajorant (r324TwoHalfCompleteAbsorbedBase A C K (r324FourDirectRunInflatedBase B)) lam eps supportConstant m z

Pointwise two-half scale absorption for the four-direct branch. This is the direct/direct analogue of r324_twoHalf_initial_terminalScale_mul_majorant_le, with the endpoint slots already Fourier-integrated and therefore absent from the analytic scale product.

source

theorem Anderson4D.r324_twoHalf_initial_fourDirectScale_mul_integral_majorant_le {rho : SmoothCutoff} {C K A B lam eps supportConstant : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (hA : 1 ≤ A) (hC : 0 ≤ C) (hK : 0 ≤ K) (hB : 0 ≤ B) (hlam : 0 ≤ lam) (heps : 0 < eps) (leftData : (R324WithinHalfResidualPrefix.initial rho lam eps kappaP).R324CompatibleAnalyticBudgetTrace fun (x : Fin (m + 1)) => A) (rightData : (R324WithinHalfResidualPrefix.initial rho lam eps kappaM).R324CompatibleAnalyticBudgetTrace fun (x : Fin (m + 1)) => A) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hm : 1 ≤ m) (hleftOutgoing : Fin.last m ∉ extractedRightEdges kappaP) (hleftIncoming : ⟨0, ⋯⟩ ∈ finalActive kappaP) (hrightOutgoing : Fin.last m ∉ extractedRightEdges kappaM) (hrightIncoming : ⟨0, ⋯⟩ ∈ finalActive kappaM) (head : R324NestedCrossBlock kappaP kappaM pi) (tail : List (R324NestedCrossBlock kappaP kappaM pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remaining = head :: tail) :

have terminal := R324TwoHalfTerminalData.ofCertifiedTraces leftData.analytic rightData.analytic; have hleft := ⋯; have hright := ⋯; terminal.left.endpointErasedScaleProduct hleft leftData.analytic.terminalScale * terminal.right.endpointErasedScaleProduct hright rightData.analytic.terminalScale * ∫ (z : T4), primitiveInsertedMajorant B lam eps supportConstant (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remainingOrder z ∂paperMeasure ≤ ∫ (z : T4), primitiveInsertedMajorant (r324TwoHalfCompleteAbsorbedBase A C K (r324FourDirectRunInflatedBase B)) lam eps supportConstant m z ∂paperMeasure

Integrated form of the four-direct two-half scale absorption.

source

theorem Anderson4D.R324TwoHalfTerminalData.integral_coupling_mul_norm_initialNestedEndpointIntegratedResidualDensity_le_fourDirectAmbientMajorant {rho : SmoothCutoff} {C K A B lam eps supportConstant : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (hA : 1 ≤ A) (hC : 0 ≤ C) (hK : 0 ≤ K) (hB : 0 ≤ B) (hlam : 0 < lam) (heps : 0 < eps) (heps1 : eps ≤ 1) (hlog : 1 ≤ |Real.log eps|) (hm : 1 ≤ m) (hmtrunc : m ≤ truncOrder eps) (leftData : (R324WithinHalfResidualPrefix.initial rho lam eps kappaP).R324CompatibleAnalyticBudgetTrace fun (x : Fin (m + 1)) => A) (rightData : (R324WithinHalfResidualPrefix.initial rho lam eps kappaM).R324CompatibleAnalyticBudgetTrace fun (x : Fin (m + 1)) => A) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hleftOutgoing : Fin.last m ∉ extractedRightEdges kappaP) (hleftIncoming : ⟨0, ⋯⟩ ∈ finalActive kappaP) (hrightOutgoing : Fin.last m ∉ extractedRightEdges kappaM) (hrightIncoming : ⟨0, ⋯⟩ ∈ finalActive kappaM) (head : R324NestedCrossBlock kappaP kappaM pi) (tail : List (R324NestedCrossBlock kappaP kappaM pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remaining = head :: tail) (alpha beta : Z4) (hrunBound : have terminal := ofCertifiedTraces leftData.analytic rightData.analytic; have step := r324InitialNestedCrossStepContext kappaP kappaM pi head tail hremaining; have hleftInitial := ⋯; have hrightInitial := ⋯; (∫ (v : step.SurvivingCoordinate → T4), terminal.completeNestedRunDensity step hleftInitial hrightInitial v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure) ≤ ∫ (z : T4), primitiveInsertedMajorant B lam eps supportConstant step.residual.remainingOrder z ∂paperMeasure) :

have terminal := ofCertifiedTraces leftData.analytic rightData.analytic; have hleft := ⋯; have hright := ⋯; have step := r324InitialNestedCrossStepContext kappaP kappaM pi head tail hremaining; (∫ (v : terminal.NestedCoordinate pi → T4), lamEps lam eps ^ (2 * step.residual.remainingOrder) * ‖terminal.initialNestedEndpointIntegratedResidualDensity pi hleft hright alpha beta v‖ ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure) ≤ paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * ∫ (z : T4), primitiveInsertedMajorant (r324TwoHalfCompleteAbsorbedBase A C K (r324FourDirectRunInflatedBase B)) lam eps supportConstant m z ∂paperMeasure

Direct/direct residual branch in ambient-order inserted-majorant currency, for fixed compatible traces and a supplied complete-run bound.

source

theorem Anderson4D.exists_r324PaperFourDirectEndpointWeightedMajorantBound (rho : SmoothCutoff) :

∃ (primitiveConstant : ℝ) (supportConstant : ℝ), 0 < primitiveConstant ∧ 0 < supportConstant ∧ ∀ {eps : ℝ} (m : ℕ) (alpha beta : Z4), 0 < eps → eps ≤ 1 / 4 → 1 ≤ |Real.log eps| → 2 ≤ m → m ≤ truncOrder eps → ∀ (p : R324RefinedScheduleIndex m) (hm0 : 0 < m), (r324RefinedContractionRepresentative m ↑p.fst ↑p.snd).fst.singles.Nonempty → ⟨0, hm0⟩ ∈ finalActive (r324RefinedContractionRepresentative m ↑p.fst ↑p.snd).fst → Fin.last m ∉ extractedRightEdges (r324RefinedContractionRepresentative m ↑p.fst ↑p.snd).fst → ⟨0, hm0⟩ ∈ finalActive (r324RefinedContractionRepresentative m ↑p.fst ↑p.snd).snd.fst → Fin.last m ∉ extractedRightEdges (r324RefinedContractionRepresentative m ↑p.fst ↑p.snd).snd.fst → |lamEps 1 eps| ^ (2 * m) * ‖r324RefinedPhysicalIntegral rho eps m alpha beta p‖ ≤ paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant 1 eps supportConstant m z ∂paperMeasure

Uniform producer for the all-four-direct residual endpoint pattern. The constants are chosen before the scale, order, refined schedule, and Fourier modes.

Endpoint classification on the actual refined-fibre representative #

source

noncomputable def Anderson4D.r324ActualRefinedEndpointReductionCase {m : ℕ} (p : R324RefinedScheduleIndex m) :

Fin 4 → SmoothCutoff.R324EndpointReductionCase

The four endpoint cases attached to the representative which actually appears in the signed physical-collapse theorem. This deliberately does not use r324RefinedScheduleRepresentative, whose choice is only made in the coarser contraction fibre.

Equations

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

Instances For

source

theorem Anderson4D.r324ActualRefinedEndpointReductionCase_eq_refined {m : ℕ} (p : R324RefinedScheduleIndex m) :

r324ActualRefinedEndpointReductionCase p = SmoothCutoff.r324RefinedEndpointReductionCase p

The endpoint pattern is independent of which representative of the fixed within-half signature is used. In particular, the representative chosen in the residual-refined fibre has the same four paper endpoint cases as the representative chosen in the coarser contraction fibre.

The proof uses the rigidity of the actual extraction recursion under a fixed endpoint signature; it does not assume invariance of the refined representative as extra data.

source

theorem Anderson4D.r324RefinedContractionRepresentative_singles_nonempty {m : ℕ} (p : R324RefinedScheduleIndex m) (hsingles : (r324RefinedScheduleRepresentative p).fst.singles.Nonempty) :

(r324RefinedContractionRepresentative m ↑p.fst ↑p.snd).fst.singles.Nonempty

A residual single in the coarse schedule representative is therefore also present in the refined-fibre representative used by the exact signed physical collapse.

source

theorem Anderson4D.r324ActualRefinedEndpointReductionCase_direct_iff {m : ℕ} (hm : 0 < m) (p : R324RefinedScheduleIndex m) :

(r324ActualRefinedEndpointReductionCase p 0 = SmoothCutoff.R324EndpointReductionCase.directFourier ↔ ⟨0, hm⟩ ∈ finalActive (r324RefinedContractionRepresentative m ↑p.fst ↑p.snd).fst) ∧ (r324ActualRefinedEndpointReductionCase p 1 = SmoothCutoff.R324EndpointReductionCase.directFourier ↔ Fin.last m ∉ extractedRightEdges (r324RefinedContractionRepresentative m ↑p.fst ↑p.snd).fst) ∧ (r324ActualRefinedEndpointReductionCase p 2 = SmoothCutoff.R324EndpointReductionCase.directFourier ↔ ⟨0, hm⟩ ∈ finalActive (r324RefinedContractionRepresentative m ↑p.fst ↑p.snd).snd.fst) ∧ (r324ActualRefinedEndpointReductionCase p 3 = SmoothCutoff.R324EndpointReductionCase.directFourier ↔ Fin.last m ∉ extractedRightEdges (r324RefinedContractionRepresentative m ↑p.fst ↑p.snd).snd.fst)

Definitional four-bit classification for the actual refined representative.

source

theorem Anderson4D.r324ActualRefinedEndpointReductionCase_cases {m : ℕ} (p : R324RefinedScheduleIndex m) (j : Fin 4) :

r324ActualRefinedEndpointReductionCase p j = SmoothCutoff.R324EndpointReductionCase.directFourier ∨ r324ActualRefinedEndpointReductionCase p j = SmoothCutoff.R324EndpointReductionCase.insertedSacrifice

The exact two-half endpoint ledger #

source

def Anderson4D.r324LeftHalfEndpointCases (cases : Fin 4 → SmoothCutoff.R324EndpointReductionCase) :

R324PaperHalfEndpointCases

The two endpoint cases belonging to the left half, in the paper order incoming then outgoing.

Equations

Anderson4D.r324LeftHalfEndpointCases cases = ![cases 0, cases 1]

Instances For

source

def Anderson4D.r324RightHalfEndpointCases (cases : Fin 4 → SmoothCutoff.R324EndpointReductionCase) :

R324PaperHalfEndpointCases

The two endpoint cases belonging to the right half, in the paper order incoming then outgoing.

Equations

Anderson4D.r324RightHalfEndpointCases cases = ![cases 2, cases 3]

Instances For

source

theorem Anderson4D.r324PaperHalfEndpointSacrifice_mul_eq_product (eps : ℝ) (cases : Fin 4 → SmoothCutoff.R324EndpointReductionCase) :

r324PaperHalfEndpointSacrifice eps (r324LeftHalfEndpointCases cases) * r324PaperHalfEndpointSacrifice eps (r324RightHalfEndpointCases cases) = SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps cases

Multiplying the two genuine half-chain endpoint costs gives exactly the four-endpoint cost of Step 4(A). In particular no uniform epsilon^{-2} is inserted at a direct endpoint while the two halves are spliced.

source

def Anderson4D.R324PaperResidualEndpointPatternWeightedMajorantBound (rho : SmoothCutoff) (primitiveConstant supportConstant : ℝ) :

Prop

The paper-faithful residual endpoint interface before the last uniform epsilon^{-8} enlargement. The physical producer records the four cases of the representative which actually occurs in the signed collapse; a direct endpoint therefore still has cost exactly one here.

Equations

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

Instances For

source

theorem Anderson4D.R324PaperResidualEndpointPatternWeightedMajorantBound.to_uniform {rho : SmoothCutoff} {primitiveConstant supportConstant : ℝ} (h : R324PaperResidualEndpointPatternWeightedMajorantBound rho primitiveConstant supportConstant) :

R324PaperResidualEndpointWeightedMajorantBound rho primitiveConstant supportConstant

Only after the four signed endpoint operations have been assembled do we replace their literal case product by the paper's uniform epsilon^{-8} budget.

source

theorem Anderson4D.exists_r324PaperResidualFourDirectBranchWeightedMajorantBound (rho : SmoothCutoff) :

∃ (primitiveConstant : ℝ) (supportConstant : ℝ), 0 < primitiveConstant ∧ 0 < supportConstant ∧ ∀ {eps : ℝ} (m : ℕ) (alpha beta : Z4), 0 < eps → eps ≤ 1 / 4 → 1 ≤ |Real.log eps| → 2 ≤ m → m ≤ truncOrder eps → ∀ (p : R324RefinedScheduleIndex m), (r324RefinedScheduleRepresentative p).fst.singles.Nonempty → (SmoothCutoff.r324RefinedEndpointReductionCase p = fun (x : Fin 4) => SmoothCutoff.R324EndpointReductionCase.directFourier) → |lamEps 1 eps| ^ (2 * m) * ‖r324RefinedPhysicalIntegral rho eps m alpha beta p‖ ≤ paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * (eps⁻¹ ^ 8 * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant 1 eps supportConstant m z ∂paperMeasure)

Coarse-interface form of the genuine all-four-direct producer. The public residual branch is stated using the schedule representative, while the signed collapse uses the representative of the residual-refined fibre. Endpoint-signature rigidity supplies the bridge, and the stronger direct estimate is enlarged to the common paper epsilon^{-8} currency only at the final scalar step.

Documentation

Anderson4D.DetParametrix.Paper42_Moment.R324PaperEndpointTwoHalfSplice

Paper Step 4(A): structural two-half endpoint splice #

The one-endpoint ordinary-to-inserted integral bridge #

The retained outgoing terminal, jointly in its endpoint variables #

Exact root regrouping for a direct outgoing endpoint #

The paired-incoming/retained-outgoing endpoint coefficient #

The right-half cross-factor projection #

Pointwise splice of the two exceptional-incoming/direct-outgoing halves #

The actual refined-root endpoint cases #

The residual incoming/outgoing exceptional blocks are distinct #

Exact direct/direct splice of the two completed halves #

Actual refined root, with all four direct endpoints #

The four-direct core in complete-run currency #

Complete-budget terminal scales, independent of endpoint cases #

Endpoint classification on the actual refined-fibre representative #

The exact two-half endpoint ledger #