Documentation

@[reducible, inline]

abbrev Anderson4D.SmoothCutoff.R324RefinedEndpointNonzeroRawConfiguration (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) :

Raw refined indices retained only after their complete endpoint and internal physical integral has been evaluated and found nonzero.

Equations

ρ.R324RefinedEndpointNonzeroRawConfiguration hm ε α β p = { a : ℕ // ρ.r324RefinedRawFullPairingIntegral hm ε α β p a ≠ 0 }

Instances For

@[reducible, inline]

abbrev Anderson4D.SmoothCutoff.R324NonzeroRouteLabel (m : ℕ) :

The data that must remain common on a corrected physical fibre: the actual contraction, the complete increment key, and the underlying genuine cross slot selected by the first-large selector. Retaining the contraction prevents equal Fin m positions belonging to different cross edges from being merged.

Equations

Anderson4D.SmoothCutoff.R324NonzeroRouteLabel m = (Anderson4D.MomentContraction m × (Fin m → Anderson4D.Z4) × Fin m)

Instances For

noncomputable def Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteLabel (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (a : ρ.R324RefinedEndpointNonzeroRawConfiguration hm ε α β p) :

R324NonzeroRouteLabel m

Route label of one endpoint-nonzero raw configuration. The second component is the underlying Fin m position of the actual residual slot; its proof of membership in the contraction's singles set remains available in r324RefinedRawSelectedResidualSlot.

Equations

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

Instances For

@[reducible, inline]

abbrev Anderson4D.SmoothCutoff.R324RefinedEndpointNonzeroRouteFiber (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

Genuine fibre of endpoint-nonzero configurations having one fixed complete increment key and one fixed canonical selector slot.

Equations

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

Instances For

theorem Anderson4D.SmoothCutoff.r324RefinedRawFourierIntegral_eq_rawFullPairingIntegral (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (a : ℕ) :

ρ.r324RefinedRawFourierIntegral hm ε α β p a = ρ.r324RefinedRawFullPairingIntegral hm ε α β p a

The integrated raw Fourier term is definitionally represented by the full-pairing coefficient used for zero deletion.

theorem Anderson4D.SmoothCutoff.summable_r324RefinedRawFullPairingIntegral (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (p : R324RefinedScheduleIndex m) :

Summable (ρ.r324RefinedRawFullPairingIntegral hm ε α β p)

Full endpoint coefficients in one refined schedule are summable.

theorem Anderson4D.SmoothCutoff.tsum_r324RefinedRawFullPairingIntegral_eq_nonzero (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (p : R324RefinedScheduleIndex m) :

∑' (a : ℕ), ρ.r324RefinedRawFullPairingIntegral hm ε α β p a = ∑' (a : ρ.R324RefinedEndpointNonzeroRawConfiguration hm ε α β p), ρ.r324RefinedRawFullPairingIntegral hm ε α β p ↑a

Exact zero deletion at the correct boundary: only coefficients whose complete physical integral is zero are removed.

Exact contraction/key/selector partition before norms #

theorem Anderson4D.SmoothCutoff.tsum_r324RefinedEndpointNonzero_eq_routeFibres (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) :

∑' (a : ρ.R324RefinedEndpointNonzeroRawConfiguration hm ε α β p), ρ.r324RefinedRawFullPairingIntegral hm ε α β p ↑a = ∑' (route : R324NonzeroRouteLabel m) (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route), ρ.r324RefinedRawFullPairingIntegral hm ε α β p ↑↑a

After zero deletion, the remaining signed coefficient series partitions exactly by contraction, complete increment key, and actual selector slot.

Exact selector-restricted physical fibres #

noncomputable def Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRoutePhysicalTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) (q : R324PhysicalPoint m) :

One genuine selector-restricted physical term on a corrected route fibre.

Equations

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

Instances For

noncomputable def Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRoutePhysicalCore (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (q : R324PhysicalPoint m) :

Signed physical sum of exactly one nonzero contraction/key/selector fibre. No unrestricted projected covariance has been substituted.

Equations

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

Instances For

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteFiber_contraction (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) :

r324RefinedRawMomentContraction p ↑↑a = route.1

Membership in a corrected route fibre exposes the actual contraction whose dependent selector fibre is being used.

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteFiber_key (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) :

r324RefinedRawIncrementKey hm p ↑↑a = route.2.1

Membership in a corrected route fibre exposes the promised complete increment key.

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteFiber_selector (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) :

↑(ρ.r324RefinedRawSelectedResidualSlot hm ε α β hexternal hε hε1 hmtrunc p ↑↑a ⋯) = route.2.2

Membership also exposes the underlying genuine selector slot. The stronger proof that this position belongs to the actual residual singles set remains part of r324RefinedRawSelectedResidualSlot.

theorem Anderson4D.SmoothCutoff.sum_r324RefinedEndpointNonzeroRouteKey_eq_external (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) :

∑ i : Fin m, z4EuclideanFrequency (route.2.1 i) = z4EuclideanFrequency (α + β)

Every inhabited corrected route key carries the exact external frequency. This is the later central-frequency routing input and follows from endpoint nonvanishing, not from a dummy zero-term route.

Internal signed cores after endpoint-licensed zero deletion #

noncomputable def Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteInternalTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) (v : Fin (2 * m) → T4) :

One selector-restricted signed internal term in a corrected route fibre.

Equations

ρ.r324RefinedEndpointNonzeroRouteInternalTerm hm ε α β hexternal hε hε1 hmtrunc p route a v = ρ.r324RefinedRawSelectorRestrictedSignedCore hm ε α β hexternal hε hε1 hmtrunc p ↑↑a ⋯ v

Instances For

noncomputable def Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteInternalCore (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (v : Fin (2 * m) → T4) :

The signed internal core of a fixed (contraction, key, selector) fibre. The zero-deletion predicate in the index type was established only after complete endpoint integration; the norm has still not been taken.

Equations

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

Instances For

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteInternalTerm_eq_actual (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) (v : Fin (2 * m) → T4) :

ρ.r324RefinedEndpointNonzeroRouteInternalTerm hm ε α β hexternal hε hε1 hmtrunc p route a v = ((r324RenormalizedInteriorCore (r324RefinedRawMomentContraction p ↑↑a).fst fun (i : Fin m) => v (leftMomentIndex i)) * r324RenormalizedInteriorCore (r324RefinedRawMomentContraction p ↑↑a).snd.fst fun (i : Fin m) => v (rightMomentIndex i)) * ρ.r324RefinedRawCovarianceConfiguration hm ε p (↑↑a) v

On an endpoint-nonzero member, exposing the selected high mode gives the actual contraction's two internal Green cores times the original raw covariance configuration. The contraction is not replaced by a schedule representative at this boundary.

noncomputable def Anderson4D.SmoothCutoff.r324NonzeroRouteInteriorSkeletonL1 {m : ℕ} (route : R324NonzeroRouteLabel m) :

Internal L¹ skeleton mass attached to the actual contraction in a corrected route.

Equations

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

Instances For

theorem Anderson4D.SmoothCutoff.r324NonzeroRouteInteriorSkeletonL1_nonneg {m : ℕ} (route : R324NonzeroRouteLabel m) :

0 ≤ r324NonzeroRouteInteriorSkeletonL1 route

noncomputable def Anderson4D.SmoothCutoff.r324AllContractionInteriorSkeletonL1 (m : ℕ) :

A finite uniform envelope for the internal skeleton masses of every possible contraction.

Equations

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

Instances For

theorem Anderson4D.SmoothCutoff.r324AllContractionInteriorSkeletonL1_nonneg (m : ℕ) :

0 ≤ r324AllContractionInteriorSkeletonL1 m

theorem Anderson4D.SmoothCutoff.r324NonzeroRouteInteriorSkeletonL1_le_all {m : ℕ} (route : R324NonzeroRouteLabel m) :

r324NonzeroRouteInteriorSkeletonL1 route ≤ r324AllContractionInteriorSkeletonL1 m

theorem Anderson4D.SmoothCutoff.norm_r324RefinedEndpointNonzeroRouteInternalTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) (v : Fin (2 * m) → T4) :

‖ρ.r324RefinedEndpointNonzeroRouteInternalTerm hm ε α β hexternal hε hε1 hmtrunc p route a v‖ = r324SelectedInteriorSkeletonNormDensity route.1.fst route.1.snd.fst v * ρ.r324RefinedRawCovarianceWeight hm ε p ↑↑a

Exact coordinate-independent norm ledger for one corrected internal term.

theorem Anderson4D.SmoothCutoff.summable_r324RefinedEndpointNonzeroRouteInternalTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (v : Fin (2 * m) → T4) :

Summable fun (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) => ρ.r324RefinedEndpointNonzeroRouteInternalTerm hm ε α β hexternal hε hε1 hmtrunc p route a v

Internal terms in a corrected route fibre are summable pointwise.

theorem Anderson4D.SmoothCutoff.integral_norm_r324RefinedEndpointNonzeroRouteInternalTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) :

(∫ (v : Fin (2 * m) → T4), ‖ρ.r324RefinedEndpointNonzeroRouteInternalTerm hm ε α β hexternal hε hε1 hmtrunc p route a v‖ ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) = r324NonzeroRouteInteriorSkeletonL1 route * ρ.r324RefinedRawCovarianceWeight hm ε p ↑↑a

Integral norm of one corrected internal term.

theorem Anderson4D.SmoothCutoff.summable_integral_norm_r324RefinedEndpointNonzeroRouteInternalTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

Summable fun (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) => ∫ (v : Fin (2 * m) → T4), ‖ρ.r324RefinedEndpointNonzeroRouteInternalTerm hm ε α β hexternal hε hε1 hmtrunc p route a v‖ ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

The internal integral-norm ledger is summable on each corrected route fibre.

theorem Anderson4D.SmoothCutoff.integrable_norm_r324RefinedEndpointNonzeroRouteInternalTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) :

MeasureTheory.Integrable (fun (v : Fin (2 * m) → T4) => ‖ρ.r324RefinedEndpointNonzeroRouteInternalTerm hm ε α β hexternal hε hε1 hmtrunc p route a v‖) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)

Each corrected internal term has integrable norm.

theorem Anderson4D.SmoothCutoff.integrable_r324RefinedEndpointNonzeroRouteInternalTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) :

MeasureTheory.Integrable (ρ.r324RefinedEndpointNonzeroRouteInternalTerm hm ε α β hexternal hε hε1 hmtrunc p route a) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)

