Exact covariance-factor reassembly of one refined quad harvest

The canonical high-frequency covariance mode is selected separately on each endpoint-nonzero Fourier configuration. Consequently its lattice mode is not constant on the complete refined fibre. The exact object which can be reassembled is therefore a signed double series, first over the genuine corrected route fibres and then over the members of each fibre. This file keeps both sums intact.

For every member we remove exactly one covariance coefficient before the physical integral. We then reassemble the endpoint phases, the signed route fibres, and the complete refined fibre. No norm is taken on an entity, configuration, or route.

The final analytic boundary is a single norm of the already reassembled signed series. In particular, this file does not replace that norm by a sum of route norms.

Removing the selected coefficient on one genuine raw member

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawSelectedCovarianceMode (rho : SmoothCutoff) {m : ℕ} (hm : 0 < m) (eps : ℝ) (alpha beta : Z4) (hexternal : alpha + beta ≠ 0) (heps : 0 < eps) (heps1 : eps ≤ 1) (hmtrunc : m ≤ truncOrder eps) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : rho.r324RefinedRawFullPairingIntegral hm eps alpha beta p a ≠ 0) : Z4

The actual lattice mode on the canonical selected cross-pair of one endpoint-nonzero raw refined Fourier member.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawOpenCovarianceCore (rho : SmoothCutoff) {m : ℕ} (hm : 0 < m) (eps : ℝ) (alpha beta : Z4) (hexternal : alpha + beta ≠ 0) (heps : 0 < eps) (heps1 : eps ≤ 1) (hmtrunc : m ≤ truncOrder eps) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : rho.r324RefinedRawFullPairingIntegral hm eps alpha beta p a ≠ 0) (v : Fin (2 * m) → T4) : ℂ

The signed internal term after deleting only the selected covariance coefficient. Its character, both Green cores, and every unselected fixed Fourier mode remain in the amplitude.

Equations

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

theorem Anderson4D.SmoothCutoff.r324RefinedRawSelectorRestrictedSignedCore_eq_coeff_mul_open (rho : SmoothCutoff) {m : ℕ} (hm : 0 < m) (eps : ℝ) (alpha beta : Z4) (hexternal : alpha + beta ≠ 0) (heps : 0 < eps) (heps1 : eps ≤ 1) (hmtrunc : m ≤ truncOrder eps) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : rho.r324RefinedRawFullPairingIntegral hm eps alpha beta p a ≠ 0) (v : Fin (2 * m) → T4) : rho.r324RefinedRawSelectorRestrictedSignedCore hm eps alpha beta hexternal heps heps1 hmtrunc p a hne v = rho.covarianceModeCoeff eps (rho.r324RefinedRawSelectedCovarianceMode hm eps alpha beta hexternal heps heps1 hmtrunc p a hne) * rho.r324RefinedRawOpenCovarianceCore hm eps alpha beta hexternal heps heps1 hmtrunc p a hne v

Exact pointwise removal of the selected covariance coefficient from one selector-restricted signed internal term.

Endpoint phases and the physical integral

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawOpenCovarianceIntegrand (rho : SmoothCutoff) {m : ℕ} (hm : 0 < m) (eps : ℝ) (alpha beta : Z4) (hexternal : alpha + beta ≠ 0) (heps : 0 < eps) (heps1 : eps ≤ 1) (hmtrunc : m ≤ truncOrder eps) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : rho.r324RefinedRawFullPairingIntegral hm eps alpha beta p a ≠ 0) (x y z w : T4) (v : Fin (2 * m) → T4) : ℂ

The complete five-group physical integrand after removal of the one selected covariance coefficient.

Equations

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

theorem Anderson4D.SmoothCutoff.r324RefinedRawEndpointIntegrand_eq_coeff_mul_open (rho : SmoothCutoff) {m : ℕ} (hm : 0 < m) (eps : ℝ) (alpha beta : Z4) (hexternal : alpha + beta ≠ 0) (heps : 0 < eps) (heps1 : eps ≤ 1) (hmtrunc : m ≤ truncOrder eps) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : rho.r324RefinedRawFullPairingIntegral hm eps alpha beta p a ≠ 0) (x y z w : T4) (v : Fin (2 * m) → T4) : rho.r324RefinedRawEndpointIntegrand hm eps alpha beta p a x y z w v = rho.covarianceModeCoeff eps (rho.r324RefinedRawSelectedCovarianceMode hm eps alpha beta hexternal heps heps1 hmtrunc p a hne) * rho.r324RefinedRawOpenCovarianceIntegrand hm eps alpha beta hexternal heps heps1 hmtrunc p a hne x y z w v

