The physical/operator bridge for the finite parametrix

The pairing definition of the finite parametrix is convenient for the probabilistic estimates, while inversion needs a bounded factor of the form Q * G. This file constructs that factor from the finite graded resolvent words. Every word is a finite product of bounded Green and multiplication operators, so no inverse of the smoothing Green operator is introduced.

The analytic comparison with the pairing expansion is deliberately kept separate from the algebraic construction. In particular, no pointwise kernel realization is postulated at exceptional noise samples.

Bounded operators attached to graded words

noncomputable def Anderson4D.PartialPairing.renormWordWeightContinuousMap (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (d : ℕ) : C(T4, ℂ)

Continuous complex realization of one graded-word vertex weight.

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.renormWordWeightContinuousMap_apply (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (d : ℕ) (z : T4) : (renormWordWeightContinuousMap M ρ lam ε ω hξ d) z = ↑(renormWordWeight M ρ lam ε d z ω)

def Anderson4D.PartialPairing.renormWordL2Factor (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : List ℕ → ↥TorusL2 →L[ℂ] ↥TorusL2

The bounded factor represented by a graded word. Multiplication by greenL2Op on the right restores the final Green edge of the physical kernel.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.PartialPairing.renormWordL2Factor M ρ lam ε ω hξ [] = 1

noncomputable def Anderson4D.PartialPairing.gradedParametrixL2FactorOrder (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (n : ℕ) : ↥TorusL2 →L[ℂ] ↥TorusL2

The order-n bounded factor, summed over all compositions of the graded order.

Equations

• Anderson4D.PartialPairing.gradedParametrixL2FactorOrder M ρ lam ε ω hξ n = ∑ c : Composition n, Anderson4D.PartialPairing.renormWordL2Factor M ρ lam ε ω hξ c.blocks

noncomputable def Anderson4D.PartialPairing.gradedTruncatedParametrixL2Factor (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (A : ℕ) : ↥TorusL2 →L[ℂ] ↥TorusL2

The finite factorized parametrix through graded order A.

Equations

• Anderson4D.PartialPairing.gradedTruncatedParametrixL2Factor M ρ lam ε ω hξ A = ∑ n ∈ Finset.range (A + 1), Anderson4D.PartialPairing.gradedParametrixL2FactorOrder M ρ lam ε ω hξ n

Word actions on Fourier characters

def Anderson4D.PartialPairing.renormWordContinuousAction (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (β : Z4) : List ℕ → C(T4, ℂ)

Continuous representative of a graded word acting on a Fourier character after its final Green factor is restored.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.PartialPairing.renormWordContinuousAction M ρ lam ε ω hξ β [] = Anderson4D.greenPhysicalConvolution (Anderson4D.charT4Continuous β)

theorem Anderson4D.PartialPairing.renormWordL2Factor_mul_green_apply_char (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (β : Z4) (word : List ℕ) : (renormWordL2Factor M ρ lam ε ω hξ word * greenL2Op) (charT4Lp 2 β) = (ContinuousMap.toLp 2 haarT4 ℂ) (renormWordContinuousAction M ρ lam ε ω hξ β word)

Exact L² realization of the recursive continuous word action.

def Anderson4D.PartialPairing.renormWordActionPathWeight (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (β : Z4) (word : List ℕ) : Fin (word.length + 1) → C(T4, ℂ)

Vertex weights for the flat path attached to one graded word. The last vertex carries the input character.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.PartialPairing.renormWordActionPathWeight M ρ lam ε ω hξ β [] x_2 = Anderson4D.charT4Continuous β

@[simp]

theorem Anderson4D.PartialPairing.renormWordActionPathWeight_cons_zero (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (β : Z4) (d : ℕ) (word : List ℕ) : renormWordActionPathWeight M ρ lam ε ω hξ β (d :: word) 0 = renormWordWeightContinuousMap M ρ lam ε ω hξ d

@[simp]

theorem Anderson4D.PartialPairing.renormWordActionPathWeight_cons_succ (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (β : Z4) (d : ℕ) (word : List ℕ) (i : Fin (word.length + 1)) : renormWordActionPathWeight M ρ lam ε ω hξ β (d :: word) i.succ = renormWordActionPathWeight M ρ lam ε ω hξ β word i

theorem Anderson4D.PartialPairing.weightedGreenPath_renormWord_cons (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (β : Z4) (d : ℕ) (word : List ℕ) (x z : T4) (v : Fin (word.length + 1) → T4) : weightedGreenPath (renormWordActionPathWeight M ρ lam ε ω hξ β (d :: word)) x (Fin.cons z v) = ↑(greenFn (x - z)) * (renormWordWeightContinuousMap M ρ lam ε ω hξ d) z * weightedGreenPath (renormWordActionPathWeight M ρ lam ε ω hξ β word) z v

theorem Anderson4D.PartialPairing.renormWordContinuousAction_eq_weightedGreenPath_ae (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (β : Z4) (word : List ℕ) : ∀ᵐ (x : T4) ∂paperMeasure, (renormWordContinuousAction M ρ lam ε ω hξ β word) x = ∫ (v : Fin (word.length + 1) → T4), weightedGreenPath (renormWordActionPathWeight M ρ lam ε ω hξ β word) x v ∂MeasureTheory.Measure.pi fun (x : Fin (word.length + 1)) => paperMeasure

Every recursive word action is its flat weighted Green path for almost every left endpoint.

Identification with the graded-word kernels

noncomputable def Anderson4D.PartialPairing.renormWordKernelC (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (word : List ℕ) (x y : T4) (ω : M.Ω) : ℂ

Complex form of a graded-word kernel. This is definitionally the same integral as renormWordKernel, with the real integrand embedded in ℂ.

Equations

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

theorem Anderson4D.PartialPairing.renormWordKernelC_eq_ofReal (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (word : List ℕ) (x y : T4) (ω : M.Ω) : renormWordKernelC M ρ lam ε word x y ω = ↑(renormWordKernel M ρ lam ε word x y ω)

noncomputable def Anderson4D.PartialPairing.gradedParametrixKernelC (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) : ℂ

Complex kernel of the order-n graded parametrix.

Equations

• Anderson4D.PartialPairing.gradedParametrixKernelC M ρ lam ε n x y ω = ∑ c : Composition n, Anderson4D.PartialPairing.renormWordKernelC M ρ lam ε c.blocks x y ω

theorem Anderson4D.PartialPairing.gradedParametrixKernelC_eq_ofReal (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) : gradedParametrixKernelC M ρ lam ε n x y ω = ↑(gradedParametrix M ρ lam ε n x y ω)

noncomputable def Anderson4D.PartialPairing.renormWordFlatActionIntegrand (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (β : Z4) (word : List ℕ) (x y : T4) (v : Fin word.length → T4) : ℂ

Flat complex integrand of one word acting on a Fourier character.

Equations

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

theorem Anderson4D.PartialPairing.weightedGreenPath_renormWord_snoc (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (β : Z4) (word : List ℕ) (x y : T4) (v : Fin word.length → T4) : weightedGreenPath (renormWordActionPathWeight M ρ lam ε ω hξ β word) x (Fin.snoc v y) = renormWordFlatActionIntegrand M ρ lam ε ω β word x y v

Separating the terminal path vertex produces exactly the word kernel integrand times the input character.

theorem Anderson4D.PartialPairing.renormWordL2Factor_mul_green_apply_char_ae (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (β : Z4) (word : List ℕ) : ↑↑((renormWordL2Factor M ρ lam ε ω hξ word * greenL2Op) (charT4Lp 2 β)) =ᵐ[haarT4] fun (x : T4) => ∫ (y : T4), renormWordKernelC M ρ lam ε word x y ω * charT4 β y ∂paperMeasure

A.e. kernel form of a bounded graded-word factor followed by the final Green operator.

theorem Anderson4D.PartialPairing.ae_integrable_renormWordKernelC_mul_char (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (β : Z4) (word : List ℕ) : ∀ᵐ (x : T4) ∂paperMeasure, MeasureTheory.Integrable (fun (y : T4) => renormWordKernelC M ρ lam ε word x y ω * charT4 β y) paperMeasure

For almost every left endpoint, the word kernel acting on one Fourier character is integrable in the right endpoint.

theorem Anderson4D.PartialPairing.gradedParametrixL2FactorOrder_mul_green_apply_char_ae (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (β : Z4) (n : ℕ) : ↑↑((gradedParametrixL2FactorOrder M ρ lam ε ω hξ n * greenL2Op) (charT4Lp 2 β)) =ᵐ[haarT4] fun (x : T4) => ∫ (y : T4), gradedParametrixKernelC M ρ lam ε n x y ω * charT4 β y ∂paperMeasure

A.e. kernel action of one complete graded order.

Fourier coefficients and the physical operator

theorem Anderson4D.PartialPairing.torusL2Operator_ext_of_matrixCoeff {A B : ↥TorusL2 →L[ℂ] ↥TorusL2} (hcoeff : ∀ (α β : Z4), torusFourierMatrixCoeff A α β = torusFourierMatrixCoeff B α β) : A = B

Bounded operators on TorusL2 are determined by all their Fourier matrix coefficients.

theorem Anderson4D.PartialPairing.torusFourierMatrixCoeff_gradedParametrixL2FactorOrder_mul_green (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (n : ℕ) (α β : Z4) : torusFourierMatrixCoeff (gradedParametrixL2FactorOrder M ρ lam ε ω hξ n * greenL2Op) α β = (↑paperTorusVolume)⁻¹ * paperKernelCoeff (fun (x y : T4) => gradedParametrixKernelC M ρ lam ε n x y ω) α β

Fourier coefficient of one bounded graded order after restoring the final Green edge.

def Anderson4D.PartialPairing.ParametrixGradedCoefficientAgreement (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (ω : M.Ω) : Prop

The sole coefficient-level analytic bridge between the pairing parametrix used by P-3.5b and the graded word expansion used by the bounded operator algebra. It asks only for the integrated coefficients, not for a false all-endpoint kernel identity.

Equations

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

theorem Anderson4D.PartialPairing.gradedParametrixL2FactorOrder_mul_green_eq_canonical (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A n : ℕ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (hn : n ≤ A) (hagree : ParametrixGradedCoefficientAgreement M ρ lam ε A ω) (hcanonical : ∀ (α β : Z4), torusFourierMatrixCoeff (canonicalParametrixOrderL2Operator M ρ lam ε n ω) α β = (↑paperTorusVolume)⁻¹ * pmCoeff M ρ lam ε n α β ω) : gradedParametrixL2FactorOrder M ρ lam ε ω hξ n * greenL2Op = canonicalParametrixOrderL2Operator M ρ lam ε n ω

At a sample where the integrated pairing/graded comparison holds, the bounded graded construction equals the canonical coefficient operator at each positive order.

theorem Anderson4D.PartialPairing.gradedParametrixL2FactorOrder_zero (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : gradedParametrixL2FactorOrder M ρ lam ε ω hξ 0 = 1

The zeroth graded factor is the identity operator.

theorem Anderson4D.PartialPairing.canonicalPhysicalTruncatedParametrixL2Operator_eq (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (ω : M.Ω) : canonicalPhysicalTruncatedParametrixL2Operator M ρ lam ε A ω = greenL2Op + ∑ n ∈ Finset.range A, canonicalParametrixOrderL2Operator M ρ lam ε (n + 1) ω

The Fin-indexed physical truncation is the Green operator plus its positive canonical orders.

theorem Anderson4D.PartialPairing.gradedTruncatedParametrixL2Factor_mul_green_eq_canonical (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (hagree : ParametrixGradedCoefficientAgreement M ρ lam ε A ω) (hcanonical : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), torusFourierMatrixCoeff (canonicalParametrixOrderL2Operator M ρ lam ε n ω) α β = (↑paperTorusVolume)⁻¹ * pmCoeff M ρ lam ε n α β ω) : gradedTruncatedParametrixL2Factor M ρ lam ε ω hξ A * greenL2Op = canonicalPhysicalTruncatedParametrixL2Operator M ρ lam ε A ω

Actual physical bridge. The finite graded factor followed by G is exactly the canonical bounded operator built from the P-3.5b Fourier coefficients. The hypotheses are samplewise versions of the two honest a.e. coefficient facts; no arbitrary realization operator is quantified.

Canonical random factor and concrete P-err residuals

noncomputable def Anderson4D.PartialPairing.canonicalGradedTruncatedParametrixL2Factor (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2

Proof-independent totalization of the graded bounded factor. Continuity of the mollified noise holds almost surely at positive scale; the zero branch is used only on the exceptional set.

Equations

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

noncomputable def Anderson4D.PartialPairing.canonicalPerrRightRemainder (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2

The concrete right P-err residual for the bounded factorized Anderson operator.

Equations

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

noncomputable def Anderson4D.PartialPairing.canonicalPerrLeftRemainder (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2

The concrete left P-err residual.

Equations

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

noncomputable def Anderson4D.PartialPairing.canonicalPerrRightPhysicalRemainder (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2

Physical form of the right factor residual after restoring the final Green operator.

Equations

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

noncomputable def Anderson4D.PartialPairing.canonicalPerrLeftPhysicalRemainder (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2

Physical form of the left factor residual. The right preconditioner is 1 - M G, as forced by associativity from Q (1 - G M) G.

Equations

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

theorem Anderson4D.PartialPairing.canonicalPerrRightRemainder_mul_green_eq_physical (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (ω : M.Ω) (hbridge : canonicalGradedTruncatedParametrixL2Factor M ρ lam ε A ω * greenL2Op = canonicalPhysicalTruncatedParametrixL2Operator M ρ lam ε A ω) : canonicalPerrRightRemainder M ρ lam ε A ω * greenL2Op = canonicalPerrRightPhysicalRemainder M ρ lam ε A ω

Restoring the final Green edge turns the factor right residual into the corresponding physical preconditioned residual.

theorem Anderson4D.PartialPairing.canonicalPerrLeftRemainder_mul_green_eq_physical (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (ω : M.Ω) (hbridge : canonicalGradedTruncatedParametrixL2Factor M ρ lam ε A ω * greenL2Op = canonicalPhysicalTruncatedParametrixL2Operator M ρ lam ε A ω) : canonicalPerrLeftRemainder M ρ lam ε A ω * greenL2Op = canonicalPerrLeftPhysicalRemainder M ρ lam ε A ω

Restoring the final Green edge turns the factor left residual into the physical right-preconditioned residual.

theorem Anderson4D.PartialPairing.canonicalPerr_andersonParametrixData (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (ω : M.Ω) : AndersonParametrixData greenL2Op (mollifiedPotentialL2Op M ρ lam ε ω) (canonicalGradedTruncatedParametrixL2Factor M ρ lam ε A ω) (canonicalPerrLeftRemainder M ρ lam ε A ω) (canonicalPerrRightRemainder M ρ lam ε A ω)

The two factorized P-err identities hold for the canonical construction at every sample. This theorem contains no norm estimate: identifying and estimating the displayed residuals is the remaining analytic P-err task.

theorem Anderson4D.PartialPairing.ae_canonicalParametrixOrderL2Operator_coeff_of_momentBounds {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A : ℕ} (hfubini : ∀ (m : ℕ), 1 ≤ m → m ≤ A → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : ∀ (m : ℕ), 1 ≤ m → m ≤ A → WickAtSecondMomentLaw M ρ ε m) (hdet : ∀ (m : ℕ), 1 ≤ m → m ≤ A → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) : ∀ᵐ (ω : M.Ω), ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), torusFourierMatrixCoeff (canonicalParametrixOrderL2Operator M ρ lam ε n ω) α β = (↑paperTorusVolume)⁻¹ * pmCoeff M ρ lam ε n α β ω

P-3.5b supplies the canonical positive-order coefficient identities simultaneously through every finite truncation order.

theorem Anderson4D.PartialPairing.ae_canonicalGradedTruncatedParametrixL2Factor_mul_green_eq {M : NoiseModel} {ρ : SmoothCutoff} {lam ε : ℝ} {A : ℕ} (hε : 0 < ε) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε A ω) (hcanonical : ∀ᵐ (ω : M.Ω), ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), torusFourierMatrixCoeff (canonicalParametrixOrderL2Operator M ρ lam ε n ω) α β = (↑paperTorusVolume)⁻¹ * pmCoeff M ρ lam ε n α β ω) : ∀ᵐ (ω : M.Ω), canonicalGradedTruncatedParametrixL2Factor M ρ lam ε A ω * greenL2Op = canonicalPhysicalTruncatedParametrixL2Operator M ρ lam ε A ω

Almost-sure physical bridge for the proof-independent canonical factor.

theorem Anderson4D.PartialPairing.ae_canonicalPerrRemainders_mul_green_eq_physical {M : NoiseModel} {ρ : SmoothCutoff} {lam ε : ℝ} {A : ℕ} (hε : 0 < ε) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε A ω) (hcanonical : ∀ᵐ (ω : M.Ω), ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), torusFourierMatrixCoeff (canonicalParametrixOrderL2Operator M ρ lam ε n ω) α β = (↑paperTorusVolume)⁻¹ * pmCoeff M ρ lam ε n α β ω) : ∀ᵐ (ω : M.Ω), canonicalPerrRightRemainder M ρ lam ε A ω * greenL2Op = canonicalPerrRightPhysicalRemainder M ρ lam ε A ω ∧ canonicalPerrLeftRemainder M ρ lam ε A ω * greenL2Op = canonicalPerrLeftPhysicalRemainder M ρ lam ε A ω

Both concrete factor residuals agree almost surely with their physical preconditioned forms. These are the bounded-operator versions of paper (3.20)--(3.21); identifying the physical forms with the explicit boundary kernels is the remaining kernel-realization step.

theorem Anderson4D.PartialPairing.ae_canonicalFactorizedParametrixValid {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A : ℕ} (hfubini : ∀ (m : ℕ), 1 ≤ m → m ≤ A → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : ∀ (m : ℕ), 1 ≤ m → m ≤ A → WickAtSecondMomentLaw M ρ ε m) (hdet : ∀ (m : ℕ), 1 ≤ m → m ≤ A → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε A ω) : ∀ᵐ (ω : M.Ω), canonicalFactorizedParametrixValid M ρ lam ε A (canonicalGradedTruncatedParametrixL2Factor M ρ lam ε A) (canonicalPerrLeftRemainder M ρ lam ε A) (canonicalPerrRightRemainder M ρ lam ε A) ω

The arbitrary Qfactor/Rleft/Rright validity interface is discharged for the canonical construction. The only analytic bridge left is the integrated pairing/graded coefficient agreement.

theorem Anderson4D.PartialPairing.measureReal_compl_canonicalConstructedL2ParametrixGoodEvent_le {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A : ℕ} (hfubini : ∀ (m : ℕ), 1 ≤ m → m ≤ A → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : ∀ (m : ℕ), 1 ≤ m → m ≤ A → WickAtSecondMomentLaw M ρ ε m) (hdet : ∀ (m : ℕ), 1 ≤ m → m ≤ A → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε A ω) (hintR : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖canonicalPerrLeftRemainder M ρ lam ε A ω‖ + ‖canonicalPerrRightRemainder M ρ lam ε A ω‖) MeasureTheory.volume) (δR : ℝ) (hfirstR : ∫ (ω : M.Ω), ‖canonicalPerrLeftRemainder M ρ lam ε A ω‖ + ‖canonicalPerrRightRemainder M ρ lam ε A ω‖ ≤ δR) : MeasureTheory.volume.real (canonicalL2ParametrixGoodEvent M ρ lam ε A (canonicalGradedTruncatedParametrixL2Factor M ρ lam ε A) (canonicalPerrLeftRemainder M ρ lam ε A) (canonicalPerrRightRemainder M ρ lam ε A))ᶜ ≤ canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant powerConstant lam ε A / (ε ^ (-14)) ^ 2 + δR / ε ^ 28

Exceptional-set estimate with the canonical factor and P-err residuals, eliminating the former arbitrary validity hypothesis.