Each corrected internal term itself is integrable.

theorem Anderson4D.SmoothCutoff.integrable_r324RefinedEndpointNonzeroRouteInternalCore (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

MeasureTheory.Integrable (ρ.r324RefinedEndpointNonzeroRouteInternalCore hm ε α β hexternal hε hε1 hmtrunc p route) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)

The complete signed internal route core is integrable.

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRoutePhysicalTerm_eq_raw (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) (q : R324PhysicalPoint m) :

ρ.r324RefinedEndpointNonzeroRoutePhysicalTerm hm ε α β hexternal hε hε1 hmtrunc p route a q = r324Flatten (ρ.r324RefinedRawEndpointIntegrand hm ε α β p ↑↑a) q

The routed physical term is exactly the original raw endpoint integrand; only its already-proved selector-restricted factorization has been exposed.

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRoutePhysicalTerm_eq_endpointSeparated (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) (x y z w : T4) (v : Fin (2 * m) → T4) :

ρ.r324RefinedEndpointNonzeroRoutePhysicalTerm hm ε α β hexternal hε hε1 hmtrunc p route a (x, y, z, w, v) = r324EndpointSeparatedIntegrand α β (r324ContractionEndpointAnchors hm route.1 v) (r324ContractionEndpointFlags route.1) (ρ.r324RefinedEndpointNonzeroRouteInternalTerm hm ε α β hexternal hε hε1 hmtrunc p route a v) x y z w

