The no-prefix paired-head extraction

This module proves the combinatorial fact specific to case (2) of Proposition 3.4: deleting a paired head from a pairing with no fully paired head prefix simply shifts the extraction list. The proof tracks the already removed tail intervals so that a later relative interval starting at the head would reconstruct a forbidden original prefix.

def Anderson4D.PartialPairing.hdRemoved {n : ℕ} (active : Finset (Fin n)) : Finset (Fin (n + 1))

Ambient tail indices which have already been removed from the active state. The head itself is always active.

Equations

• Anderson4D.PartialPairing.hdRemoved active = Finset.univ \ Anderson4D.PartialPairing.hdGlobalActive active

@[simp]

theorem Anderson4D.PartialPairing.not_mem_hdRemoved_zero {n : ℕ} (active : Finset (Fin n)) : 0 ∉ hdRemoved active

@[simp]

theorem Anderson4D.PartialPairing.mem_hdRemoved_succ {n : ℕ} {active : Finset (Fin n)} {i : Fin n} : i.succ ∈ hdRemoved active ↔ i ∉ active

@[simp]

theorem Anderson4D.PartialPairing.hdRemoved_univ {n : ℕ} : hdRemoved Finset.univ = ∅

theorem Anderson4D.PartialPairing.hdRemoved_sdiff_relIcc {n : ℕ} (active : Finset (Fin n)) (l r : Fin n) : hdRemoved (active \ relIcc active l r) = hdRemoved active ∪ relIcc (hdGlobalActive active) l.succ r.succ

Removing a successor interval adds exactly that interval to the ambient removed set.

theorem Anderson4D.PartialPairing.hdRemoved_fullyPaired_sdiff {n : ℕ} {κ : PartialPairing (Fin (n + 1))} {active : Finset (Fin n)} {l r : Fin n} (hremoved : IsFullyPairedOn κ (hdRemoved active)) (hcand : IsRelFullyPaired κ (hdGlobalActive active) l.succ r.succ) : IsFullyPairedOn κ (hdRemoved (active \ relIcc active l r))

A fully paired removed set stays fully paired after one proper tail candidate is extracted.

theorem Anderson4D.PartialPairing.hdMarkedIndex_mem_sdiff {n : ℕ} (d : MarkedSingle (Fin n)) {active : Finset (Fin n)} {l r : Fin n} (hmark : d.index ∈ active) (hcand : IsRelFullyPaired d.pairing active l r) : d.index ∈ active \ relIcc active l r

A fully paired tail candidate cannot remove the marked single created by deleting the head pair.

theorem Anderson4D.PartialPairing.hdRemoved_prefix_fullyPaired {n : ℕ} (κ : PartialPairing (Fin (n + 1))) (hκ : κ 0 ≠ 0) (active : Finset (Fin n)) (hremoved : IsFullyPairedOn κ (hdRemoved active)) (hsep : HdSeparated (κ.headDeletionData hκ) active) (hmark : (κ.headDeletionData hκ).index ∈ active) (r : Fin n) (hr : r ∈ active) : IsFullyPairedOn κ (hdRemoved active ∩ {i : Fin (n + 1) | ↑i ≤ ↑r.succ})

At an active tail boundary, the part of the removed set lying to its left is itself fully paired. Order separation rules out a removed pair straddling that boundary.

theorem Anderson4D.PartialPairing.hdActivePrefix_union_removedPrefix {n : ℕ} (active : Finset (Fin n)) (r : Fin n) : relIcc (hdGlobalActive active) 0 r.succ ∪ hdRemoved active ∩ {i : Fin (n + 1) | ↑i ≤ ↑r.succ} = {i : Fin (n + 1) | ↑i ≤ ↑r.succ}

Active and removed indices partition every prefix whose right endpoint lies in the active tail.

theorem Anderson4D.PartialPairing.hasFullyPairedHeadPrefix_of_fullyPairedPrefix {m : ℕ} (κ : PartialPairing (Fin (m + 1))) (b : Fin (m + 1)) (hfull : IsFullyPairedOn κ {i : Fin (m + 1) | ↑i ≤ ↑b}) : κ.HasFullyPairedHeadPrefix

Any fully paired ordinary prefix has positive even size, hence is one of the paper's headEvenPrefix sets.

theorem Anderson4D.PartialPairing.no_headCandidate_of_noPrefix {n : ℕ} (κ : PartialPairing (Fin (n + 1))) (hκ : κ 0 ≠ 0) (active : Finset (Fin n)) (hnoprefix : ¬κ.HasFullyPairedHeadPrefix) (hremoved : IsFullyPairedOn κ (hdRemoved active)) (hsep : HdSeparated (κ.headDeletionData hκ) active) (hmark : (κ.headDeletionData hκ).index ∈ active) : ¬∃ (b : Fin (n + 1)), IsRelFullyPaired κ (hdGlobalActive active) 0 b

