Closing the with-prefix branch of the left parametrix identity

This module reindexes the actual marked-single contraction sum by the paper's minimal non-split head prefix and applies the fixed-data case-(3) bridge. Every reindexing is an equivalence, so no multiplicity factor is introduced.

def Anderson4D.PartialPairing.withPrefixMarkedEquiv (n : ℕ) : { d : MarkedSingle (Fin n) // markedHasHeadPrefix d } ≃ { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedWithPrefix }

Marked old singles whose new head has a fully paired prefix are in bijection with the paper's case-(3) ambient pairings.

Equations

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

theorem Anderson4D.PartialPairing.leftWithPrefixContractionSum_eq_headDeletionSum (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) : leftWithPrefixContractionSum M ρ lam ε n x y ω = ∑ κ : { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedWithPrefix }, headPairedContractionContribution M ρ lam ε n ((↑κ).headDeletionData ⋯) x y ω

Reindex the still-unreduced with-prefix contraction sum by its ambient case-(3) pairing.

Exact-cardinality specialization of a fixed q fibre

def Anderson4D.PartialPairing.caseThreeExactTailPairing (p r : ℕ) (τ : PartialPairing (Fin (2 * p + 1 + r + 1 - 2 * (p + 1)))) : PartialPairing (Fin r)

Cast the tail type produced by assembleCaseThree at the exact old order 2p+1+r back to the paper tail type Fin r.

Equations

• Anderson4D.PartialPairing.caseThreeExactTailPairing p r τ = Anderson4D.PartialPairing.arithmeticCastPairing ⋯ τ

def Anderson4D.PartialPairing.caseThreeExactTailPairingEquiv (p r : ℕ) : PartialPairing (Fin (2 * p + 1 + r + 1 - 2 * (p + 1))) ≃ PartialPairing (Fin r)

The tail cast above is an actual equivalence of pairing types, used to reindex the finite tail sum without multiplicity.

Equations

• Anderson4D.PartialPairing.caseThreeExactTailPairingEquiv p r = Anderson4D.PartialPairing.congr (Fin.castOrderIso ⋯).toEquiv

@[simp]

theorem Anderson4D.PartialPairing.caseThreeExactTailPairingEquiv_apply (p r : ℕ) (τ : PartialPairing (Fin (2 * p + 1 + r + 1 - 2 * (p + 1)))) : (caseThreeExactTailPairingEquiv p r) τ = caseThreeExactTailPairing p r τ

@[simp]

theorem Anderson4D.PartialPairing.caseThreeExactTailPairing_apply_val (p r : ℕ) (τ : PartialPairing (Fin (2 * p + 1 + r + 1 - 2 * (p + 1)))) (j : Fin (2 * p + 1 + r + 1 - 2 * (p + 1))) : ↑((caseThreeExactTailPairing p r τ) (Fin.cast ⋯ j)) = ↑(τ j)

theorem Anderson4D.PartialPairing.assembleCaseThree_exact_eq_caseThreeHeadPairing (p r : ℕ) (σ : PartialPairing (Fin (2 * (p + 1)))) (τ : PartialPairing (Fin (2 * p + 1 + r + 1 - 2 * (p + 1)))) : assembleCaseThree ⋯ σ τ = caseThreeHeadPairing p r σ (caseThreeExactTailPairing p r τ)

At an exact old order, the canonical ambient assembly is literally the arithmetic successor presentation used by the fixed-data head-deletion bridge.

theorem Anderson4D.PartialPairing.headDeletionData_assembleCaseThree_exact (p r : ℕ) (σ : PartialPairing (Fin (2 * (p + 1)))) (τ : PartialPairing (Fin (2 * p + 1 + r + 1 - 2 * (p + 1)))) (hσ : IsNonSplit σ) : (assembleCaseThree ⋯ σ τ).headDeletionData ⋯ = caseThreeHeadDeletionData p r σ (caseThreeExactTailPairing p r τ) hσ

Head deletion respects the exact canonical case-(3) assembly.

theorem Anderson4D.PartialPairing.randRI_arithmeticCast (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) {m n : ℕ} (h : m = n) (κ : PartialPairing (Fin m)) (x y : T4) (ω : M.Ω) : randRI M ρ lam ε n (arithmeticCastPairing h κ) x y ω = randRI M ρ lam ε m κ x y ω

randRI is invariant under the canonical transport between propositionally equal finite cardinalities.

theorem Anderson4D.PartialPairing.randRI_assembleCaseThree_exact (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (p r : ℕ) (σ : PartialPairing (Fin (2 * (p + 1)))) (τ : PartialPairing (Fin (2 * p + 1 + r + 1 - 2 * (p + 1)))) (x y : T4) (ω : M.Ω) : randRI M ρ lam ε (2 * p + 1 + r + 1) (assembleCaseThree ⋯ σ τ) x y ω = randRI M ρ lam ε (2 * (p + 1) + r) (σ.appendPairing (caseThreeExactTailPairing p r τ)) x y ω

The ambient random kernel of an exact canonical assembly is the paper-facing appended-pairing kernel.

Fixed fibre collapse

theorem Anderson4D.PartialPairing.sum_caseThreeExactFiber_headDeletion_eq_randRI_add_counterterm (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (p r : ℕ) (x y : T4) (ω : M.Ω) (hhead : CaseThreeHeadContractionIntegrability M ρ ε p r x y ω) (hsum : CaseThreeSummationIntegrability M ρ lam ε p r x y ω) : ∑ K : { κ : PartialPairing (Fin (2 * p + 1 + r + 1)) // κ.HeadPairedWithPrefix } with caseThreeQ K = p + 1, headPairedContractionContribution M ρ lam ε (2 * p + 1 + r) ((↑K).headDeletionData ⋯) x y ω = ∑ K : { κ : PartialPairing (Fin (2 * p + 1 + r + 1)) // κ.HeadPairedWithPrefix } with caseThreeQ K = p + 1, randRI M ρ lam ε (2 * p + 1 + r + 1) (↑K) x y ω + caseThreeCountertermBlock M ρ lam ε (p + 1) r x y ω

A complete fixed minimal-prefix fibre: after canonical multiplicity-one reindexing, its actual head-deletion contractions are the corresponding ambient random kernels plus the paper counterterm block.

All minimal prefixes at a fixed old order

structure Anderson4D.PartialPairing.LeftWithPrefixCaseThreeIntegrability (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) : Prop

Analytic ledger for every paper minimal-prefix order q ∈ [1, ⌊(n+1)/2⌋]. The fixed-data bridge uses zero-based q-1, while the counterterm and the paper use the positive order q.

• contraction (q : ℕ) : q ∈ Finset.Icc 1 ((n + 1) / 2) → CaseThreeHeadContractionIntegrability M ρ ε (q - 1) (n + 1 - 2 * q) x y ω
• summation (q : ℕ) : q ∈ Finset.Icc 1 ((n + 1) / 2) → CaseThreeSummationIntegrability M ρ lam ε (q - 1) (n + 1 - 2 * q) x y ω

theorem Anderson4D.PartialPairing.leftWithPrefixContractionSum_eq_randRISum_add_countertermSum (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) (hint : LeftWithPrefixCaseThreeIntegrability M ρ lam ε n x y ω) : leftWithPrefixContractionSum M ρ lam ε n x y ω = leftWithPrefixRandRISum M ρ lam ε n x y ω + leftOrderCountertermSum M ρ lam ε n x y ω

Closed case-(3) branch of Proposition 3.4.

At fixed old order n, summing every actual with-prefix Wick contraction over the unique minimal prefix q ∈ Icc 1 ((n+1)/2) gives every ambient with-prefix random kernel once, plus the full fixed-order counterterm sum.

Direct assembly into the left parametrix identity

theorem Anderson4D.PartialPairing.leftPreconditionedParametrixAction_eq_green_add_remainder_of_integrability (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (x y : T4) (ω : M.Ω) (hsource : ∀ n ∈ Finset.range A, LeftOrderSourceIntegrability M ρ lam ε n x y ω) (hsplit : ∀ n ∈ Finset.range A, ∀ (κ : PartialPairing (Fin n)), LeftPairingSplitIntegrability M ρ ε n κ x y ω) (hcreation : ∀ n ∈ Finset.range A, ∀ (κ : PartialPairing (Fin n)), 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)) (hnoPrefix : ∀ n ∈ Finset.range A, ∀ (d : { d : MarkedSingle (Fin n) // ¬markedHasHeadPrefix d }), 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)) (hcaseThree : ∀ n ∈ Finset.range A, LeftWithPrefixCaseThreeIntegrability M ρ lam ε n x y ω) : leftPreconditionedParametrixAction M ρ lam ε A x y ω = greenFn (x - y) + leftPreconditionedRemainder M ρ lam ε A x y ω

The complete left preconditioned remainder identity with the case-(3) equality discharged by the explicit all-prefix integrability ledger above. No branch identity remains as a hypothesis.