The paired-head branch with a closed non-split prefix

This file connects the actual Wick-contraction summand obtained by deleting the paired head of an assembled case-(3) pairing with the J × R source used in the paper's prefix-collapse argument.

theorem Anderson4D.PartialPairing.appendPairing_nonSplit_head_ne (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) : (σ.appendPairing τ) 0 ≠ 0

The head of a non-split prefix remains paired after an arbitrary pairing is appended to it.

def Anderson4D.PartialPairing.caseThreeHeadPairing (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) : PartialPairing (Fin (2 * q + 1 + r + 1))

The assembled pairing transported to the successor presentation of its cardinality used by head deletion.

Equations

• Anderson4D.PartialPairing.caseThreeHeadPairing q r σ τ = Anderson4D.PartialPairing.arithmeticCastPairing ⋯ (σ.appendPairing τ)

theorem Anderson4D.PartialPairing.caseThreeHeadPairing_zero_ne (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) : (caseThreeHeadPairing q r σ τ) 0 ≠ 0

@[simp]

theorem Anderson4D.PartialPairing.caseThreeHeadPairing_apply_val (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (i : Fin (2 * q + 1 + r + 1)) : ↑((caseThreeHeadPairing q r σ τ) i) = ↑((σ.appendPairing τ) ⟨↑i, ⋯⟩)

def Anderson4D.PartialPairing.caseThreePrefixHeadDeletionData (q : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (hσ : IsNonSplit σ) : MarkedSingle (Fin (2 * q + 1))

Head deletion inside the non-split prefix alone.

Equations

• Anderson4D.PartialPairing.caseThreePrefixHeadDeletionData q σ hσ = σ.headDeletionData ⋯

def Anderson4D.PartialPairing.appendMarkedSingle {a b : ℕ} (d : MarkedSingle (Fin a)) (τ : PartialPairing (Fin b)) : MarkedSingle (Fin (a + b))

Append a tail pairing to marked-single data in a consecutive prefix.

Equations

• Anderson4D.PartialPairing.appendMarkedSingle d τ = { pairing := d.pairing.appendPairing τ, index := Fin.castAdd b d.index, isSingle := ⋯ }

def Anderson4D.PartialPairing.caseThreeHeadDeletionData (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) : MarkedSingle (Fin (2 * q + 1 + r))

The marked old single obtained by deleting the head of an assembled case-(3) pairing.

Equations

• Anderson4D.PartialPairing.caseThreeHeadDeletionData q r σ τ hσ = (Anderson4D.PartialPairing.caseThreeHeadPairing q r σ τ).headDeletionData ⋯

theorem Anderson4D.PartialPairing.caseThreeHeadDeletionData_eq_append (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) : caseThreeHeadDeletionData q r σ τ hσ = appendMarkedSingle (caseThreePrefixHeadDeletionData q σ hσ) τ

Deleting the assembled head acts only on the non-split prefix; the tail pairing is unchanged.

theorem Anderson4D.PartialPairing.caseThreePrefixHeadDeletion_singles (q : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (hσ : IsNonSplit σ) : (caseThreePrefixHeadDeletionData q σ hσ).pairing.singles = {(caseThreePrefixHeadDeletionData q σ hσ).index}

Removing the head pair from a full non-split prefix leaves exactly its former partner as a single.

theorem Anderson4D.PartialPairing.caseThreeHeadDeletion_singles (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) : (caseThreeHeadDeletionData q r σ τ hσ).pairing.singles = insert (caseThreeHeadDeletionData q r σ τ hσ).index (Finset.map (Fin.natAddEmb (2 * q + 1)) τ.singles)

In assembled case-(3) data, the marked prefix single is the first single in increasing order; all other singles come from the tail.

theorem Anderson4D.PartialPairing.caseThreeHeadDeletion_rank (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) : List.idxOf (caseThreeHeadDeletionData q r σ τ hσ).index ((caseThreeHeadDeletionData q r σ τ hσ).pairing.singles.sort fun (a b : Fin (2 * q + 1 + r)) => a ≤ b) = 0

The marked contraction has rank zero in the ordered singles list.

theorem Anderson4D.PartialPairing.caseThreeHeadDeletion_wickLabels_erase (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) (xt : Fin (2 * q + 1 + r + 2) → T4) : (wickAtSingleLabels (caseThreeHeadDeletionData q r σ τ hσ).pairing xt).eraseIdx (List.idxOf (caseThreeHeadDeletionData q r σ τ hσ).index ((caseThreeHeadDeletionData q r σ τ hσ).pairing.singles.sort fun (a b : Fin (2 * q + 1 + r)) => a ≤ b)) = wickAtSingleLabels τ (arithmeticCastTuple ⋯ (ambientTailTuple ⋯ xt))

After removing the marked prefix single, the ordered Wick labels are exactly the labels of the appended tail pairing.

Deterministic ledger for the deleted prefix

def Anderson4D.PartialPairing.prefixWithLeftTuple {N a : ℕ} (ha : a ≤ N) (xt : Fin (N + 2) → T4) : Fin (a + 1) → T4

The first a+1 spatial slots of an old contraction tuple. These are exactly the variables of the closed J block: its left endpoint, the a-1 remaining internal variables, and its right endpoint.

Equations

• Anderson4D.PartialPairing.prefixWithLeftTuple ha xt i = xt (Fin.castLE ⋯ i)

noncomputable def Anderson4D.PartialPairing.headDeletedPrefixCore (ρ : SmoothCutoff) (ε : ℝ) (a : ℕ) (κ : PartialPairing (Fin a)) (xt : Fin (a + 1) → T4) : ℝ

Deterministic factors carried by a head-deleted prefix, before the head--partner covariance is restored.

Equations

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

theorem Anderson4D.PartialPairing.caseThreePrefixHeadDeletion_extract_proper (q : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (hσ : IsNonSplit σ) (p : Fin (2 * q + 1) × Fin (2 * q + 1)) (hp : p ∈ extract (caseThreePrefixHeadDeletionData q σ hσ).pairing) : ↑p.2 + 1 < 2 * q + 1

Every extraction left after deleting the head of a non-split block ends strictly before the block's right endpoint.

theorem Anderson4D.PartialPairing.diffFactor_prefix_eq_headDeletedJ {N a : ℕ} (ha : a ≤ N) (xt : Fin (N + 2) → T4) (p : Fin a × Fin a) (hp : ↑p.2 + 1 < a) : diffFactor xt (eaPrefixPair ha p) = diffFactorJ (prefixWithLeftTuple ha xt) (hdSuccPair p)

A prefix extraction in an old contraction tuple is the corresponding shifted J difference factor.

theorem Anderson4D.PartialPairing.chainProduct_appendPairingTo_properPrefix {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (xt : Fin (N + 2) → T4) (hproper : ∀ p ∈ extract σ, ↑p.2 + 1 < a) : (∏ e : Fin (N + 1), if ↑e ∈ List.map (fun (p : Fin N × Fin N) => ↑p.2 + 1) (extract (appendPairingTo ha σ τ)) then 1 else greenFn (xt e.castSucc - xt e.succ)) = (∏ e : Fin a, if ↑e ∈ List.map (fun (p : Fin a × Fin a) => ↑p.2 + 1) (extract σ) then 1 else greenFn (prefixWithLeftTuple ha xt e.castSucc - prefixWithLeftTuple ha xt e.succ)) * ∏ e : Fin (N - a + 1), if ↑e ∈ List.map (fun (p : Fin (N - a) × Fin (N - a)) => ↑p.2 + 1) (extract τ) then 1 else greenFn (ambientTailTuple ha xt e.castSucc - ambientTailTuple ha xt e.succ)

Chain factors split at a consecutive prefix provided no prefix extraction removes the boundary edge.

theorem Anderson4D.PartialPairing.detIntegrand_appendPairingTo_properPrefix (ρ : SmoothCutoff) (ε : ℝ) {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (xt : Fin (N + 2) → T4) (hproper : ∀ p ∈ extract σ, ↑p.2 + 1 < a) : detIntegrand ρ ε N (appendPairingTo ha σ τ) xt = headDeletedPrefixCore ρ ε a σ (prefixWithLeftTuple ha xt) * detIntegrand ρ ε (N - a) τ (ambientTailTuple ha xt)

Closed-form factorization of an old contraction pairing into its proper head-deleted prefix and the full tail integrand.

theorem Anderson4D.PartialPairing.headDeletedPrefixCore_mul_eta_eq_detJintegrand (ρ : SmoothCutoff) (ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (hσ : IsNonSplit σ) (xt : Fin (2 * (q + 1)) → T4) : headDeletedPrefixCore ρ ε (2 * q + 1) (caseThreePrefixHeadDeletionData q σ hσ).pairing xt * ρ.etaEpsT4 ε (xt 0 - xt (caseThreePrefixHeadDeletionData q σ hσ).index.succ) = detJintegrand ρ ε (q + 1) σ xt

Restoring the head--partner covariance turns the proper head-deleted prefix ledger into the paper's full non-split J integrand.

The actual case-(3) contraction tuple

def Anderson4D.PartialPairing.caseThreeContractionTuple (q r : ℕ) (x z w y : T4) (t : Fin (2 * q + r) → T4) : Fin (2 * q + 1 + r + 2) → T4

Delete the first (new-head) internal coordinate from the ambient case-(3) tuple. The result is the old tuple integrated by the Wick contraction summand.

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.caseThreeContractionTuple_zero (q r : ℕ) (x z w y : T4) (t : Fin (2 * q + r) → T4) : caseThreeContractionTuple q r x z w y t 0 = z

theorem Anderson4D.PartialPairing.prefixWithLeftTuple_caseThreeContraction (q r : ℕ) (x z w y : T4) (t : Fin (2 * q + r) → T4) : prefixWithLeftTuple ⋯ (caseThreeContractionTuple q r x z w y t) = detJTupleSucc q z w fun (i : Fin (2 * q)) => t (Fin.castAdd r i)

The closed prefix of the contraction tuple is the tuple used in detJintegrand.

theorem Anderson4D.PartialPairing.ambientTailTuple_caseThreeContraction (q r : ℕ) (x z w y : T4) (t : Fin (2 * q + r) → T4) : ambientTailTuple ⋯ (caseThreeContractionTuple q r x z w y t) = arithmeticCastTuple ⋯ (caseThreeTailTuple q r w y t)

The tail beginning at the right endpoint w is the usual case-(3) tail tuple, up to the unavoidable arithmetic cast.

theorem Anderson4D.PartialPairing.caseThreeContractionTuple_marked (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) (x z w y : T4) (t : Fin (2 * q + r) → T4) : caseThreeContractionTuple q r x z w y t (varIdx (caseThreeHeadDeletionData q r σ τ hσ).index) = detJTupleSucc q z w (fun (i : Fin (2 * q)) => t (Fin.castAdd r i)) (caseThreePrefixHeadDeletionData q σ hσ).index.succ

The marked old variable is the same prefix coordinate as the partner restored in the closed J block.

theorem Anderson4D.PartialPairing.caseThreeHeadContraction_det_eq (ρ : SmoothCutoff) (ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) (x z w y : T4) (t : Fin (2 * q + r) → T4) : detIntegrand ρ ε (2 * q + 1 + r) (caseThreeHeadDeletionData q r σ τ hσ).pairing (caseThreeContractionTuple q r x z w y t) * ρ.etaEpsT4 ε (z - caseThreeContractionTuple q r x z w y t (varIdx (caseThreeHeadDeletionData q r σ τ hσ).index)) = detJintegrand ρ ε (q + 1) σ (detJTupleSucc q z w fun (i : Fin (2 * q)) => t (Fin.castAdd r i)) * detIntegrand ρ ε r τ (caseThreeTailTuple q r w y t)

The deterministic part of the actual Wick contraction is exactly the closed non-split J integrand times the deterministic tail integrand.

theorem Anderson4D.PartialPairing.caseThreeHeadContraction_wickLabels (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) (x z w y : T4) (t : Fin (2 * q + r) → T4) : (wickAtSingleLabels (caseThreeHeadDeletionData q r σ τ hσ).pairing (caseThreeContractionTuple q r x z w y t)).eraseIdx (List.idxOf (caseThreeHeadDeletionData q r σ τ hσ).index ((caseThreeHeadDeletionData q r σ τ hσ).pairing.singles.sort fun (a b : Fin (2 * q + 1 + r)) => a ≤ b)) = wickAtSingleLabels τ (caseThreeTailTuple q r w y t)

On the actual case-(3) tuple, erasing the marked Wick label leaves literally the ordered tail labels.

theorem Anderson4D.PartialPairing.caseThreeHeadContractionTerm_eq_jointCore (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) (x z w y : T4) (t : Fin (2 * q + r) → T4) (ω : M.Ω) : detIntegrand ρ ε (2 * q + 1 + r) (caseThreeHeadDeletionData q r σ τ hσ).pairing (caseThreeContractionTuple q r x z w y t) * (ρ.etaEpsT4 ε (z - caseThreeContractionTuple q r x z w y t (varIdx (caseThreeHeadDeletionData q r σ τ hσ).index)) * wickPolynomial (fun (a b : T4) => ρ.etaEpsT4 ε (a - b)) (fun (a : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' a) ((wickAtSingleLabels (caseThreeHeadDeletionData q r σ τ hσ).pairing (caseThreeContractionTuple q r x z w y t)).eraseIdx (List.idxOf (caseThreeHeadDeletionData q r σ τ hσ).index ((caseThreeHeadDeletionData q r σ τ hσ).pairing.singles.sort fun (a b : Fin (2 * q + 1 + r)) => a ≤ b))) ω) = caseThreeJointCore M ρ ε q r σ τ z w y ω t

Pointwise fixed-data case-(3) bridge: the actual Wick contraction integrand is the paper's joint J × R source.

Fubini for the old contraction variables

def Anderson4D.PartialPairing.caseThreeContractionInternal (q r : ℕ) (w : T4) (t : Fin (2 * q + r) → T4) : Fin (2 * q + 1 + r) → T4

Paper order (u,w,v) for the old variables after the new head has been deleted.

Equations

• Anderson4D.PartialPairing.caseThreeContractionInternal q r w t j = ⟨2 * q, ⋯⟩.insertNth w t (Fin.cast ⋯ j)

@[simp]

theorem Anderson4D.PartialPairing.caseThreeContractionInternal_prefix (q r : ℕ) (w : T4) (t : Fin (2 * q + r) → T4) (i : Fin (2 * q)) : caseThreeContractionInternal q r w t ⟨↑i, ⋯⟩ = t (Fin.castAdd r i)

@[simp]

theorem Anderson4D.PartialPairing.caseThreeContractionInternal_middle (q r : ℕ) (w : T4) (t : Fin (2 * q + r) → T4) : caseThreeContractionInternal q r w t ⟨2 * q, ⋯⟩ = w

@[simp]

theorem Anderson4D.PartialPairing.caseThreeContractionInternal_suffix (q r : ℕ) (w : T4) (t : Fin (2 * q + r) → T4) (j : Fin r) : caseThreeContractionInternal q r w t (Fin.natAdd (2 * q + 1) j) = t (Fin.natAdd (2 * q) j)

noncomputable def Anderson4D.PartialPairing.caseThreeContractionVariablesEquiv (q r : ℕ) : (Fin (2 * q + 1 + r) → T4) ≃ᵐ T4 × (Fin (2 * q + r) → T4)

Measurable coordinate separation (u,w,v) ↔ (w,(u,v)).

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.caseThreeContractionVariablesEquiv_symm_apply (q r : ℕ) (w : T4) (t : Fin (2 * q + r) → T4) : (caseThreeContractionVariablesEquiv q r).symm (w, t) = caseThreeContractionInternal q r w t

theorem Anderson4D.PartialPairing.measurePreserving_caseThreeContractionVariablesEquiv (q r : ℕ) : MeasureTheory.MeasurePreserving (⇑(caseThreeContractionVariablesEquiv q r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * q + 1 + r)) => paperMeasure) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (2 * q + r)) => paperMeasure))

theorem Anderson4D.PartialPairing.integral_caseThreeContractionVariables (q r : ℕ) (f : (Fin (2 * q + 1 + r) → T4) → ℝ) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin (2 * q + 1 + r)) => paperMeasure)) : (∫ (v : Fin (2 * q + 1 + r) → T4), f v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q + 1 + r)) => paperMeasure) = ∫ (w : T4), ∫ (t : Fin (2 * q + r) → T4), f (caseThreeContractionInternal q r w t) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q + r)) => paperMeasure ∂paperMeasure