Under the removed-set and separation invariants, a relative candidate beginning at the head would reconstruct an original fully paired head prefix.

theorem Anderson4D.PartialPairing.selectRel_headDeletion_eq_succ_of_no_head {n : ℕ} (κ : PartialPairing (Fin (n + 1))) (hκ : κ 0 ≠ 0) (active : Finset (Fin n)) (hnohead : ¬∃ (b : Fin (n + 1)), IsRelFullyPaired κ (hdGlobalActive active) 0 b) (hg : ∃ (l : Fin (n + 1)) (r : Fin (n + 1)), IsRelFullyPaired κ (hdGlobalActive active) l r) (hl : ∃ (l : Fin n) (r : Fin n), IsRelFullyPaired (κ.headDeletionData hκ).pairing active l r) : selectRel κ (hdGlobalActive active) hg = hdSuccPair (selectRel (κ.headDeletionData hκ).pairing active hl)

If no relative candidate begins at the head, the deterministic selector commutes exactly with deleting that head.

theorem Anderson4D.PartialPairing.no_globalCandidate_of_no_head_no_tail {n : ℕ} (κ : PartialPairing (Fin (n + 1))) (hκ : κ 0 ≠ 0) (active : Finset (Fin n)) (hnohead : ¬∃ (b : Fin (n + 1)), IsRelFullyPaired κ (hdGlobalActive active) 0 b) (hnotail : ¬∃ (l : Fin n) (r : Fin n), IsRelFullyPaired (κ.headDeletionData hκ).pairing active l r) : ¬∃ (l : Fin (n + 1)) (r : Fin (n + 1)), IsRelFullyPaired κ (hdGlobalActive active) l r

With neither a head candidate nor a tail candidate, the ambient head-extended state has no candidate at all.

Exact no-prefix extraction recursion

theorem Anderson4D.PartialPairing.extractAux_headDeletion_noPrefix_state {n : ℕ} (κ : PartialPairing (Fin (n + 1))) (hκ : κ 0 ≠ 0) (hnoprefix : ¬κ.HasFullyPairedHeadPrefix) (fuel : ℕ) (active : Finset (Fin n)) : active.card ≤ 2 * fuel + 1 → IsFullyPairedOn κ (hdRemoved active) → HdSeparated (κ.headDeletionData hκ) active → (κ.headDeletionData hκ).index ∈ active → extractAux κ (fuel + 1) (hdGlobalActive active) = List.map hdSuccPair (extractAux (κ.headDeletionData hκ).pairing fuel active)

State-level recursion for case (2). The removed-set invariant is what rules out a relative head interval after earlier tail intervals have been extracted.

theorem Anderson4D.PartialPairing.extract_headDeletion_noPrefix {n : ℕ} (κ : PartialPairing (Fin (n + 1))) (hκ : κ 0 ≠ 0) (hnoprefix : ¬κ.HasFullyPairedHeadPrefix) : extract κ = List.map hdSuccPair (extract (κ.headDeletionData hκ).pairing)

Public extraction theorem for a paired head with no fully paired head prefix: head deletion only shifts the old extraction list.

theorem Anderson4D.PartialPairing.headDeletionData_wickHeadEquiv {n : ℕ} (d : MarkedSingle (Fin n)) (hκ : ((wickHeadEquiv n) (Sum.inr d)) 0 ≠ 0) : ((wickHeadEquiv n) (Sum.inr d)).headDeletionData hκ = d

Deleting a head which was introduced from marked-single data recovers that data exactly.

theorem Anderson4D.PartialPairing.contractionExtractCompatible_of_headPairedNoPrefix {n : ℕ} (d : MarkedSingle (Fin n)) (hcase : ((wickHeadEquiv n) (Sum.inr d)).HeadPairedNoPrefix) : ContractionExtractCompatible d

The no-prefix head class implies the exact extraction compatibility used by the analytic case-(2) factorization.

def Anderson4D.PartialPairing.noPrefixMarkedEquiv (n : ℕ) : { d : MarkedSingle (Fin n) // ((wickHeadEquiv n) (Sum.inr d)).HeadPairedNoPrefix } ≃ { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedNoPrefix }

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

Equations

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

theorem Anderson4D.PartialPairing.sum_headPairedNoPrefixContribution_eq_randRI (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) (hint : ∀ (d : { d : MarkedSingle (Fin n) // ((wickHeadEquiv n) (Sum.inr d)).HeadPairedNoPrefix }), 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)) : ∑ d : { d : MarkedSingle (Fin n) // ((wickHeadEquiv n) (Sum.inr d)).HeadPairedNoPrefix }, headPairedContractionContribution M ρ lam ε n (↑d) x y ω = ∑ κ : { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedNoPrefix }, randRI M ρ lam ε (n + 1) (↑κ) x y ω

Summed case (2) of Proposition 3.4. Every marked contraction with no fully paired head prefix is integrated and reindexed to the corresponding paper pairing with multiplicity one.