Pairing reindexing for Proposition 3.4

This file supplies the finite equivalences behind the creation--contraction step in Proposition 3.4. A contraction is indexed by a partial pairing together with one marked single. Removing that marked single leaves a pairing on its complement; adjoining the new head and pairing it with the marked index is therefore exactly the paired branch of finHeadEquiv.

Removing and restoring a marked single

def Anderson4D.PartialPairing.eraseSingle {α : Type u_1} [DecidableEq α] (κ : PartialPairing α) (j : α) (hj : κ j = j) : PartialPairing { i : α // i ≠ j }

Remove a specified fixed point from a partial pairing.

Equations

• κ.eraseSingle j hj = { toFun := fun (i : { i : α // i ≠ j }) => ⟨κ ↑i, ⋯⟩, involutive := ⋯ }

@[simp]

theorem Anderson4D.PartialPairing.eraseSingle_apply_val {α : Type u_1} [DecidableEq α] (κ : PartialPairing α) (j : α) (hj : κ j = j) (i : { i : α // i ≠ j }) : ↑((κ.eraseSingle j hj) i) = κ ↑i

def Anderson4D.PartialPairing.insertSingle {α : Type u_1} [DecidableEq α] (j : α) (κ : PartialPairing { i : α // i ≠ j }) : PartialPairing α

Restore a distinguished fixed point to a pairing of its complement.

Equations

• Anderson4D.PartialPairing.insertSingle j κ = { toFun := fun (i : α) => if h : i = j then j else ↑(κ ⟨i, h⟩), involutive := ⋯ }

@[simp]

theorem Anderson4D.PartialPairing.insertSingle_apply_eq {α : Type u_1} [DecidableEq α] (j : α) (κ : PartialPairing { i : α // i ≠ j }) : (insertSingle j κ) j = j

@[simp]

theorem Anderson4D.PartialPairing.insertSingle_apply_ne {α : Type u_1} [DecidableEq α] (j : α) (κ : PartialPairing { i : α // i ≠ j }) (i : α) (hi : i ≠ j) : (insertSingle j κ) i = ↑(κ ⟨i, hi⟩)

@[simp]

theorem Anderson4D.PartialPairing.eraseSingle_insertSingle {α : Type u_1} [DecidableEq α] (j : α) (κ : PartialPairing { i : α // i ≠ j }) : (insertSingle j κ).eraseSingle j ⋯ = κ

@[simp]

theorem Anderson4D.PartialPairing.insertSingle_eraseSingle {α : Type u_1} [DecidableEq α] (κ : PartialPairing α) (j : α) (hj : κ j = j) : insertSingle j (κ.eraseSingle j hj) = κ

structure Anderson4D.PartialPairing.MarkedSingle (α : Type u_1) [Fintype α] [DecidableEq α] : Type u_1

Wick-contraction data: a partial pairing and one of its single indices. A structure (rather than a nested subtype) keeps equality of the computational fields independent of proof terms.

• pairing : PartialPairing α
• index : α
• isSingle : self.index ∈ self.pairing.singles

theorem Anderson4D.PartialPairing.MarkedSingle.ext {α : Type u_1} [Fintype α] [DecidableEq α] {d e : MarkedSingle α} (hpairing : d.pairing = e.pairing) (hindex : d.index = e.index) : d = e

theorem Anderson4D.PartialPairing.MarkedSingle.ext_iff {α : Type u_1} [Fintype α] [DecidableEq α] {d e : MarkedSingle α} : d = e ↔ d.pairing = e.pairing ∧ d.index = e.index

def Anderson4D.PartialPairing.markedSingleEquiv (α : Type u_1) [Fintype α] [DecidableEq α] : MarkedSingle α ≃ (j : α) × PartialPairing { i : α // i ≠ j }

A pairing with a marked single is equivalently a choice of the marked index and a pairing of its complement.

Equations

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

@[implicit_reducible]

noncomputable instance Anderson4D.PartialPairing.markedSingleFintype (α : Type u_1) [Fintype α] [DecidableEq α] : Fintype (MarkedSingle α)

Equations

• Anderson4D.PartialPairing.markedSingleFintype α = Fintype.ofEquiv ((j : α) × Anderson4D.PartialPairing { i : α // i ≠ j }) (Anderson4D.PartialPairing.markedSingleEquiv α).symm

Ordered singles, as used by wickAtSingleLabels

@[reducible, inline]

abbrev Anderson4D.PartialPairing.RankedSingle (α : Type u_1) [Fintype α] [LinearOrder α] : Type u_1

A pairing together with the rank of one single in increasing order.

Equations

• Anderson4D.PartialPairing.RankedSingle α = ((κ : Anderson4D.PartialPairing α) × Fin κ.singles.card)

def Anderson4D.PartialPairing.markedSingleSigmaEquiv (α : Type u_1) [Fintype α] [LinearOrder α] : (κ : PartialPairing α) × ↥κ.singles ≃ MarkedSingle α

The nested sigma representation of a marked single is definitionally the same data as MarkedSingle.

Equations

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

def Anderson4D.PartialPairing.rankedSingleEquiv (α : Type u_1) [Fintype α] [LinearOrder α] : RankedSingle α ≃ MarkedSingle α

Increasing enumeration converts the rank used in the Wick list into the corresponding marked ambient single.

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.wickAtSingleLabels_length {m : ℕ} (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) : (wickAtSingleLabels κ xt).length = κ.singles.card

The actual list index in wickAtSingleLabels is the increasing single-index enumeration.

def Anderson4D.PartialPairing.wickLabelIndexEquiv {m : ℕ} (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) : Fin (wickAtSingleLabels κ xt).length ≃ ↥κ.singles

Equations

• κ.wickLabelIndexEquiv xt = ↑((Fin.castOrderIso ⋯).trans (κ.singles.orderIsoOfFin ⋯))

@[simp]

theorem Anderson4D.PartialPairing.wickAtSingleLabels_get_eq {m : ℕ} (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) (j : Fin (wickAtSingleLabels κ xt).length) : (wickAtSingleLabels κ xt).get j = xt (varIdx ↑((κ.wickLabelIndexEquiv xt) j))

theorem Anderson4D.PartialPairing.sum_rankedSingle {α : Type u_1} {R : Type u_2} [Fintype α] [LinearOrder α] [AddCommMonoid R] (f : MarkedSingle α → R) : ∑ κ : PartialPairing α, ∑ j : Fin κ.singles.card, f ((rankedSingleEquiv α) ⟨κ, j⟩) = ∑ d : MarkedSingle α, f d

Reindex a nested Wick contraction sum by marked singles.

Creation and contraction as the two head branches

def Anderson4D.PartialPairing.wickHeadEquiv (n : ℕ) : PartialPairing (Fin n) ⊕ MarkedSingle (Fin n) ≃ PartialPairing (Fin (n + 1))

The Wick creation/contraction indexing set is exactly the set of partial pairings after adjoining a new zero-indexed head.

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.wickHeadEquiv_apply_creation (n : ℕ) (κ : PartialPairing (Fin n)) : (wickHeadEquiv n) (Sum.inl κ) = (finHeadEquiv n).symm (Sum.inl κ)

@[simp]

theorem Anderson4D.PartialPairing.wickHeadEquiv_apply_contraction (n : ℕ) (d : MarkedSingle (Fin n)) : (wickHeadEquiv n) (Sum.inr d) = (finHeadEquiv n).symm (Sum.inr ((markedSingleEquiv (Fin n)) d))

theorem Anderson4D.PartialPairing.wickHeadEquiv_creation_isSingle (n : ℕ) (κ : PartialPairing (Fin n)) : ((wickHeadEquiv n) (Sum.inl κ)).HeadIsSingle

The creation branch fixes the new head.

theorem Anderson4D.PartialPairing.wickHeadEquiv_contraction_not_isSingle (n : ℕ) (d : MarkedSingle (Fin n)) : ¬((wickHeadEquiv n) (Sum.inr d)).HeadIsSingle

The contraction branch pairs the new head with the marked old single, hence cannot fix it.

Restricted equivalences matching PairingHeadCases

def Anderson4D.PartialPairing.IsCreation {A : Type u_1} {B : Type u_2} : A ⊕ B → Prop

Predicate selecting the creation summand.

Equations

• Anderson4D.PartialPairing.IsCreation (Sum.inl val) = True
• Anderson4D.PartialPairing.IsCreation (Sum.inr val) = False

def Anderson4D.PartialPairing.IsContraction {A : Type u_1} {B : Type u_2} : A ⊕ B → Prop

Predicate selecting the contraction summand.

Equations

• Anderson4D.PartialPairing.IsContraction (Sum.inl val) = False
• Anderson4D.PartialPairing.IsContraction (Sum.inr val) = True

def Anderson4D.PartialPairing.creationSubtypeEquiv (A : Type u_1) (B : Type u_2) : { s : A ⊕ B // IsCreation s } ≃ A

A subtype of the left summand is canonically the left type.

Equations

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

def Anderson4D.PartialPairing.contractionSubtypeEquiv (A : Type u_1) (B : Type u_2) : { s : A ⊕ B // IsContraction s } ≃ B

A subtype of the right summand is canonically the right type.

Equations

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

theorem Anderson4D.PartialPairing.isCreation_iff_headIsSingle (n : ℕ) (s : PartialPairing (Fin n) ⊕ MarkedSingle (Fin n)) : IsCreation s ↔ ((wickHeadEquiv n) s).HeadIsSingle

theorem Anderson4D.PartialPairing.isContraction_iff_not_headIsSingle (n : ℕ) (s : PartialPairing (Fin n) ⊕ MarkedSingle (Fin n)) : IsContraction s ↔ ¬((wickHeadEquiv n) s).HeadIsSingle

def Anderson4D.PartialPairing.creationHeadEquiv (n : ℕ) : PartialPairing (Fin n) ≃ { κ : PartialPairing (Fin (n + 1)) // κ.HeadIsSingle }

Created pairings are exactly the HeadIsSingle class.

Equations

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

def Anderson4D.PartialPairing.contractionHeadEquiv (n : ℕ) : MarkedSingle (Fin n) ≃ { κ : PartialPairing (Fin (n + 1)) // ¬κ.HeadIsSingle }

Contracted pairings are exactly the complement of the HeadIsSingle class.

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.creationHeadEquiv_apply_val (n : ℕ) (κ : PartialPairing (Fin n)) : ↑((creationHeadEquiv n) κ) = (wickHeadEquiv n) (Sum.inl κ)

@[simp]

theorem Anderson4D.PartialPairing.contractionHeadEquiv_apply_val (n : ℕ) (d : MarkedSingle (Fin n)) : ↑((contractionHeadEquiv n) d) = (wickHeadEquiv n) (Sum.inr d)

noncomputable def Anderson4D.PartialPairing.pairedHeadCasesEquiv (n : ℕ) : { κ : PartialPairing (Fin (n + 1)) // ¬κ.HeadIsSingle } ≃ { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedNoPrefix } ⊕ { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedWithPrefix }

Split a paired-head pairing according to existence of a fully paired head prefix.

Equations

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

def Anderson4D.PartialPairing.pairedHeadCasesValue {R : Type u_1} {n : ℕ} (f : PartialPairing (Fin (n + 1)) → R) : { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedNoPrefix } ⊕ { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedWithPrefix } → R

Evaluate the same ambient-pairing function on either paired-head case.

Equations

• Anderson4D.PartialPairing.pairedHeadCasesValue f (Sum.inl κ) = f ↑κ
• Anderson4D.PartialPairing.pairedHeadCasesValue f (Sum.inr κ) = f ↑κ

@[simp]

theorem Anderson4D.PartialPairing.pairedHeadCasesValue_equiv_apply {R : Type u_1} (n : ℕ) (f : PartialPairing (Fin (n + 1)) → R) (κ : { κ : PartialPairing (Fin (n + 1)) // ¬κ.HeadIsSingle }) : pairedHeadCasesValue f ((pairedHeadCasesEquiv n) κ) = f ↑κ

noncomputable def Anderson4D.PartialPairing.contractionHeadCasesEquiv (n : ℕ) : MarkedSingle (Fin n) ≃ { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedNoPrefix } ⊕ { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedWithPrefix }

Final pairing-index equivalence for the Wick contraction sum: every marked single produces, uniquely, either case (2) or case (3) of Proposition 3.4.

Equations

• Anderson4D.PartialPairing.contractionHeadCasesEquiv n = (Anderson4D.PartialPairing.contractionHeadEquiv n).trans (Anderson4D.PartialPairing.pairedHeadCasesEquiv n)

noncomputable def Anderson4D.PartialPairing.rankedContractionHeadCasesEquiv (n : ℕ) : RankedSingle (Fin n) ≃ { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedNoPrefix } ⊕ { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedWithPrefix }

The exact index type occurring in the nested Wick contraction sum, followed by the paper case-(2)/(3) classification.

Equations

• Anderson4D.PartialPairing.rankedContractionHeadCasesEquiv n = (Anderson4D.PartialPairing.rankedSingleEquiv (Fin n)).trans (Anderson4D.PartialPairing.contractionHeadCasesEquiv n)

Finite-sum reindexing

theorem Anderson4D.PartialPairing.sum_creation_contraction {R : Type u_1} [AddCommMonoid R] (n : ℕ) (f : PartialPairing (Fin (n + 1)) → R) : ∑ κ : PartialPairing (Fin n), f ↑((creationHeadEquiv n) κ) + ∑ d : MarkedSingle (Fin n), f ↑((contractionHeadEquiv n) d) = ∑ κ : PartialPairing (Fin (n + 1)), f κ

Creation and contraction together enumerate every pairing with a new head exactly once.

theorem Anderson4D.PartialPairing.sum_contraction_headCases {R : Type u_1} [AddCommMonoid R] (n : ℕ) (f : PartialPairing (Fin (n + 1)) → R) : ∑ d : MarkedSingle (Fin n), f ↑((contractionHeadEquiv n) d) = ∑ κ : { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedNoPrefix }, f ↑κ + ∑ κ : { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedWithPrefix }, f ↑κ

The contraction sum is exactly the sum of paper head cases (2) and (3), with no multiplicity.

theorem Anderson4D.PartialPairing.sum_creation_headCase {R : Type u_1} [AddCommMonoid R] (n : ℕ) (f : PartialPairing (Fin (n + 1)) → R) : ∑ κ : PartialPairing (Fin n), f ↑((creationHeadEquiv n) κ) = ∑ κ : { κ : PartialPairing (Fin (n + 1)) // κ.HeadIsSingle }, f ↑κ

The creation sum is precisely head case (1).

theorem Anderson4D.PartialPairing.sum_ranked_contraction_headCases {R : Type u_1} [AddCommMonoid R] (n : ℕ) (f : PartialPairing (Fin (n + 1)) → R) : ∑ κ : PartialPairing (Fin n), ∑ j : Fin κ.singles.card, f ↑((contractionHeadEquiv n) ((rankedSingleEquiv (Fin n)) ⟨κ, j⟩)) = ∑ κ : { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedNoPrefix }, f ↑κ + ∑ κ : { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedWithPrefix }, f ↑κ

Nested Wick contraction ranks reindex with multiplicity one to the paper's paired-head cases.

theorem Anderson4D.PartialPairing.sum_wickIndices_headCases {R : Type u_1} [AddCommMonoid R] (n : ℕ) (f : PartialPairing (Fin (n + 1)) → R) : ∑ κ : PartialPairing (Fin n), f ↑((creationHeadEquiv n) κ) + ∑ κ : PartialPairing (Fin n), ∑ j : Fin κ.singles.card, f ↑((contractionHeadEquiv n) ((rankedSingleEquiv (Fin n)) ⟨κ, j⟩)) = ∑ κ : { κ : PartialPairing (Fin (n + 1)) // κ.HeadIsSingle }, f ↑κ + ∑ κ : { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedNoPrefix }, f ↑κ + ∑ κ : { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedWithPrefix }, f ↑κ

Full Wick indexing ledger: the created term and every contraction term enumerate the three disjoint head classes exactly once.

Concatenating a closed prefix and an external remainder

def Anderson4D.PartialPairing.sumPairing {α : Type u_1} {β : Type u_2} (σ : PartialPairing α) (τ : PartialPairing β) : PartialPairing (α ⊕ β)

Disjoint sum of two partial pairings.

Equations

• σ.sumPairing τ = { toFun := fun (x : α ⊕ β) => match x with | Sum.inl i => Sum.inl (σ i) | Sum.inr j => Sum.inr (τ j), involutive := ⋯ }

@[simp]

theorem Anderson4D.PartialPairing.sumPairing_apply_left {α : Type u_1} {β : Type u_2} (σ : PartialPairing α) (τ : PartialPairing β) (i : α) : (σ.sumPairing τ) (Sum.inl i) = Sum.inl (σ i)

@[simp]

theorem Anderson4D.PartialPairing.sumPairing_apply_right {α : Type u_1} {β : Type u_2} (σ : PartialPairing α) (τ : PartialPairing β) (j : β) : (σ.sumPairing τ) (Sum.inr j) = Sum.inr (τ j)

def Anderson4D.PartialPairing.appendPairing {a b : ℕ} (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin b)) : PartialPairing (Fin (a + b))

Concatenate pairings on two finite consecutive blocks.

Equations

• σ.appendPairing τ = (Anderson4D.PartialPairing.congr finSumFinEquiv) (σ.sumPairing τ)

@[simp]

theorem Anderson4D.PartialPairing.appendPairing_apply_castAdd {a b : ℕ} (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin b)) (i : Fin a) : (σ.appendPairing τ) (Fin.castAdd b i) = Fin.castAdd b (σ i)

@[simp]

theorem Anderson4D.PartialPairing.appendPairing_apply_natAdd {a b : ℕ} (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin b)) (j : Fin b) : (σ.appendPairing τ) (Fin.natAdd a j) = Fin.natAdd a (τ j)

def Anderson4D.PartialPairing.appendPairingTo {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) : PartialPairing (Fin N)

Concatenate a block of length a and its arithmetic complement inside Fin N.

Equations

• Anderson4D.PartialPairing.appendPairingTo ha σ τ = (Anderson4D.PartialPairing.congr (Fin.castOrderIso ⋯).toEquiv) (σ.appendPairing τ)

@[simp]

theorem Anderson4D.PartialPairing.appendPairingTo_apply_prefix {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (i : Fin a) : (appendPairingTo ha σ τ) (Fin.castLE ha i) = Fin.castLE ha (σ i)

def Anderson4D.PartialPairing.suffixFin {N a : ℕ} (ha : a ≤ N) (j : Fin (N - a)) : Fin N

Canonical embedding of a remainder coordinate after the first a entries.

Equations

• Anderson4D.PartialPairing.suffixFin ha j = ⟨a + ↑j, ⋯⟩

@[simp]

theorem Anderson4D.PartialPairing.suffixFin_val {N a : ℕ} (ha : a ≤ N) (j : Fin (N - a)) : ↑(suffixFin ha j) = a + ↑j

@[simp]

theorem Anderson4D.PartialPairing.appendPairingTo_apply_suffix {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (j : Fin (N - a)) : (appendPairingTo ha σ τ) (suffixFin ha j) = suffixFin ha (τ j)

theorem Anderson4D.PartialPairing.appendPairingTo_prefix_fullyPaired {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (hσ : σ.IsFull) : IsFullyPairedOn (appendPairingTo ha σ τ) {i : Fin N | ↑i < a}

The first block of an appended pairing is closed and full whenever the prefix pairing is full.

theorem Anderson4D.PartialPairing.prefix_fullyPaired_of_appendPairingTo {N a r : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (h : IsFullyPairedOn (appendPairingTo ha σ τ) {i : Fin N | ↑i < r}) : IsFullyPairedOn σ {i : Fin a | ↑i < r}

Any smaller fully paired prefix of an appended pairing restricts to the corresponding fully paired prefix of its first block.

The canonical case-(3) assembly

def Anderson4D.PartialPairing.assembleCaseThree {m q : ℕ} (hq : 2 * q ≤ m + 1) (σ : PartialPairing (Fin (2 * q))) (τ : PartialPairing (Fin (m + 1 - 2 * q))) : PartialPairing (Fin (m + 1))

Assemble a non-split closed head block with an arbitrary remainder.

Equations

• Anderson4D.PartialPairing.assembleCaseThree hq σ τ = Anderson4D.PartialPairing.appendPairingTo hq σ τ

theorem Anderson4D.PartialPairing.assembleCaseThree_isFullyPairedHeadPrefix {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) (σ : PartialPairing (Fin (2 * q))) (τ : PartialPairing (Fin (m + 1 - 2 * q))) (hσ : IsNonSplit σ) : (assembleCaseThree hq σ τ).IsFullyPairedHeadPrefix q

theorem Anderson4D.PartialPairing.assembleCaseThree_headPairedWithPrefix {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) (σ : PartialPairing (Fin (2 * q))) (τ : PartialPairing (Fin (m + 1 - 2 * q))) (hσ : IsNonSplit σ) : (assembleCaseThree hq σ τ).HeadPairedWithPrefix

theorem Anderson4D.PartialPairing.assembleCaseThree_no_smaller {m q : ℕ} (hq : 2 * q ≤ m + 1) (σ : PartialPairing (Fin (2 * q))) (τ : PartialPairing (Fin (m + 1 - 2 * q))) (hσ : IsNonSplit σ) {r : ℕ} (hr : r < q) : ¬(assembleCaseThree hq σ τ).IsFullyPairedHeadPrefix r

Non-splitting of the internal block rules out every smaller fully paired head prefix after assembly.

theorem Anderson4D.PartialPairing.assembleCaseThree_firstQ {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) (σ : PartialPairing (Fin (2 * q))) (τ : PartialPairing (Fin (m + 1 - 2 * q))) (hσ : IsNonSplit σ) : (assembleCaseThree hq σ τ).firstFullyPairedHeadQ ⋯ = q

The first fully paired head prefix of the assembled pairing is exactly the prescribed non-split block.

theorem Anderson4D.PartialPairing.HeadPrefixDecomposition.eq_of_q_eq {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d₁ d₂ : κ.HeadPrefixDecomposition) (h : d₁.q = d₂.q) : d₁ = d₂

Two minimal-prefix decompositions of the same pairing are equal once their numerical prefix orders agree; all remaining fields are propositions.

def Anderson4D.PartialPairing.assembledHeadPrefixDecomposition {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) (σ : PartialPairing (Fin (2 * q))) (τ : PartialPairing (Fin (m + 1 - 2 * q))) (hσ : IsNonSplit σ) : (assembleCaseThree hq σ τ).HeadPrefixDecomposition

The explicit minimal-prefix decomposition of an assembled case-(3) pairing.

Equations

• Anderson4D.PartialPairing.assembledHeadPrefixDecomposition hqpos hq σ τ hσ = { q := q, q_pos := hqpos, two_mul_le := hq, fullyPaired := ⋯, minimal := ⋯ }

def Anderson4D.PartialPairing.assembleCaseThreeSubtype {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) (σ : PartialPairing (Fin (2 * q))) (τ : PartialPairing (Fin (m + 1 - 2 * q))) (hσ : IsNonSplit σ) : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix }

Bundle an assembled pairing in the case-(3) subtype.

Equations

• Anderson4D.PartialPairing.assembleCaseThreeSubtype hqpos hq σ τ hσ = ⟨Anderson4D.PartialPairing.assembleCaseThree hq σ τ, ⋯⟩

@[simp]

theorem Anderson4D.PartialPairing.assembleCaseThreeSubtype_q {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) (σ : PartialPairing (Fin (2 * q))) (τ : PartialPairing (Fin (m + 1 - 2 * q))) (hσ : IsNonSplit σ) : caseThreeQ (assembleCaseThreeSubtype hqpos hq σ τ hσ) = q

theorem Anderson4D.PartialPairing.assembledHeadPrefix_collapse_eq {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) (σ : PartialPairing (Fin (2 * q))) (τ : PartialPairing (Fin (m + 1 - 2 * q))) (hσ : IsNonSplit σ) : (assembledHeadPrefixDecomposition hqpos hq σ τ hσ).collapsePrefixPairing = σ

Restricting the explicit assembled pairing back to its first block recovers the original non-split pairing.

theorem Anderson4D.PartialPairing.caseThreeDecomposition_assemble {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) (σ : PartialPairing (Fin (2 * q))) (τ : PartialPairing (Fin (m + 1 - 2 * q))) (hσ : IsNonSplit σ) : caseThreeDecomposition (assembleCaseThreeSubtype hqpos hq σ τ hσ) = assembledHeadPrefixDecomposition hqpos hq σ τ hσ

The canonical decomposition chosen by caseThreeDecomposition coincides with the explicit assembled decomposition.

Recovering the external remainder

def Anderson4D.PartialPairing.suffixComplOrderIso {N a : ℕ} (ha : a ≤ N) : { i : Fin N // i ∉ {j : Fin N | ↑j < a} } ≃o Fin (N - a)

The complement of the first a consecutive coordinates is order-isomorphic to Fin (N-a) by subtracting a.

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.suffixComplOrderIso_symm_apply_val {N a : ℕ} (ha : a ≤ N) (j : Fin (N - a)) : ↑((suffixComplOrderIso ha).symm j) = suffixFin ha j

theorem Anderson4D.PartialPairing.HeadPrefixDecomposition.remainderOrderIso_eq_suffix {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) : d.remainderOrderIso = suffixComplOrderIso ⋯

For every head-prefix decomposition, the abstract monotone remainder enumeration is the concrete suffix enumeration.

theorem Anderson4D.PartialPairing.HeadPrefixDecomposition.remainderPairing_apply_suffix {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) (j : Fin (m + 1 - 2 * d.q)) : suffixFin ⋯ (d.remainderPairing j) = κ (suffixFin ⋯ j)

The remainder pairing, embedded back after the prefix, agrees with the ambient pairing on every suffix coordinate.

theorem Anderson4D.PartialPairing.assembled_remainderOrderIso_eq {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) (σ : PartialPairing (Fin (2 * q))) (τ : PartialPairing (Fin (m + 1 - 2 * q))) (hσ : IsNonSplit σ) : (assembledHeadPrefixDecomposition hqpos hq σ τ hσ).remainderOrderIso = suffixComplOrderIso hq

The generic monotone complement enumeration used by remainderOrderIso is the concrete suffix enumeration on an assembled head block.

theorem Anderson4D.PartialPairing.assembledHeadPrefix_remainder_eq {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) (σ : PartialPairing (Fin (2 * q))) (τ : PartialPairing (Fin (m + 1 - 2 * q))) (hσ : IsNonSplit σ) : (assembledHeadPrefixDecomposition hqpos hq σ τ hσ).remainderPairing = τ

Restricting the explicit assembled pairing to the suffix recovers the original external remainder pairing.

theorem Anderson4D.PartialPairing.HeadPrefixDecomposition.assemble_collapse_remainder {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) : assembleCaseThree ⋯ d.collapsePrefixPairing d.remainderPairing = κ

Reassembling the collapsed head block and the canonical remainder of an arbitrary head-prefix decomposition recovers the ambient pairing.

The exact fixed-prefix fibre bijection

@[reducible, inline]

abbrev Anderson4D.PartialPairing.CaseThreeAssemblyData (m q : ℕ) : Type

The paper's independent data at a fixed counterterm length 2q: a non-split full head pairing together with an arbitrary tail pairing.

Equations

• Anderson4D.PartialPairing.CaseThreeAssemblyData m q = ({ σ : Anderson4D.PartialPairing (Fin (2 * q)) // Anderson4D.IsNonSplit σ } × Anderson4D.PartialPairing (Fin (m + 1 - 2 * q)))

@[reducible, inline]

abbrev Anderson4D.PartialPairing.CaseThreeFiber (m q : ℕ) : Type

The ambient case-(3) pairings whose least closed head block has length exactly 2q.

Equations

• Anderson4D.PartialPairing.CaseThreeFiber m q = { κ : { κ : Anderson4D.PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix } // Anderson4D.PartialPairing.caseThreeQ κ = q }

def Anderson4D.PartialPairing.caseThreeFiberAssembly {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) : CaseThreeAssemblyData m q → CaseThreeFiber m q

Assemble fixed-q counterterm data as an ambient case-(3) pairing.

Equations

• Anderson4D.PartialPairing.caseThreeFiberAssembly hqpos hq data = ⟨Anderson4D.PartialPairing.assembleCaseThreeSubtype hqpos hq (↑data.1) data.2 ⋯, ⋯⟩

theorem Anderson4D.PartialPairing.caseThreeFiberAssembly_injective {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) : Function.Injective (caseThreeFiberAssembly hqpos hq)

Assembly is injective: the prefix and suffix coordinates can each be read back from the ambient involution.

theorem Anderson4D.PartialPairing.caseThreeFiberAssembly_surjective {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) : Function.Surjective (caseThreeFiberAssembly hqpos hq)

Every ambient pairing in the fixed-q fibre is obtained by assembling its canonical collapsed prefix and remainder.

noncomputable def Anderson4D.PartialPairing.caseThreeFiberEquiv {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) : CaseThreeAssemblyData m q ≃ CaseThreeFiber m q

Exact multiplicity-one correspondence between the paper's (σ₁, σ₂) data and ambient case-(3) pairings at a fixed q.

Equations

• Anderson4D.PartialPairing.caseThreeFiberEquiv hqpos hq = Equiv.ofBijective (Anderson4D.PartialPairing.caseThreeFiberAssembly hqpos hq) ⋯

@[simp]

theorem Anderson4D.PartialPairing.caseThreeFiberEquiv_apply {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) (data : CaseThreeAssemblyData m q) : ↑((caseThreeFiberEquiv hqpos hq) data) = assembleCaseThreeSubtype hqpos hq (↑data.1) data.2 ⋯

theorem Anderson4D.PartialPairing.sum_caseThreeFiber_equiv {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) {R : Type u_1} [AddCommMonoid R] (f : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix } → R) : ∑ K : CaseThreeFiber m q, f ↑K = ∑ data : CaseThreeAssemblyData m q, f (assembleCaseThreeSubtype hqpos hq (↑data.1) data.2 ⋯)

Reindex a sum over the fixed-q ambient fibre by the independent non-split prefix and remainder data, with no multiplicity factor.

theorem Anderson4D.PartialPairing.sum_caseThree_filter_equiv {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) {R : Type u_1} [AddCommMonoid R] (f : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix } → R) : ∑ K : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix } with caseThreeQ K = q, f K = ∑ σ : { σ : PartialPairing (Fin (2 * q)) // IsNonSplit σ }, ∑ τ : PartialPairing (Fin (m + 1 - 2 * q)), f (assembleCaseThreeSubtype hqpos hq (↑σ) τ ⋯)

Filtered form used directly after sum_caseThree_by_q: the fibre filter is exactly the independent prefix--tail product.

Support bookkeeping for the assembled pairing

@[simp]

theorem Anderson4D.PartialPairing.appendPairingTo_prefix_mem_singles {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (i : Fin a) : Fin.castLE ha i ∈ (appendPairingTo ha σ τ).singles ↔ i ∈ σ.singles

@[simp]

theorem Anderson4D.PartialPairing.appendPairingTo_suffix_mem_singles {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (j : Fin (N - a)) : suffixFin ha j ∈ (appendPairingTo ha σ τ).singles ↔ j ∈ τ.singles

@[simp]

theorem Anderson4D.PartialPairing.appendPairingTo_prefix_mem_pairSupport {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (i : Fin a) : Fin.castLE ha i ∈ (appendPairingTo ha σ τ).pairSupport ↔ i ∈ σ.pairSupport

@[simp]

theorem Anderson4D.PartialPairing.appendPairingTo_suffix_mem_pairSupport {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (j : Fin (N - a)) : suffixFin ha j ∈ (appendPairingTo ha σ τ).pairSupport ↔ j ∈ τ.pairSupport

@[simp]

theorem Anderson4D.PartialPairing.appendPairingTo_prefix_lt_apply {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (i : Fin a) : Fin.castLE ha i < (appendPairingTo ha σ τ) (Fin.castLE ha i) ↔ i < σ i

@[simp]

theorem Anderson4D.PartialPairing.appendPairingTo_suffix_lt_apply {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (j : Fin (N - a)) : suffixFin ha j < (appendPairingTo ha σ τ) (suffixFin ha j) ↔ j < τ j

def Anderson4D.PartialPairing.prefixSuffixEquiv {N a : ℕ} (ha : a ≤ N) : Fin a ⊕ Fin (N - a) ≃ Fin N

Consecutive prefix--suffix decomposition of Fin N.

Equations

• Anderson4D.PartialPairing.prefixSuffixEquiv ha = finSumFinEquiv.trans (Fin.castOrderIso ⋯).toEquiv

@[simp]

theorem Anderson4D.PartialPairing.prefixSuffixEquiv_apply_left {N a : ℕ} (ha : a ≤ N) (i : Fin a) : (prefixSuffixEquiv ha) (Sum.inl i) = Fin.castLE ha i

@[simp]

theorem Anderson4D.PartialPairing.prefixSuffixEquiv_apply_right {N a : ℕ} (ha : a ≤ N) (j : Fin (N - a)) : (prefixSuffixEquiv ha) (Sum.inr j) = suffixFin ha j

theorem Anderson4D.PartialPairing.prod_prefix_suffix {N a : ℕ} (ha : a ≤ N) {R : Type u_1} [CommMonoid R] (f : Fin N → R) : ∏ i : Fin N, f i = (∏ i : Fin a, f (Fin.castLE ha i)) * ∏ j : Fin (N - a), f (suffixFin ha j)

Split a product over a finite ordinal into consecutive prefix and suffix products.

theorem Anderson4D.PartialPairing.prod_orientedPairSupport_appendPairingTo {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) {R : Type u_1} [CommMonoid R] (F : Fin N → Fin N → R) : ∏ k ∈ (appendPairingTo ha σ τ).pairSupport with k < (appendPairingTo ha σ τ) k, F k ((appendPairingTo ha σ τ) k) = (∏ i ∈ σ.pairSupport with i < σ i, F (Fin.castLE ha i) (Fin.castLE ha (σ i))) * ∏ j ∈ τ.pairSupport with j < τ j, F (suffixFin ha j) (suffixFin ha (τ j))

Products indexed by oriented pairs split over an appended pairing. This is the covariance-product ledger used by the case-(3) closed form.

def Anderson4D.PartialPairing.appendSinglesEquiv {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (hσ : σ.IsFull) : ↥(appendPairingTo ha σ τ).singles ≃ ↥τ.singles

If the prefix pairing is full, every single of the appended pairing lies uniquely in the suffix.

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.appendSinglesEquiv_symm_apply_val {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (hσ : σ.IsFull) (j : ↥τ.singles) : ↑((appendSinglesEquiv ha σ τ hσ).symm j) = suffixFin ha ↑j

@[simp]

theorem Anderson4D.PartialPairing.appendSinglesEquiv_apply_val {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (hσ : σ.IsFull) (i : ↥(appendPairingTo ha σ τ).singles) : ↑↑((appendSinglesEquiv ha σ τ hσ) i) = ↑↑i - a

theorem Anderson4D.PartialPairing.appendSinglesEquiv_lt_iff {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (hσ : σ.IsFull) (i j : ↥(appendPairingTo ha σ τ).singles) : (appendSinglesEquiv ha σ τ hσ) i < (appendSinglesEquiv ha σ τ hσ) j ↔ i < j

theorem Anderson4D.PartialPairing.wickAt_appendPairingTo (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (hσ : σ.IsFull) (xt : Fin (N + 2) → T4) (yt : Fin (N - a + 2) → T4) (hxt : ∀ (j : Fin (N - a)), xt (varIdx (suffixFin ha j)) = yt (varIdx j)) (ω : M.Ω) : wickAt M ρ ε (appendPairingTo ha σ τ) xt ω = wickAt M ρ ε τ yt ω

With a full appended prefix, the Wick factor is exactly the Wick factor of the suffix pairing. Only the values of the two tuples at suffix variables have to agree.

@[simp]

theorem Anderson4D.PartialPairing.appendPairing_castAdd_mem_singles {a b : ℕ} (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin b)) (i : Fin a) : Fin.castAdd b i ∈ (σ.appendPairing τ).singles ↔ i ∈ σ.singles

@[simp]

theorem Anderson4D.PartialPairing.appendPairing_natAdd_mem_singles {a b : ℕ} (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin b)) (j : Fin b) : Fin.natAdd a j ∈ (σ.appendPairing τ).singles ↔ j ∈ τ.singles

def Anderson4D.PartialPairing.appendPairingSinglesEquiv {a b : ℕ} (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin b)) (hσ : σ.IsFull) : ↥(σ.appendPairing τ).singles ≃ ↥τ.singles

Singles equivalence for the arithmetic-exact appendPairing.

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.appendPairingSinglesEquiv_symm_apply_val {a b : ℕ} (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin b)) (hσ : σ.IsFull) (j : ↥τ.singles) : ↑((σ.appendPairingSinglesEquiv τ hσ).symm j) = Fin.natAdd a ↑j

@[simp]

theorem Anderson4D.PartialPairing.appendPairingSinglesEquiv_apply_val {a b : ℕ} (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin b)) (hσ : σ.IsFull) (i : ↥(σ.appendPairing τ).singles) : ↑↑((σ.appendPairingSinglesEquiv τ hσ) i) = ↑↑i - a

theorem Anderson4D.PartialPairing.appendPairingSinglesEquiv_lt_iff {a b : ℕ} (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin b)) (hσ : σ.IsFull) (i j : ↥(σ.appendPairing τ).singles) : (σ.appendPairingSinglesEquiv τ hσ) i < (σ.appendPairingSinglesEquiv τ hσ) j ↔ i < j

theorem Anderson4D.PartialPairing.wickAt_appendPairing (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {a b : ℕ} (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin b)) (hσ : σ.IsFull) (xt : Fin (a + b + 2) → T4) (yt : Fin (b + 2) → T4) (hxt : ∀ (j : Fin b), xt (varIdx (Fin.natAdd a j)) = yt (varIdx j)) (ω : M.Ω) : wickAt M ρ ε (σ.appendPairing τ) xt ω = wickAt M ρ ε τ yt ω

Direct appendPairing form of wickAt_appendPairingTo.

Spatial tuples for the case-(3) closed-form bridge

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

Ambient internal variables in paper order: (z, u₁, …, u₂q, w, v₁, …, vᵣ).

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.caseThreeAmbientInternal_prefix (q r : ℕ) (z w : T4) (t : Fin (2 * q + r) → T4) (i : Fin (2 * (q + 1))) : caseThreeAmbientInternal q r z w t (Fin.castAdd r i) = detJTupleSucc q z w (fun (k : Fin (2 * q)) => t (Fin.castAdd r k)) i

@[simp]

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

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

The suffix random tuple beginning at w.

Equations

• Anderson4D.PartialPairing.caseThreeTailTuple q r w y t = Anderson4D.assemble w y fun (j : Fin r) => t (Fin.natAdd (2 * q) j)

theorem Anderson4D.PartialPairing.wickAt_caseThreeAmbient (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : σ.IsFull) (x z w y : T4) (t : Fin (2 * q + r) → T4) (ω : M.Ω) : wickAt M ρ ε (σ.appendPairing τ) (assemble x y (caseThreeAmbientInternal q r z w t)) ω = wickAt M ρ ε τ (caseThreeTailTuple q r w y t) ω

Wick factors of a case-(3) assembled pairing are precisely those of the external tail.