Fubini after separating the right endpoint w of the closed prefix from the remaining old variables.

@[simp]

theorem Anderson4D.PartialPairing.caseThreeContractionTuple_last (q r : ℕ) (x z w y : T4) (t : Fin (2 * q + r) → T4) : caseThreeContractionTuple q r x z w y t (Fin.last (2 * q + 1 + r + 1)) = y

theorem Anderson4D.PartialPairing.caseThreeContractionTuple_varIdx (q r : ℕ) (x z w y : T4) (t : Fin (2 * q + r) → T4) (i : Fin (2 * q + 1 + r)) : caseThreeContractionTuple q r x z w y t (varIdx i) = caseThreeContractionInternal q r w t i

Internal slots of the reindexed old tuple agree with the explicit Fin.insertNth reconstruction used by Fubini.

theorem Anderson4D.PartialPairing.assemble_caseThreeContractionInternal (q r : ℕ) (x z w y : T4) (t : Fin (2 * q + r) → T4) : assemble z y (caseThreeContractionInternal q r w t) = caseThreeContractionTuple q r x z w y t

The tuple reconstructed by the contraction Fubini equivalence is the tuple used by the pointwise contraction bridge.

The integrated fixed-data case-(3) bridge

noncomputable def Anderson4D.PartialPairing.caseThreeHeadContractionWeightedCore (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) (x z y : T4) (v : Fin (2 * q + 1 + r) → T4) (ω : M.Ω) : ℝ