Because the route label retains the actual contraction, every member of the fibre has the same endpoint anchors and flags.

noncomputable def Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteEndpointIntegrand (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (x y z w : T4) (v : Fin (2 * m) → T4) :

Curried endpoint-separated integrand of a complete corrected route fibre.

Equations

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

Instances For

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRoutePhysicalCore_eq_endpointIntegrand (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (q : R324PhysicalPoint m) :

ρ.r324RefinedEndpointNonzeroRoutePhysicalCore hm ε α β hexternal hε hε1 hmtrunc p route q = r324Flatten (ρ.r324RefinedEndpointNonzeroRouteEndpointIntegrand hm ε α β hexternal hε hε1 hmtrunc p route) q

The full routed physical core is pointwise exactly the endpoint-separated integrand of the internal signed route core.

theorem Anderson4D.SmoothCutoff.integrable_r324RefinedEndpointNonzeroRoutePhysicalTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) :

MeasureTheory.Integrable (ρ.r324RefinedEndpointNonzeroRoutePhysicalTerm hm ε α β hexternal hε hε1 hmtrunc p route a) (r324PhysicalMeasure m)

Each member of a corrected route fibre is integrable on the full five-group physical space.

theorem Anderson4D.SmoothCutoff.summable_integral_norm_r324RefinedEndpointNonzeroRoutePhysicalTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

Summable fun (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route) => ∫ (q : R324PhysicalPoint m), ‖ρ.r324RefinedEndpointNonzeroRoutePhysicalTerm hm ε α β hexternal hε hε1 hmtrunc p route a q‖ ∂r324PhysicalMeasure m

The integral norms in every corrected route fibre are summable.

theorem Anderson4D.SmoothCutoff.integrable_r324RefinedEndpointNonzeroRoutePhysicalCore (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

MeasureTheory.Integrable (ρ.r324RefinedEndpointNonzeroRoutePhysicalCore hm ε α β hexternal hε hε1 hmtrunc p route) (r324PhysicalMeasure m)

Every signed corrected route core is integrable.

theorem Anderson4D.SmoothCutoff.integrable_r324Flatten_refinedEndpointNonzeroRouteEndpointIntegrand (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

MeasureTheory.Integrable (r324Flatten (ρ.r324RefinedEndpointNonzeroRouteEndpointIntegrand hm ε α β hexternal hε hε1 hmtrunc p route)) (r324PhysicalMeasure m)

The endpoint-separated representation of a corrected route is jointly integrable on the genuine five-group product.

theorem Anderson4D.SmoothCutoff.integral_r324RefinedEndpointNonzeroRoutePhysicalCore_eq_internalFirst (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

∫ (q : R324PhysicalPoint m), ρ.r324RefinedEndpointNonzeroRoutePhysicalCore hm ε α β hexternal hε hε1 hmtrunc p route q ∂r324PhysicalMeasure m = ∫ (v : Fin (2 * m) → T4), ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), ρ.r324RefinedEndpointNonzeroRouteEndpointIntegrand hm ε α β hexternal hε hε1 hmtrunc p route x y z w v ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

Exact internal-first representation of one corrected route coefficient.

theorem Anderson4D.SmoothCutoff.norm_integral_r324RefinedEndpointNonzeroRoutePhysicalCore_le_fourier (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

‖∫ (q : R324PhysicalPoint m), ρ.r324RefinedEndpointNonzeroRoutePhysicalCore hm ε α β hexternal hε hε1 hmtrunc p route q ∂r324PhysicalMeasure m‖ ≤ 16 * paperFourthOrderModeDecay α * paperFourthOrderModeDecay β * ∫ (v : Fin (2 * m) → T4), ‖ρ.r324RefinedEndpointNonzeroRouteInternalCore hm ε α β hexternal hε hε1 hmtrunc p route v‖ ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

Four endpoint integrations of a corrected route supply the two paper fourth-order Fourier decays before the internal norm density is introduced.

theorem Anderson4D.SmoothCutoff.integral_r324RefinedEndpointNonzeroRoutePhysicalCore (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

∫ (q : R324PhysicalPoint m), ρ.r324RefinedEndpointNonzeroRoutePhysicalCore hm ε α β hexternal hε hε1 hmtrunc p route q ∂r324PhysicalMeasure m = ∑' (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route), ρ.r324RefinedRawFullPairingIntegral hm ε α β p ↑↑a

Exact Fubini identity for one corrected route fibre.

Exact corrected expansion of the original moment #

theorem Anderson4D.SmoothCutoff.r324RefinedPhysicalIntegral_eq_nonzeroRoutePhysicalCore (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) :

r324RefinedPhysicalIntegral ρ ε m α β p = ∑' (route : R324NonzeroRouteLabel m), ∫ (q : R324PhysicalPoint m), ρ.r324RefinedEndpointNonzeroRoutePhysicalCore hm ε α β hexternal hε hε1 hmtrunc p route q ∂r324PhysicalMeasure m

One refined physical integral is exactly the sum of the integrated selector-restricted route cores. Zero deletion and all components of the route label occur before any norm.

theorem Anderson4D.SmoothCutoff.deterministicMomentPairingSum_eq_nonzeroRoutedPhysical (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) :

deterministicMomentPairingSum ρ lam ε m α β = ↑(lamEps lam ε) ^ (2 * m) * ∑ p : R324RefinedScheduleIndex m, ∑' (route : R324NonzeroRouteLabel m), ∫ (q : R324PhysicalPoint m), ρ.r324RefinedEndpointNonzeroRoutePhysicalCore hm ε α β hexternal hε hε1 hmtrunc p route q ∂r324PhysicalMeasure m

Paper-facing exact boundary for the complete deterministic moment: the common coupling remains outside the finite refined-schedule ledger, and every inner series is first zero-deleted and then route-partitioned.

Nonnegative density after exact routing #

noncomputable def Anderson4D.SmoothCutoff.r324NonzeroRouteSlotCost {m : ℕ} (route : R324NonzeroRouteLabel m) (i : Fin m) :

Reciprocal eighth-order cost attached directly to the key component of a corrected route label.

Equations

Anderson4D.SmoothCutoff.r324NonzeroRouteSlotCost route i = (1 + ‖Anderson4D.z4EuclideanFrequency (route.2.1 i)‖ ^ 2) ^ 4

Instances For

theorem Anderson4D.SmoothCutoff.r324NonzeroRouteSlotCost_pos {m : ℕ} (route : R324NonzeroRouteLabel m) (i : Fin m) :

0 < r324NonzeroRouteSlotCost route i

theorem Anderson4D.SmoothCutoff.one_le_r324NonzeroRouteSlotCost {m : ℕ} (route : R324NonzeroRouteLabel m) (i : Fin m) :

1 ≤ r324NonzeroRouteSlotCost route i

theorem Anderson4D.SmoothCutoff.r324NonzeroRouteSlotCost_mul_decay {m : ℕ} (route : R324NonzeroRouteLabel m) (i : Fin m) :

r324NonzeroRouteSlotCost route i * eighthOrderFrequencyDecay ‖z4EuclideanFrequency (route.2.1 i)‖ = 1

The route cost has the exact reciprocal-decay normalization of the natural-key cost, but it is attached directly to the retained route key.

theorem Anderson4D.SmoothCutoff.r324NonzeroRouteSlotCost_eq_groupedIncrementCost {m : ℕ} (hm : 0 < m) (route : R324NonzeroRouteLabel m) (b : ℕ) (hkey : route.2.1 = (r324NatEquivStandardConfigurations hm) b) (i : Fin m) :

r324NonzeroRouteSlotCost route i = r324GroupedIncrementCost hm b i

When a corrected key is named by the existing natural enumeration, its slot cost is literally the existing grouped cost.

noncomputable def Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteDensityBase (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (v : Fin (2 * m) → T4) :

Unweighted nonnegative internal mass of one corrected signed route fibre. Endpoint Fourier decay has already been extracted before this density is consumed.

Equations

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

Instances For

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteDensityBase_nonneg (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (v : Fin (2 * m) → T4) :

0 ≤ ρ.r324RefinedEndpointNonzeroRouteDensityBase lam hm ε α β hexternal hε hε1 hmtrunc p route v

theorem Anderson4D.SmoothCutoff.integrable_r324RefinedEndpointNonzeroRouteDensityBase (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

MeasureTheory.Integrable (ρ.r324RefinedEndpointNonzeroRouteDensityBase lam hm ε α β hexternal hε hε1 hmtrunc p route) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)

theorem Anderson4D.SmoothCutoff.norm_integral_r324RefinedEndpointNonzeroRoutePhysicalCore_le_base (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

|lamEps lam ε| ^ (2 * m) * ‖∫ (q : R324PhysicalPoint m), ρ.r324RefinedEndpointNonzeroRoutePhysicalCore hm ε α β hexternal hε hε1 hmtrunc p route q ∂r324PhysicalMeasure m‖ ≤ 16 * paperFourthOrderModeDecay α * paperFourthOrderModeDecay β * ∫ (v : Fin (2 * m) → T4), ρ.r324RefinedEndpointNonzeroRouteDensityBase lam hm ε α β hexternal hε hε1 hmtrunc p route v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

Direct analytic link from one exact signed route coefficient to its unweighted nonnegative internal density. The four endpoint integrations are performed before the norm is taken and contribute the two explicit fourth-order Fourier decays.

noncomputable def Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRoutedDensityTerm (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (i : Fin m) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (v : Fin (2 * m) → T4) :

One honest nonnegative routed density term. The norm is taken after all endpoint-nonzero configurations with a common (contraction, key, selector) label have been summed with their signs intact.

Equations

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

Instances For

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRoutedDensityTerm_nonneg (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (i : Fin m) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (v : Fin (2 * m) → T4) :

0 ≤ ρ.r324RefinedEndpointNonzeroRoutedDensityTerm lam hm ε α β hexternal hε hε1 hmtrunc i p route v

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteDensityBase_le_routed (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (i : Fin m) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) (v : Fin (2 * m) → T4) :

ρ.r324RefinedEndpointNonzeroRouteDensityBase lam hm ε α β hexternal hε hε1 hmtrunc p route v ≤ ρ.r324RefinedEndpointNonzeroRoutedDensityTerm lam hm ε α β hexternal hε hε1 hmtrunc i p route v

theorem Anderson4D.SmoothCutoff.integrable_r324RefinedEndpointNonzeroRoutedDensityTerm (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (i : Fin m) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

MeasureTheory.Integrable (ρ.r324RefinedEndpointNonzeroRoutedDensityTerm lam hm ε α β hexternal hε hε1 hmtrunc i p route) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)

Qualitative integrability of each corrected routed density term. Summability over all route labels is intentionally left to the later high-mode enlargement argument.

theorem Anderson4D.SmoothCutoff.integral_norm_r324RefinedEndpointNonzeroRouteInternalCore_le (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

(∫ (v : Fin (2 * m) → T4), ‖ρ.r324RefinedEndpointNonzeroRouteInternalCore hm ε α β hexternal hε hε1 hmtrunc p route v‖ ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) ≤ ∑' (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route), ∫ (v : Fin (2 * m) → T4), ‖ρ.r324RefinedEndpointNonzeroRouteInternalTerm hm ε α β hexternal hε hε1 hmtrunc p route a v‖ ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

Triangle inequality in internal L¹, still retaining the genuine signed route fibre on the left.

theorem Anderson4D.SmoothCutoff.integral_r324RefinedEndpointNonzeroRouteDensityBase_le_rawFiber (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

(∫ (v : Fin (2 * m) → T4), ρ.r324RefinedEndpointNonzeroRouteDensityBase lam hm ε α β hexternal hε hε1 hmtrunc p route v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) ≤ |lamEps lam ε| ^ (2 * m) * (r324NonzeroRouteInteriorSkeletonL1 route * ∑' (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route), ρ.r324RefinedRawCovarianceWeight hm ε p ↑↑a)

The unweighted internal route density is bounded by the exact raw covariance masses in that route fibre.

theorem Anderson4D.SmoothCutoff.sum_integral_r324RefinedEndpointNonzeroRoutedDensityTerm_le_rawFiber (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

(∑ i : Fin m, ∫ (v : Fin (2 * m) → T4), ρ.r324RefinedEndpointNonzeroRoutedDensityTerm lam hm ε α β hexternal hε hε1 hmtrunc i p route v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) ≤ |lamEps lam ε| ^ (2 * m) * (r324NonzeroRouteInteriorSkeletonL1 route * ∑' (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route), ρ.r324RefinedRawCovarianceRouteWeight hm ε p ↑↑a)

After summing all marked slots, one corrected route density is bounded by the raw degree-eight covariance route weights in precisely that route fibre.

theorem Anderson4D.SmoothCutoff.norm_integral_r324RefinedEndpointNonzeroRoutePhysicalCore_le_routed (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (i : Fin m) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

|lamEps lam ε| ^ (2 * m) * ‖∫ (q : R324PhysicalPoint m), ρ.r324RefinedEndpointNonzeroRoutePhysicalCore hm ε α β hexternal hε hε1 hmtrunc p route q ∂r324PhysicalMeasure m‖ ≤ 16 * paperFourthOrderModeDecay α * paperFourthOrderModeDecay β * ∫ (v : Fin (2 * m) → T4), ρ.r324RefinedEndpointNonzeroRoutedDensityTerm lam hm ε α β hexternal hε hε1 hmtrunc i p route v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

Each exact signed route coefficient is controlled by every marked slot version of its corrected routed density.

Direct route terms and their marked-slot budgets #

noncomputable def Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteMomentTerm (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

The exact contribution of one corrected route to the deterministic moment expansion.

Equations

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

Instances For

noncomputable def Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

A route pays all marked slots at once. Consequently any slot may later be selected by the central-frequency pigeonhole argument without changing the route enumeration.

Equations

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

Instances For

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteWeight_nonneg (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

0 ≤ ρ.r324RefinedEndpointNonzeroRouteWeight lam hm ε α β hexternal hε hε1 hmtrunc p route

noncomputable def Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteRawMajorant (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

Uniform raw majorant for a corrected route. The only infinite factor is the genuine fibre sum of the already-proved degree-eight raw covariance route weights; the skeleton envelope is a finite contraction sum.

Equations

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

Instances For

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteRawMajorant_nonneg (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

0 ≤ ρ.r324RefinedEndpointNonzeroRouteRawMajorant lam hm ε α β hexternal hε hε1 hmtrunc p route

theorem Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteWeight_le_rawMajorant (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

ρ.r324RefinedEndpointNonzeroRouteWeight lam hm ε α β hexternal hε hε1 hmtrunc p route ≤ ρ.r324RefinedEndpointNonzeroRouteRawMajorant lam hm ε α β hexternal hε hε1 hmtrunc p route

theorem Anderson4D.SmoothCutoff.summable_r324RefinedEndpointNonzeroRouteRawMajorant (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) :

Summable fun (route : R324NonzeroRouteLabel m) => ρ.r324RefinedEndpointNonzeroRouteRawMajorant lam hm ε α β hexternal hε hε1 hmtrunc p route

Qualitative summability of the raw majorants on one refined schedule, obtained by the exact route-fibre partition of the weighted raw covariance series.

theorem Anderson4D.SmoothCutoff.summable_all_r324RefinedEndpointNonzeroRouteWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) :

Summable fun (pr : R324RefinedScheduleIndex m × R324NonzeroRouteLabel m) => ρ.r324RefinedEndpointNonzeroRouteWeight lam hm ε α β hexternal hε hε1 hmtrunc pr.1 pr.2

The corrected route weights are independently summable; this is a theorem of the raw cutoff decay, not a field supplied by phase A.

theorem Anderson4D.SmoothCutoff.norm_r324RefinedEndpointNonzeroRouteMomentTerm_le_slotDecay (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (i : Fin m) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

‖ρ.r324RefinedEndpointNonzeroRouteMomentTerm lam hm ε α β hexternal hε hε1 hmtrunc p route‖ ≤ (16 * paperFourthOrderModeDecay α * paperFourthOrderModeDecay β * ∫ (v : Fin (2 * m) → T4), ρ.r324RefinedEndpointNonzeroRoutedDensityTerm lam hm ε α β hexternal hε hε1 hmtrunc i p route v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) * eighthOrderFrequencyDecay ‖z4EuclideanFrequency (route.2.1 i)‖

The exact route term is paid by any one of its marked-slot densities, with the reciprocal eighth-order cost restored as decay.

theorem Anderson4D.SmoothCutoff.norm_r324RefinedEndpointNonzeroRouteMomentTerm_le_weight_mul_decay (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (i : Fin m) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) :

‖ρ.r324RefinedEndpointNonzeroRouteMomentTerm lam hm ε α β hexternal hε hε1 hmtrunc p route‖ ≤ ρ.r324RefinedEndpointNonzeroRouteWeight lam hm ε α β hexternal hε hε1 hmtrunc p route * eighthOrderFrequencyDecay ‖z4EuclideanFrequency (route.2.1 i)‖

Paying the finite sum of all slot densities makes the local decay estimate uniform in the subsequently selected slot.

Exact countable route expansion #

theorem Anderson4D.SmoothCutoff.summable_r324RefinedEndpointNonzeroRouteMomentTerm (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) :

Summable fun (route : R324NonzeroRouteLabel m) => ρ.r324RefinedEndpointNonzeroRouteMomentTerm lam hm ε α β hexternal hε hε1 hmtrunc p route

For one refined schedule, the exact corrected route terms form an absolutely summable series. This is inherited from the raw complete endpoint coefficients and the genuine route-fibre partition.

theorem Anderson4D.SmoothCutoff.summable_all_r324RefinedEndpointNonzeroRouteMomentTerm (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) :

Summable fun (pr : R324RefinedScheduleIndex m × R324NonzeroRouteLabel m) => ρ.r324RefinedEndpointNonzeroRouteMomentTerm lam hm ε α β hexternal hε hε1 hmtrunc pr.1 pr.2

Absolute summability after adjoining the finite refined-schedule index.

theorem Anderson4D.SmoothCutoff.deterministicMomentPairingSum_eq_tsum_nonzeroRouteMomentTerm (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) :

deterministicMomentPairingSum ρ lam ε m α β = ∑' (pr : R324RefinedScheduleIndex m × R324NonzeroRouteLabel m), ρ.r324RefinedEndpointNonzeroRouteMomentTerm lam hm ε α β hexternal hε hε1 hmtrunc pr.1 pr.2

The deterministic moment is exactly the tsum over the corrected schedule/route product.

noncomputable def Anderson4D.SmoothCutoff.r324NatEquivRefinedEndpointNonzeroRoutes {m : ℕ} (hm : 0 < m) :

ℕ ≃ R324RefinedScheduleIndex m × R324NonzeroRouteLabel m

The finite schedule index times the corrected countable route label is denumerable when m > 0.

Equations

Anderson4D.SmoothCutoff.r324NatEquivRefinedEndpointNonzeroRoutes hm = (Denumerable.eqv (Anderson4D.R324RefinedScheduleIndex m × Anderson4D.SmoothCutoff.R324NonzeroRouteLabel m)).symm

Instances For

noncomputable def Anderson4D.SmoothCutoff.r324RefinedEndpointNonzeroRouteIncrement (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (pr : R324RefinedScheduleIndex m × R324NonzeroRouteLabel m) (i : Fin m) :

EuclideanSpace ℝ (Fin dim)

Nonzero route terms use their genuine complete key. Zero terms use a harmless delta route so that frequency conservation remains an unconditional field of the countable decomposition.

Equations

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

Instances For

theorem Anderson4D.SmoothCutoff.sum_r324RefinedEndpointNonzeroRouteIncrement (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (pr : R324RefinedScheduleIndex m × R324NonzeroRouteLabel m) :

∑ i : Fin m, ρ.r324RefinedEndpointNonzeroRouteIncrement lam hm ε α β hexternal hε hε1 hmtrunc pr i = z4EuclideanFrequency (α + β)

A nonzero corrected route term has an inhabited genuine route fibre, hence its complete key sums to the external frequency.

theorem Anderson4D.SmoothCutoff.countableCentralRoutedMomentReductionOutput_of_nonzeroRoutes (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (weightBudget : ℝ) (hbudget : ∑' (pr : R324RefinedScheduleIndex m × R324NonzeroRouteLabel m), ρ.r324RefinedEndpointNonzeroRouteWeight lam hm ε α β hexternal hε hε1 hmtrunc pr.1 pr.2 ≤ weightBudget) :

CountableCentralRoutedMomentReductionOutput ρ lam ε m α β weightBudget

Direct constructor of the central countable routing output from the route weights.

The zero external-shift branch #

noncomputable def Anderson4D.SmoothCutoff.r324ZeroShiftGroupedCoreWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m × ℕ) :

Endpoint-free L¹ weight of a grouped configuration, without any artificial reciprocal central-frequency cost.

Equations

ρ.r324ZeroShiftGroupedCoreWeight lam hm ε p = |Anderson4D.lamEps lam ε| ^ (2 * m) * ρ.r324GroupedRefinedCoreL1 hm ε p

Instances For

theorem Anderson4D.SmoothCutoff.r324ZeroShiftGroupedCoreWeight_nonneg (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m × ℕ) :

0 ≤ ρ.r324ZeroShiftGroupedCoreWeight lam hm ε p

noncomputable def Anderson4D.SmoothCutoff.r324ZeroShiftGroupedWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m × ℕ) :

Four endpoint integrations applied to the zero-shift grouped term. There is no eighth-order slot cost because the central decay is exactly one in this branch.

Equations

ρ.r324ZeroShiftGroupedWeight lam hm ε α β p = 16 * Anderson4D.paperFourthOrderModeDecay α * Anderson4D.paperFourthOrderModeDecay β * ρ.r324ZeroShiftGroupedCoreWeight lam hm ε p

Instances For

theorem Anderson4D.SmoothCutoff.r324ZeroShiftGroupedWeight_nonneg (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m × ℕ) :

0 ≤ ρ.r324ZeroShiftGroupedWeight lam hm ε α β p

theorem Anderson4D.SmoothCutoff.summable_r324ZeroShiftGroupedCoreWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) :

Summable (ρ.r324ZeroShiftGroupedCoreWeight lam hm ε)

The no-cost zero-shift core weights are qualitatively summable. The degree-eight grouped weights are used only as a summable majorant; the zero-shift weight itself contains no such cost.

theorem Anderson4D.SmoothCutoff.summable_r324ZeroShiftGroupedWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) :

Summable (ρ.r324ZeroShiftGroupedWeight lam hm ε α β)

theorem Anderson4D.SmoothCutoff.norm_r324GroupedEndpointConfigurationTerm_le_zeroShiftWeight (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m × ℕ) (hcore : MeasureTheory.Integrable (fun (v : Fin (2 * m) → T4) => ‖ρ.r324KeyGroupedRefinedEndpointCore hm ε p.1 p.2 v‖) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)) :

‖r324GroupedEndpointConfigurationTerm hm ρ lam ε α β (r324RefinedScheduleRepresentative p.1) (ρ.r324KeyGroupedRefinedEndpointCore hm ε p.1 p.2)‖ ≤ ρ.r324ZeroShiftGroupedWeight lam hm ε α β p

Local endpoint Fourier estimate for a grouped configuration, with no central-frequency cost.

theorem Anderson4D.SmoothCutoff.countableCentralRoutedMomentReductionOutput_of_zeroShift (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hshift : α + β = 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (weightBudget : ℝ) (hbudget : ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324ZeroShiftGroupedWeight lam hm ε α β p ≤ weightBudget) :

CountableCentralRoutedMomentReductionOutput ρ lam ε m α β weightBudget

Honest countable central decomposition when the external shift is zero. No first-large selector is invoked: all routed increments are zero, so every central decay factor is exactly one.

noncomputable def Anderson4D.SmoothCutoff.r324EndpointNonzeroRoutedCaseDensity (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (i : Fin m) (cases : R324EndpointReductionPattern) (v : Fin (2 * m) → T4) :

Corrected density of one actual endpoint-reduction pattern. The endpoint-null deletion and endpoint Fourier integrations have already been completed, so this density lives only on the internal variables.

Equations

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

Instances For

theorem Anderson4D.SmoothCutoff.r324EndpointNonzeroRoutedCaseDensity_nonneg (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (i : Fin m) (cases : R324EndpointReductionPattern) (v : Fin (2 * m) → T4) :

0 ≤ ρ.r324EndpointNonzeroRoutedCaseDensity lam hm ε α β hexternal hε hε1 hmtrunc i cases v

Honest downstream enlargement / phase-A interface #

structure Anderson4D.SmoothCutoff.R324EndpointNonzeroDensityPhaseAOutput (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (primitiveConstant supportConstant : ℝ) :