Exact coefficient removal survives all four endpoint phases pointwise.

theorem Anderson4D.SmoothCutoff.r324RefinedRawFullPairingIntegral_eq_coeff_mul_openIntegral (rho : SmoothCutoff) {m : ℕ} (hm : 0 < m) (eps : ℝ) (alpha beta : Z4) (hexternal : alpha + beta ≠ 0) (heps : 0 < eps) (heps1 : eps ≤ 1) (hmtrunc : m ≤ truncOrder eps) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : rho.r324RefinedRawFullPairingIntegral hm eps alpha beta p a ≠ 0) : rho.r324RefinedRawFullPairingIntegral hm eps alpha beta p a = rho.covarianceModeCoeff eps (rho.r324RefinedRawSelectedCovarianceMode hm eps alpha beta hexternal heps heps1 hmtrunc p a hne) * ∫ (q : R324PhysicalPoint m), r324Flatten (rho.r324RefinedRawOpenCovarianceIntegrand hm eps alpha beta hexternal heps heps1 hmtrunc p a hne) q ∂r324PhysicalMeasure m

The complete physical coefficient of one raw member is its selected covariance coefficient times the signed open physical integral.

Complete signed refined-fibre reassembly

noncomputable def Anderson4D.SmoothCutoff.r324RefinedQuadOpenCovarianceSeries (rho : SmoothCutoff) {m : ℕ} (hm : 0 < m) (eps : ℝ) (alpha beta : Z4) (hexternal : alpha + beta ≠ 0) (heps : 0 < eps) (heps1 : eps ≤ 1) (hmtrunc : m ≤ truncOrder eps) (p : R324RefinedScheduleIndex m) : ℂ

The signed series which remains after one covariance coefficient has been removed separately on every endpoint-nonzero Fourier member. The outer route partition and each inner fibre sum are both retained exactly.

Equations

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

theorem Anderson4D.SmoothCutoff.endpointDecay_mul_r324BetaQuadHarvest_eq_openCovarianceSeries (rho : SmoothCutoff) {m : ℕ} (hm : 0 < m) (eps : ℝ) (alpha beta : Z4) (hexternal : alpha + beta ≠ 0) (heps : 0 < eps) (heps1 : eps ≤ 1) (hmtrunc : m ≤ truncOrder eps) (p : R324RefinedScheduleIndex m) : ↑(paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta) * r324BetaQuadHarvest rho eps m alpha beta hm (momentRefinedContractionFiber m ↑p.fst ↑p.snd) = rho.r324RefinedQuadOpenCovarianceSeries hm eps alpha beta hexternal heps heps1 hmtrunc p

Exact full-fibre covariance reassembly. The endpoint-decay multiple of the complete quad harvest is precisely the signed open series. No triangle inequality occurs in this identity.

Signed open-series bound

def Anderson4D.SmoothCutoff.R324RefinedQuadOpenCovarianceSeriesBound (rho : SmoothCutoff) (K : ℝ) : Prop

A cancellation-preserving bound on the already reassembled signed open series. This is intentionally one norm of the complete series, not a tsum of route or entity norms.

Equations

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

theorem Anderson4D.SmoothCutoff.norm_r324BetaQuadHarvest_le_of_openCovarianceSeriesBound (rho : SmoothCutoff) {m : ℕ} (hm : 0 < m) (eps : ℝ) (alpha beta : Z4) (hexternal : alpha + beta ≠ 0) (heps : 0 < eps) (hepssmall : eps ≤ 1 / 4) (hlog : 1 ≤ |Real.log eps|) (hm2 : 2 ≤ m) (hmtrunc : m ≤ truncOrder eps) (p : R324RefinedScheduleIndex m) {K : ℝ} (hbound : rho.R324RefinedQuadOpenCovarianceSeriesBound K) : ‖r324BetaQuadHarvest rho eps m alpha beta hm (momentRefinedContractionFiber m ↑p.fst ↑p.snd)‖ ≤ ↑m ^ 8 * K ^ m * |Real.log eps| ^ (m - 1) * (eps⁻¹ ^ 8 * eighthOrderFrequencyDecay (eps ^ 2 * ‖z4EuclideanFrequency (alpha + beta)‖))

The preceding whole-series estimate gives the desired paper-scale quad-harvest estimate by cancelling the strictly positive endpoint decays.