The actual marked-single contraction integrand, including the free left Green edge, before the old variables are separated into (w,t).

Equations

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

theorem Anderson4D.PartialPairing.caseThreeHeadContractionWeightedCore_reindex (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) (x z w y : T4) (t : Fin (2 * q + r) → T4) (ω : M.Ω) : caseThreeHeadContractionWeightedCore M ρ ε q r σ τ hσ x z y (caseThreeContractionInternal q r w t) ω = greenFn (x - z) * caseThreeJointCore M ρ ε q r σ τ z w y ω t

Separating the closed-prefix endpoint turns the actual contraction integrand pointwise into the case-(3) joint core.

theorem Anderson4D.PartialPairing.headPairedContractionContribution_caseThree_eq_joint (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) (x y : T4) (ω : M.Ω) (hint : ∀ᵐ (z : T4) ∂paperMeasure, MeasureTheory.Integrable (fun (v : Fin (2 * q + 1 + r) → T4) => caseThreeHeadContractionWeightedCore M ρ ε q r σ τ hσ x z y v ω) (MeasureTheory.Measure.pi fun (x : Fin (2 * q + 1 + r)) => paperMeasure)) : headPairedContractionContribution M ρ lam ε (2 * q + 1 + r) (caseThreeHeadDeletionData q r σ τ hσ) x y ω = caseThreeJointContribution M ρ lam ε q r σ τ x y ω

