Comparing the pairing and graded parametrix expansions

The pairing expansion is the paper's definition of Pₙ; the graded word expansion makes kernel transposition transparent. This file packages only the analytic Fubini hypotheses already used by the pairing proof and proves that the two expansions satisfy the same recurrence. Consequently the actual pairing kernel is symmetric, and the right identity follows from the proved left identity without duplicating the head-case combinatorics.

structure Anderson4D.PartialPairing.ParametrixIdentityIntegrability (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) : Prop

Analytic ledger needed to compare the paper's pairing parametrix with the graded resolvent-word expansion off the endpoint diagonal. Every field is a concrete integrability condition consumed by an existing Fubini theorem. The restriction x ≠ y is essential in four dimensions: already G(x-z)G(z-y) is not integrable when x = y.

• source (n : ℕ) (x y : T4) : x ≠ y → LeftOrderSourceIntegrability M ρ lam ε n x y ω
• split (n : ℕ) (κ : PartialPairing (Fin n)) (x y : T4) : x ≠ y → LeftPairingSplitIntegrability M ρ ε n κ x y ω
• creation (n : ℕ) (κ : PartialPairing (Fin n)) (x y : T4) : x ≠ y → MeasureTheory.Integrable (fun (u : Fin (n + 1) → T4) => randIntegrand M ρ ε ((wickHeadEquiv n) (Sum.inl κ)) (assemble x y u) ω) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)
• noPrefix (n : ℕ) (d : { d : MarkedSingle (Fin n) // ¬markedHasHeadPrefix d }) (x y : T4) : x ≠ y → MeasureTheory.Integrable (fun (u : Fin (n + 1) → T4) => randIntegrand M ρ ε ((wickHeadEquiv n) (Sum.inr ↑d)) (assemble x y u) ω) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)
• caseThree (n : ℕ) (x y : T4) : x ≠ y → LeftWithPrefixCaseThreeIntegrability M ρ lam ε n x y ω
• graded (n : ℕ) (x y : T4) (k : Fin (n + 1)) (c : Composition (n - ↑k)) : x ≠ y → RenormWordIntegrable M ρ lam ε ((↑k + 1) :: c.blocks) x y ω

theorem Anderson4D.PartialPairing.leftParametrixNoiseSource_eq_parametrix_succ_add_counterterms_of_ledger (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hint : ParametrixIdentityIntegrability M ρ lam ε ω) (n : ℕ) (x y : T4) (hxy : x ≠ y) : leftParametrixNoiseSource M ρ lam ε n x y ω = parametrixP M ρ lam ε (n + 1) x y ω + leftOrderCountertermSum M ρ lam ε n x y ω

The concrete analytic ledger discharges every hypothesis of the fixed-order left pairing recurrence.

theorem Anderson4D.PartialPairing.parametrixP_eq_gradedParametrix_of_integrability (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hint : ParametrixIdentityIntegrability M ρ lam ε ω) (n : ℕ) (x y : T4) : x ≠ y → parametrixP M ρ lam ε n x y ω = gradedParametrix M ρ lam ε n x y ω

Under the explicit Fubini ledger, the paper's pairing expansion is exactly the graded word expansion.

theorem Anderson4D.PartialPairing.parametrixKernelSymmetric_of_integrability (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hint : ParametrixIdentityIntegrability M ρ lam ε ω) (n : ℕ) : ParametrixKernelSymmetric M ρ lam ε n ω

The actual pairing kernel is symmetric at every order once the concrete Fubini ledger is available.

theorem Anderson4D.PartialPairing.parametrixKernelSymmetricThrough_of_integrability (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hint : ParametrixIdentityIntegrability M ρ lam ε ω) (N : ℕ) : ParametrixKernelSymmetricThrough M ρ lam ε N ω

Symmetry is simultaneously available through every finite truncation order.

theorem Anderson4D.PartialPairing.rightParametrixNoiseSource_eq_parametrix_succ_add_counterterms_of_ledger (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hint : ParametrixIdentityIntegrability M ρ lam ε ω) (n : ℕ) (x y : T4) (hxy : x ≠ y) : rightParametrixNoiseSource M ρ lam ε n x y ω = parametrixP M ρ lam ε (n + 1) x y ω + rightOrderCountertermSum M ρ lam ε n x y ω

Paper (3.17), the fixed-order right parametrix identity, follows from the left head-case proof and the now-proved kernel symmetry.

theorem Anderson4D.PartialPairing.xi_comp_parametrix (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hint : ParametrixIdentityIntegrability M ρ lam ε ω) (n : ℕ) (x y : T4) (hxy : x ≠ y) : leftParametrixNoiseSource M ρ lam ε n x y ω = parametrixP M ρ lam ε (n + 1) x y ω + leftOrderCountertermSum M ρ lam ε n x y ω ∧ rightParametrixNoiseSource M ρ lam ε n x y ω = parametrixP M ρ lam ε (n + 1) x y ω + rightOrderCountertermSum M ρ lam ε n x y ω

Proposition 3.4, paper (3.16)--(3.17), in the bounded preconditioned kernel form used by the formalization.

The first conjunct is (3.16) after applying the Green operator on the left; the second is the mirrored right identity. hint contains only the concrete Fubini/integrability ledger needed to interpret the totalized kernel integrals. No parametrix identity or estimate is a field of that ledger.

theorem Anderson4D.PartialPairing.leftPreconditionedParametrixAction_eq_green_add_remainder_of_ledger (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hint : ParametrixIdentityIntegrability M ρ lam ε ω) (A : ℕ) (x y : T4) (hxy : x ≠ y) : leftPreconditionedParametrixAction M ρ lam ε A x y ω = greenFn (x - y) + leftPreconditionedRemainder M ρ lam ε A x y ω

The complete left preconditioned remainder identity (3.20)--(3.21) under the global concrete integrability ledger.

theorem Anderson4D.PartialPairing.rightPreconditionedParametrixAction_eq_green_add_remainder_of_ledger (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hint : ParametrixIdentityIntegrability M ρ lam ε ω) (A : ℕ) (x y : T4) (hxy : x ≠ y) : rightPreconditionedParametrixAction M ρ lam ε A x y ω = greenFn (x - y) + rightPreconditionedRemainder M ρ lam ε A x y ω

The complete right preconditioned remainder identity (3.20)--(3.21), with no separate right head-case assumptions.