Actual fixed-data case-(3) contraction bridge. The marked-single multiple integral obtained by deleting the paired head of appendPairing σ τ is exactly the existing joint case-(3) contribution. The sole analytic assumption is integrability of the old-variable contraction integrand, which licenses the displayed Fubini reindexing.

theorem Anderson4D.PartialPairing.headPairedContractionContribution_caseThree_eq_factorized (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) (x y : T4) (ω : M.Ω) (hint : ∀ᵐ (z : T4) ∂paperMeasure, MeasureTheory.Integrable (fun (v : Fin (2 * q + 1 + r) → T4) => caseThreeHeadContractionWeightedCore M ρ ε q r σ τ hσ x z y v ω) (MeasureTheory.Measure.pi fun (x : Fin (2 * q + 1 + r)) => paperMeasure)) : headPairedContractionContribution M ρ lam ε (2 * q + 1 + r) (caseThreeHeadDeletionData q r σ τ hσ) x y ω = caseThreeFactorizedContribution M ρ lam ε q r σ τ x y ω

Paper (3.18) form of the actual fixed-data contraction bridge.

def Anderson4D.PartialPairing.CaseThreeHeadContractionIntegrability (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (q r : ℕ) (x y : T4) (ω : M.Ω) : Prop

Integrability ledger for replacing every actual case-(3) marked-single contraction in a fixed prefix/tail block by its factorized paper expression. The inner statement is almost-everywhere in the outer variable, exactly as required by the subsequent Bochner integral; endpoint diagonals need not be pointwise integrable in four dimensions.

Equations

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

theorem Anderson4D.PartialPairing.sum_headPairedCaseThreeContribution_eq_randRI_add_counterterm (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (x y : T4) (ω : M.Ω) (hhead : CaseThreeHeadContractionIntegrability M ρ ε q r x y ω) (hsum : CaseThreeSummationIntegrability M ρ lam ε q r x y ω) : ∑ σ : { σ : PartialPairing (Fin (2 * (q + 1))) // IsNonSplit σ }, ∑ τ : PartialPairing (Fin r), headPairedContractionContribution M ρ lam ε (2 * q + 1 + r) (caseThreeHeadDeletionData q r (↑σ) τ ⋯) x y ω = ∑ σ : PartialPairing (Fin (2 * (q + 1))) with IsNonSplit σ, ∑ τ : PartialPairing (Fin r), randRI M ρ lam ε (2 * (q + 1) + r) (σ.appendPairing τ) x y ω + caseThreeCountertermBlock M ρ lam ε (q + 1) r x y ω

The finite non-split-prefix/tail sum of the actual marked-single contraction sources is the ambient appended-pairing sum plus the collapsed counterterm block. This is the summation-facing form of the case-(3) contraction bridge.