Extraction compatibility for consecutive pairing blocks.

This file proves that the relative smallest-leftmost extraction algorithm acts independently on two consecutive closed pairing blocks, up to the interleaving order recorded by List.Perm.

def Anderson4D.PartialPairing.eaPrefixEmbedding {N a : ℕ} (ha : a ≤ N) : Fin a ↪ Fin N

Equations

• Anderson4D.PartialPairing.eaPrefixEmbedding ha = { toFun := Fin.castLE ha, inj' := ⋯ }

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

Equations

• Anderson4D.PartialPairing.eaSuffixEmbedding ha = { toFun := Anderson4D.PartialPairing.suffixFin ha, inj' := ⋯ }

def Anderson4D.PartialPairing.eaPrefixPair {N a : ℕ} (ha : a ≤ N) (p : Fin a × Fin a) : Fin N × Fin N

Equations

• Anderson4D.PartialPairing.eaPrefixPair ha p = (Fin.castLE ha p.1, Fin.castLE ha p.2)

def Anderson4D.PartialPairing.eaSuffixPair {N a : ℕ} (ha : a ≤ N) (p : Fin (N - a) × Fin (N - a)) : Fin N × Fin N

Equations

• Anderson4D.PartialPairing.eaSuffixPair ha p = (Anderson4D.PartialPairing.suffixFin ha p.1, Anderson4D.PartialPairing.suffixFin ha p.2)

def Anderson4D.PartialPairing.eaPrefixActive {N a : ℕ} (ha : a ≤ N) (active : Finset (Fin N)) : Finset (Fin a)

Equations

• Anderson4D.PartialPairing.eaPrefixActive ha active = {i : Fin a | Fin.castLE ha i ∈ active}

def Anderson4D.PartialPairing.eaSuffixActive {N a : ℕ} (ha : a ≤ N) (active : Finset (Fin N)) : Finset (Fin (N - a))

Equations

• Anderson4D.PartialPairing.eaSuffixActive ha active = {j : Fin (N - a) | Anderson4D.PartialPairing.suffixFin ha j ∈ active}

@[simp]

theorem Anderson4D.PartialPairing.mem_eaPrefixActive {N a : ℕ} (ha : a ≤ N) {active : Finset (Fin N)} {i : Fin a} : i ∈ eaPrefixActive ha active ↔ Fin.castLE ha i ∈ active

@[simp]

theorem Anderson4D.PartialPairing.mem_eaSuffixActive {N a : ℕ} (ha : a ≤ N) {active : Finset (Fin N)} {j : Fin (N - a)} : j ∈ eaSuffixActive ha active ↔ suffixFin ha j ∈ active

theorem Anderson4D.PartialPairing.eaPrefixActive_relIcc_prefix {N a : ℕ} (ha : a ≤ N) (active : Finset (Fin N)) (l r : Fin a) : eaPrefixActive ha (relIcc active (Fin.castLE ha l) (Fin.castLE ha r)) = relIcc (eaPrefixActive ha active) l r

theorem Anderson4D.PartialPairing.relIcc_prefix_eq_map {N a : ℕ} (ha : a ≤ N) (active : Finset (Fin N)) (l r : Fin a) : relIcc active (Fin.castLE ha l) (Fin.castLE ha r) = Finset.map (eaPrefixEmbedding ha) (relIcc (eaPrefixActive ha active) l r)

theorem Anderson4D.PartialPairing.card_relIcc_prefix {N a : ℕ} (ha : a ≤ N) (active : Finset (Fin N)) (l r : Fin a) : (relIcc active (Fin.castLE ha l) (Fin.castLE ha r)).card = (relIcc (eaPrefixActive ha active) l r).card

@[simp]

theorem Anderson4D.PartialPairing.mem_relIcc_prefix_iff {N a : ℕ} (ha : a ≤ N) {active : Finset (Fin N)} (l r i : Fin a) : Fin.castLE ha i ∈ relIcc active (Fin.castLE ha l) (Fin.castLE ha r) ↔ i ∈ relIcc (eaPrefixActive ha active) l r

theorem Anderson4D.PartialPairing.eaSuffixActive_relIcc_suffix {N a : ℕ} (ha : a ≤ N) (active : Finset (Fin N)) (l r : Fin (N - a)) : eaSuffixActive ha (relIcc active (suffixFin ha l) (suffixFin ha r)) = relIcc (eaSuffixActive ha active) l r

theorem Anderson4D.PartialPairing.relIcc_suffix_eq_map {N a : ℕ} (ha : a ≤ N) (active : Finset (Fin N)) (l r : Fin (N - a)) : relIcc active (suffixFin ha l) (suffixFin ha r) = Finset.map (eaSuffixEmbedding ha) (relIcc (eaSuffixActive ha active) l r)

theorem Anderson4D.PartialPairing.card_relIcc_suffix {N a : ℕ} (ha : a ≤ N) (active : Finset (Fin N)) (l r : Fin (N - a)) : (relIcc active (suffixFin ha l) (suffixFin ha r)).card = (relIcc (eaSuffixActive ha active) l r).card

@[simp]

theorem Anderson4D.PartialPairing.mem_relIcc_suffix_iff {N a : ℕ} (ha : a ≤ N) {active : Finset (Fin N)} (l r i : Fin (N - a)) : suffixFin ha i ∈ relIcc active (suffixFin ha l) (suffixFin ha r) ↔ i ∈ relIcc (eaSuffixActive ha active) l r

theorem Anderson4D.PartialPairing.isRelFullyPaired_append_prefix_iff {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (active : Finset (Fin N)) (l r : Fin a) : IsRelFullyPaired (appendPairingTo ha σ τ) active (Fin.castLE ha l) (Fin.castLE ha r) ↔ IsRelFullyPaired σ (eaPrefixActive ha active) l r

theorem Anderson4D.PartialPairing.isRelFullyPaired_append_suffix_iff {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (active : Finset (Fin N)) (l r : Fin (N - a)) : IsRelFullyPaired (appendPairingTo ha σ τ) active (suffixFin ha l) (suffixFin ha r) ↔ IsRelFullyPaired τ (eaSuffixActive ha active) l r

theorem Anderson4D.PartialPairing.eaPrefixActive_sdiff_prefix {N a : ℕ} (ha : a ≤ N) (active : Finset (Fin N)) (l r : Fin a) : eaPrefixActive ha (active \ relIcc active (Fin.castLE ha l) (Fin.castLE ha r)) = eaPrefixActive ha active \ relIcc (eaPrefixActive ha active) l r

theorem Anderson4D.PartialPairing.eaSuffixActive_sdiff_prefix {N a : ℕ} (ha : a ≤ N) (active : Finset (Fin N)) (l r : Fin a) : eaSuffixActive ha (active \ relIcc active (Fin.castLE ha l) (Fin.castLE ha r)) = eaSuffixActive ha active

theorem Anderson4D.PartialPairing.eaPrefixActive_sdiff_suffix {N a : ℕ} (ha : a ≤ N) (active : Finset (Fin N)) (l r : Fin (N - a)) : eaPrefixActive ha (active \ relIcc active (suffixFin ha l) (suffixFin ha r)) = eaPrefixActive ha active

theorem Anderson4D.PartialPairing.eaSuffixActive_sdiff_suffix {N a : ℕ} (ha : a ≤ N) (active : Finset (Fin N)) (l r : Fin (N - a)) : eaSuffixActive ha (active \ relIcc active (suffixFin ha l) (suffixFin ha r)) = eaSuffixActive ha active \ relIcc (eaSuffixActive ha active) l r

theorem Anderson4D.PartialPairing.selectRel_appendPairingTo_either {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (active : Finset (Fin N)) (h : ∃ (l : Fin N) (r : Fin N), IsRelFullyPaired (appendPairingTo ha σ τ) active l r) : (∃ (l : Fin a) (r : Fin a), selectRel (appendPairingTo ha σ τ) active h = eaPrefixPair ha (l, r)) ∨ ∃ (l : Fin (N - a)) (r : Fin (N - a)), selectRel (appendPairingTo ha σ τ) active h = eaSuffixPair ha (l, r)

The global selector of a block-diagonal pairing never crosses the block boundary.

theorem Anderson4D.PartialPairing.selectRel_appendPairingTo_eq_prefix {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (active : Finset (Fin N)) (h : ∃ (l : Fin N) (r : Fin N), IsRelFullyPaired (appendPairingTo ha σ τ) active l r) (l r : Fin a) (hpref : selectRel (appendPairingTo ha σ τ) active h = eaPrefixPair ha (l, r)) : have hlocal := ⋯; selectRel (appendPairingTo ha σ τ) active h = eaPrefixPair ha (selectRel σ (eaPrefixActive ha active) hlocal)

If the global selector is in the prefix block, it is exactly the embedded selector of the projected prefix state.

theorem Anderson4D.PartialPairing.selectRel_appendPairingTo_eq_suffix {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (active : Finset (Fin N)) (h : ∃ (l : Fin N) (r : Fin N), IsRelFullyPaired (appendPairingTo ha σ τ) active l r) (l r : Fin (N - a)) (hsuff : selectRel (appendPairingTo ha σ τ) active h = eaSuffixPair ha (l, r)) : have hlocal := ⋯; selectRel (appendPairingTo ha σ τ) active h = eaSuffixPair ha (selectRel τ (eaSuffixActive ha active) hlocal)

Suffix analogue of selectRel_appendPairingTo_eq_prefix.

theorem Anderson4D.PartialPairing.extractAux_appendPairingTo_perm_state {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (fuel fa fb : ℕ) (active : Finset (Fin N)) : fa + fb = fuel → (eaPrefixActive ha active).card ≤ 2 * fa + 1 → (eaSuffixActive ha active).card ≤ 2 * fb + 1 → (extractAux (appendPairingTo ha σ τ) fuel active).Perm (List.map (eaPrefixPair ha) (extractAux σ fa (eaPrefixActive ha active)) ++ List.map (eaSuffixPair ha) (extractAux τ fb (eaSuffixActive ha active)))

Stateful/fuel form of extraction compatibility. The global fuel is split between the two projected active blocks; the cardinality bounds are exactly what guarantees that a block with a candidate still has positive fuel.

theorem Anderson4D.PartialPairing.extract_appendPairingTo_perm {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) : (extract (appendPairingTo ha σ τ)).Perm (List.map (eaPrefixPair ha) (extract σ) ++ List.map (eaSuffixPair ha) (extract τ))

Extraction of a consecutive block sum is the shuffle of the two local extractions. No non-split hypothesis is needed.

Closed-form component bookkeeping

theorem Anderson4D.PartialPairing.extractedRightValues_appendPairingTo_perm {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) : (List.map (fun (p : Fin N × Fin N) => ↑p.2 + 1) (extract (appendPairingTo ha σ τ))).Perm (List.map (fun (p : Fin a × Fin a) => ↑p.2 + 1) (extract σ) ++ List.map (fun (p : Fin (N - a) × Fin (N - a)) => a + ↑p.2 + 1) (extract τ))

Right chain-edge numbers extracted from an appended pairing split into the corresponding prefix and suffix numbers.

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

The prefix variables of an ambient deterministic tuple, with the external left slot omitted.

Equations

• Anderson4D.PartialPairing.ambientPrefixTuple ha xt i = xt (Anderson4D.varIdx (Fin.castLE ha i))

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

The tail tuple starts at the last prefix variable: its slot 0 is ambient slot a, its internal variables are the ambient suffix, and its last slot is the ambient right endpoint.

Equations

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

def Anderson4D.PartialPairing.wholePrefixPair {a : ℕ} (ha0 : 0 < a) : Fin a × Fin a

The endpoints of the whole nonempty prefix.

Equations

• Anderson4D.PartialPairing.wholePrefixPair ha0 = (⟨0, ha0⟩, ⟨a - 1, ⋯⟩)

@[simp]

theorem Anderson4D.PartialPairing.ambientTailTuple_varIdx {N a : ℕ} (ha : a ≤ N) (xt : Fin (N + 2) → T4) (j : Fin (N - a)) : ambientTailTuple ha xt (varIdx j) = xt (varIdx (suffixFin ha j))

@[simp]

theorem Anderson4D.PartialPairing.ambientTailTuple_after_internal {N a : ℕ} (ha : a ≤ N) (xt : Fin (N + 2) → T4) (j : Fin (N - a)) : ambientTailTuple ha xt ⟨↑j + 2, ⋯⟩ = xt ⟨↑(suffixFin ha j) + 2, ⋯⟩

@[simp]

theorem Anderson4D.PartialPairing.ambientPrefixTuple_apply {N a : ℕ} (ha : a ≤ N) (xt : Fin (N + 2) → T4) (i : Fin a) : ambientPrefixTuple ha xt i = xt (varIdx (Fin.castLE ha i))

theorem Anderson4D.PartialPairing.covarianceProduct_appendPairingTo (ρ : SmoothCutoff) (ε : ℝ) {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (xt : Fin (N + 2) → T4) : ∏ k ∈ (appendPairingTo ha σ τ).pairSupport with k < (appendPairingTo ha σ τ) k, ρ.etaEpsT4 ε (xt (varIdx k) - xt (varIdx ((appendPairingTo ha σ τ) k))) = (∏ i ∈ σ.pairSupport with i < σ i, ρ.etaEpsT4 ε (ambientPrefixTuple ha xt i - ambientPrefixTuple ha xt (σ i))) * ∏ j ∈ τ.pairSupport with j < τ j, ρ.etaEpsT4 ε (ambientTailTuple ha xt (varIdx j) - ambientTailTuple ha xt (varIdx (τ j)))

The covariance part of the ambient closed form is the product of its prefix and tail covariance parts.

theorem Anderson4D.PartialPairing.wickAt_appendPairingTo_ambientTuple (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (hσ : σ.IsFull) (xt : Fin (N + 2) → T4) (ω : M.Ω) : wickAt M ρ ε (appendPairingTo ha σ τ) xt ω = wickAt M ρ ε τ (ambientTailTuple ha xt) ω

The Wick factor of an appended pairing is carried entirely by the tail whenever the prefix is full.

theorem Anderson4D.PartialPairing.diffFactor_eaSuffixPair {N a : ℕ} (ha : a ≤ N) (xt : Fin (N + 2) → T4) (p : Fin (N - a) × Fin (N - a)) : diffFactor xt (eaSuffixPair ha p) = diffFactor (ambientTailTuple ha xt) p

Difference factors of a suffix extraction are exactly the tail detIntegrand difference factors.

theorem Anderson4D.PartialPairing.diffFactor_eaPrefixPair {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 (ambientPrefixTuple ha xt) p

Before the last prefix coordinate, ambient prefix differences are the J-integrand differences.

theorem Anderson4D.PartialPairing.differenceProduct_appendPairingTo {N a : ℕ} (ha : a ≤ N) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (xt : Fin (N + 2) → T4) : (List.map (diffFactor xt) (extract (appendPairingTo ha σ τ))).prod = (List.map (fun (p : Fin a × Fin a) => diffFactor xt (eaPrefixPair ha p)) (extract σ)).prod * (List.map (diffFactor (ambientTailTuple ha xt)) (extract τ)).prod

The ambient difference-factor list is the product of the prefix factors and the tail factors.

theorem Anderson4D.PartialPairing.diffFactor_eaPrefixPair_whole {N a : ℕ} (ha : a ≤ N) (ha0 : 0 < a) (xt : Fin (N + 2) → T4) : diffFactor xt (eaPrefixPair ha (wholePrefixPair ha0)) = greenFn (ambientTailTuple ha xt 0 - ambientTailTuple ha xt 1) - greenFn (ambientPrefixTuple ha xt ⟨0, ha0⟩ - ambientTailTuple ha xt 1)

The whole-prefix extraction supplies the boundary Green difference between the last prefix point and the first prefix point.

@[simp]

theorem Anderson4D.PartialPairing.diffFactorJ_wholePrefixPair {a : ℕ} (ha0 : 0 < a) (xt : Fin a → T4) : diffFactorJ xt (wholePrefixPair ha0) = 1

theorem Anderson4D.PartialPairing.prefixDifferenceProduct_eq_detJ_mul_boundary {N a : ℕ} (ha : a ≤ N) (ha0 : 0 < a) (σ : PartialPairing (Fin a)) (xt : Fin (N + 2) → T4) (proper : List (Fin a × Fin a)) (hextract : (extract σ).Perm (proper ++ [wholePrefixPair ha0])) (hproper : ∀ p ∈ proper, ↑p.2 + 1 < a) : (List.map (fun (p : Fin a × Fin a) => diffFactor xt (eaPrefixPair ha p)) (extract σ)).prod = (List.map (diffFactorJ (ambientPrefixTuple ha xt)) (extract σ)).prod * (greenFn (ambientTailTuple ha xt 0 - ambientTailTuple ha xt 1) - greenFn (ambientPrefixTuple ha xt ⟨0, ha0⟩ - ambientTailTuple ha xt 1))

If the whole prefix is the final extraction, its ambient difference product is the internal J difference product followed by the one boundary Green difference.

Isolating the first tail edge

noncomputable def Anderson4D.PartialPairing.detIntegrandAfterFirst (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) : ℝ

All deterministic factors of detIntegrand except its first chain edge. Extracted edges are always numbered r+1, so edge zero is never removed.

Equations

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

theorem Anderson4D.PartialPairing.detIntegrand_eq_first_mul_afterFirst (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) : detIntegrand ρ ε m κ xt = greenFn (xt 0 - xt 1) * detIntegrandAfterFirst ρ ε m κ xt

detIntegrand is its unavoidable first Green edge times the remaining deterministic factors.

def Anderson4D.PartialPairing.setTupleFirst {m : ℕ} (z : T4) (xt : Fin (m + 2) → T4) : Fin (m + 2) → T4

Change only slot zero of a tuple.

Equations

• Anderson4D.PartialPairing.setTupleFirst z xt j = if ↑j = 0 then z else xt j

@[simp]

theorem Anderson4D.PartialPairing.setTupleFirst_zero {m : ℕ} (z : T4) (xt : Fin (m + 2) → T4) : setTupleFirst z xt 0 = z

@[simp]

theorem Anderson4D.PartialPairing.setTupleFirst_of_ne_zero {m : ℕ} (z : T4) (xt : Fin (m + 2) → T4) (j : Fin (m + 2)) (hj : ↑j ≠ 0) : setTupleFirst z xt j = xt j

@[simp]

theorem Anderson4D.PartialPairing.setTupleFirst_varIdx {m : ℕ} (z : T4) (xt : Fin (m + 2) → T4) (i : Fin m) : setTupleFirst z xt (varIdx i) = xt (varIdx i)

@[simp]

theorem Anderson4D.PartialPairing.setTupleFirst_after_internal {m : ℕ} (z : T4) (xt : Fin (m + 2) → T4) (i : Fin m) : setTupleFirst z xt ⟨↑i + 2, ⋯⟩ = xt ⟨↑i + 2, ⋯⟩

theorem Anderson4D.PartialPairing.detIntegrandAfterFirst_setTupleFirst (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (z : T4) (xt : Fin (m + 2) → T4) : detIntegrandAfterFirst ρ ε m κ (setTupleFirst z xt) = detIntegrandAfterFirst ρ ε m κ xt

None of the factors after the first chain edge sees tuple slot zero.

theorem Anderson4D.PartialPairing.wickAt_setTupleFirst (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (κ : PartialPairing (Fin m)) (z : T4) (xt : Fin (m + 2) → T4) (ω : M.Ω) : wickAt M ρ ε κ (setTupleFirst z xt) ω = wickAt M ρ ε κ xt ω

wickAt depends only on internal-variable slots.

theorem Anderson4D.PartialPairing.randIntegrand_eq_first_mul_afterFirst (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) (ω : M.Ω) : randIntegrand M ρ ε κ xt ω = greenFn (xt 0 - xt 1) * (detIntegrandAfterFirst ρ ε m κ xt * wickAt M ρ ε κ xt ω)

The random integrand also has an explicit unavoidable first edge.

theorem Anderson4D.PartialPairing.randIntegrand_sub_setTupleFirst (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (κ : PartialPairing (Fin m)) (z : T4) (xt : Fin (m + 2) → T4) (ω : M.Ω) : randIntegrand M ρ ε κ xt ω - randIntegrand M ρ ε κ (setTupleFirst z xt) ω = (greenFn (xt 0 - xt 1) - greenFn (z - xt 1)) * (detIntegrandAfterFirst ρ ε m κ xt * wickAt M ρ ε κ xt ω)

Replacing the left endpoint turns subtraction of random integrands into exactly one Green-kernel difference.

@[simp]

theorem Anderson4D.PartialPairing.hd_wickHeadEquiv_contraction_zero {n : ℕ} (d : MarkedSingle (Fin n)) : ((wickHeadEquiv n) (Sum.inr d)) 0 = d.index.succ

@[simp]

theorem Anderson4D.PartialPairing.hd_wickHeadEquiv_contraction_partner {n : ℕ} (d : MarkedSingle (Fin n)) : ((wickHeadEquiv n) (Sum.inr d)) d.index.succ = 0

@[simp]

theorem Anderson4D.PartialPairing.hd_wickHeadEquiv_contraction_succ_ne {n : ℕ} (d : MarkedSingle (Fin n)) (i : Fin n) (hi : i ≠ d.index) : ((wickHeadEquiv n) (Sum.inr d)) i.succ = (d.pairing i).succ

def Anderson4D.PartialPairing.headDeletionData {n : ℕ} (κ : PartialPairing (Fin (n + 1))) (hκ : κ 0 ≠ 0) : MarkedSingle (Fin n)

Pairing obtained by deleting a paired head and restoring its partner as a single.

Equations

• κ.headDeletionData hκ = (Anderson4D.PartialPairing.contractionHeadEquiv n).symm ⟨κ, hκ⟩

@[simp]

theorem Anderson4D.PartialPairing.contractionHeadEquiv_headDeletionData {n : ℕ} (κ : PartialPairing (Fin (n + 1))) (hκ : κ 0 ≠ 0) : ↑((contractionHeadEquiv n) (κ.headDeletionData hκ)) = κ

theorem Anderson4D.PartialPairing.headDeletionData_zero {n : ℕ} (κ : PartialPairing (Fin (n + 1))) (hκ : κ 0 ≠ 0) : κ 0 = (κ.headDeletionData hκ).index.succ

theorem Anderson4D.PartialPairing.headDeletionData_partner {n : ℕ} (κ : PartialPairing (Fin (n + 1))) (hκ : κ 0 ≠ 0) : κ (κ.headDeletionData hκ).index.succ = 0

theorem Anderson4D.PartialPairing.headDeletionData_succ_ne {n : ℕ} (κ : PartialPairing (Fin (n + 1))) (hκ : κ 0 ≠ 0) (i : Fin n) (hi : i ≠ (κ.headDeletionData hκ).index) : κ i.succ = ((κ.headDeletionData hκ).pairing i).succ

The successor copy of the head-deleted active state

def Anderson4D.PartialPairing.hdSuccEmbedding {n : ℕ} : Fin n ↪ Fin (n + 1)

Equations

• Anderson4D.PartialPairing.hdSuccEmbedding = { toFun := Fin.succ, inj' := ⋯ }

def Anderson4D.PartialPairing.hdSuccPair {n : ℕ} (p : Fin n × Fin n) : Fin (n + 1) × Fin (n + 1)

Equations

• Anderson4D.PartialPairing.hdSuccPair p = (p.1.succ, p.2.succ)

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

Equations

• Anderson4D.PartialPairing.hdTailActive active = {i : Fin n | i.succ ∈ active}

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

Equations

• Anderson4D.PartialPairing.hdGlobalActive active = insert 0 (Finset.map Anderson4D.PartialPairing.hdSuccEmbedding active)

@[simp]

theorem Anderson4D.PartialPairing.mem_hdTailActive {n : ℕ} {active : Finset (Fin (n + 1))} {i : Fin n} : i ∈ hdTailActive active ↔ i.succ ∈ active

@[simp]

theorem Anderson4D.PartialPairing.mem_hdGlobalActive_zero {n : ℕ} (active : Finset (Fin n)) : 0 ∈ hdGlobalActive active

@[simp]

theorem Anderson4D.PartialPairing.mem_hdGlobalActive_succ {n : ℕ} {active : Finset (Fin n)} {i : Fin n} : i.succ ∈ hdGlobalActive active ↔ i ∈ active

@[simp]

theorem Anderson4D.PartialPairing.hdTailActive_hdGlobalActive {n : ℕ} (active : Finset (Fin n)) : hdTailActive (hdGlobalActive active) = active

theorem Anderson4D.PartialPairing.hdGlobalActive_univ {n : ℕ} : hdGlobalActive Finset.univ = Finset.univ

@[simp]

theorem Anderson4D.PartialPairing.mem_relIcc_hd_succ_iff {n : ℕ} {active : Finset (Fin n)} (l r i : Fin n) : i.succ ∈ relIcc (hdGlobalActive active) l.succ r.succ ↔ i ∈ relIcc active l r

theorem Anderson4D.PartialPairing.relIcc_hd_succ_eq_map {n : ℕ} (active : Finset (Fin n)) (l r : Fin n) : relIcc (hdGlobalActive active) l.succ r.succ = Finset.map hdSuccEmbedding (relIcc active l r)

theorem Anderson4D.PartialPairing.card_relIcc_hd_succ {n : ℕ} (active : Finset (Fin n)) (l r : Fin n) : (relIcc (hdGlobalActive active) l.succ r.succ).card = (relIcc active l r).card

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

Proper candidates agree under head deletion

theorem Anderson4D.PartialPairing.isRelFullyPaired_headDeletion_succ_iff {n : ℕ} (κ : PartialPairing (Fin (n + 1))) (hκ : κ 0 ≠ 0) (active : Finset (Fin n)) (l r : Fin n) : IsRelFullyPaired κ (hdGlobalActive active) l.succ r.succ ↔ IsRelFullyPaired (κ.headDeletionData hκ).pairing active l r

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

The order-separation invariant of already removed pairs

def Anderson4D.PartialPairing.HdSeparated {n : ℕ} (d : MarkedSingle (Fin n)) (active : Finset (Fin n)) : Prop

Every pair already removed from active lies entirely in one gap of the remaining order: it cannot straddle an active index.

Equations

• Anderson4D.PartialPairing.HdSeparated d active = ∀ i ∉ active, ∀ j ∈ active, ¬(i ≤ j ∧ j ≤ d.pairing i ∨ d.pairing i ≤ j ∧ j ≤ i)

theorem Anderson4D.PartialPairing.hdSeparated_univ {n : ℕ} (d : MarkedSingle (Fin n)) : HdSeparated d Finset.univ

theorem Anderson4D.PartialPairing.hdSeparated_sdiff_relIcc {n : ℕ} {d : MarkedSingle (Fin n)} {active : Finset (Fin n)} {l r : Fin n} (hsep : HdSeparated d active) (hfull : IsFullyPairedOn d.pairing (relIcc active l r)) : HdSeparated d (active \ relIcc active l r)

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

The ambient active state stays fully paired when a successor candidate is removed.

Non-splitting rules out a proper relative head prefix

def Anderson4D.PartialPairing.HdNonSplit {n : ℕ} (κ : PartialPairing (Fin (n + 1))) : Prop

General-size version of the paper's non-concatenation condition.

Equations

• κ.HdNonSplit = (κ.IsFull ∧ ¬∃ p ∈ Finset.range (n + 1), p + 1 < n + 1 ∧ Anderson4D.IsFullyPairedOn κ {i : Fin (n + 1) | ↑i ≤ p})

theorem Anderson4D.PartialPairing.hdMarkedIndex_mem {n : ℕ} {κ : PartialPairing (Fin (n + 1))} {active : Finset (Fin n)} (hκ : κ 0 ≠ 0) (hglobal : IsFullyPairedOn κ (hdGlobalActive active)) : (κ.headDeletionData hκ).index ∈ active

theorem Anderson4D.PartialPairing.hdPrefix_fullyPaired_of_head_candidate {n : ℕ} {κ : PartialPairing (Fin (n + 1))} {active : Finset (Fin n)} (hκ : κ 0 ≠ 0) (hfull : κ.IsFull) (hglobal : IsFullyPairedOn κ (hdGlobalActive active)) (hsep : HdSeparated (κ.headDeletionData hκ) active) {b : Fin (n + 1)} (hcand : IsRelFullyPaired κ (hdGlobalActive active) 0 b) : IsFullyPairedOn κ {i : Fin (n + 1) | ↑i ≤ ↑b}

theorem Anderson4D.PartialPairing.hdHeadCandidate_right_eq_last {n : ℕ} {κ : PartialPairing (Fin (n + 1))} {active : Finset (Fin n)} (hκ : κ 0 ≠ 0) (hns : κ.HdNonSplit) (hglobal : IsFullyPairedOn κ (hdGlobalActive active)) (hsep : HdSeparated (κ.headDeletionData hκ) active) {b : Fin (n + 1)} (hcand : IsRelFullyPaired κ (hdGlobalActive active) 0 b) : b = Fin.last n

theorem Anderson4D.PartialPairing.relIcc_hdGlobal_zero_last {n : ℕ} (active : Finset (Fin n)) : relIcc (hdGlobalActive active) 0 (Fin.last n) = hdGlobalActive active

theorem Anderson4D.PartialPairing.card_hdGlobalActive {n : ℕ} (active : Finset (Fin n)) : (hdGlobalActive active).card = active.card + 1

Selector compatibility before the terminal head extraction

theorem Anderson4D.PartialPairing.selectRel_headDeletion_eq_succ {n : ℕ} (κ : PartialPairing (Fin (n + 1))) (hκ : κ 0 ≠ 0) (active : Finset (Fin n)) (hns : κ.HdNonSplit) (hglobal : IsFullyPairedOn κ (hdGlobalActive active)) (hsep : HdSeparated (κ.headDeletionData hκ) active) (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)

theorem Anderson4D.PartialPairing.hdWholeCandidate {n : ℕ} {κ : PartialPairing (Fin (n + 1))} {active : Finset (Fin n)} (hκ : κ 0 ≠ 0) (hns : κ.HdNonSplit) (hglobal : IsFullyPairedOn κ (hdGlobalActive active)) (hsep : HdSeparated (κ.headDeletionData hκ) active) : IsRelFullyPaired κ (hdGlobalActive active) 0 (Fin.last n)

theorem Anderson4D.PartialPairing.selectRel_headDeletion_terminal {n : ℕ} (κ : PartialPairing (Fin (n + 1))) (hκ : κ 0 ≠ 0) (active : Finset (Fin n)) (hns : κ.HdNonSplit) (hglobal : IsFullyPairedOn κ (hdGlobalActive active)) (hsep : HdSeparated (κ.headDeletionData hκ) active) (hl : ¬∃ (l : Fin n) (r : Fin n), IsRelFullyPaired (κ.headDeletionData hκ).pairing active l r) : have hg := ⋯; selectRel κ (hdGlobalActive active) hg = (0, Fin.last n)

Exact recursion and public extraction theorem

theorem Anderson4D.PartialPairing.extractAux_headDeletion_exact_state {n : ℕ} (κ : PartialPairing (Fin (n + 1))) (hκ : κ 0 ≠ 0) (hns : κ.HdNonSplit) (fuel : ℕ) (active : Finset (Fin n)) : active.card ≤ 2 * fuel + 1 → IsFullyPairedOn κ (hdGlobalActive active) → HdSeparated (κ.headDeletionData hκ) active → extractAux κ (fuel + 1) (hdGlobalActive active) = List.map hdSuccPair (extractAux (κ.headDeletionData hκ).pairing fuel active) ++ [(0, Fin.last n)]

theorem Anderson4D.PartialPairing.extract_headDeletion_exact {n : ℕ} (κ : PartialPairing (Fin (n + 1))) (hκ : κ 0 ≠ 0) (hns : κ.HdNonSplit) : extract κ = List.map hdSuccPair (extract (κ.headDeletionData hκ).pairing) ++ [(0, Fin.last n)]

theorem Anderson4D.PartialPairing.extract_nonSplit_succ_headDeletion_exact (q : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (hσ : IsNonSplit σ) : extract σ = List.map hdSuccPair (extract (σ.headDeletionData ⋯).pairing) ++ [(0, Fin.last (2 * q + 1))]

Direct specialization to a positive even non-split block.

theorem Anderson4D.PartialPairing.extract_nonSplit_eq_proper_append_whole (q : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (hσ : IsNonSplit σ) : extract σ = List.map hdSuccPair (extract (σ.headDeletionData ⋯).pairing) ++ [wholePrefixPair ⋯]

The direct paper specialization, rewritten with the generic whole-prefix endpoint pair used by the integrand ledger.

theorem Anderson4D.PartialPairing.nonSplit_proper_right_before_whole (q : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (hσ : IsNonSplit σ) (p : Fin (2 * (q + 1)) × Fin (2 * (q + 1))) (hp : p ∈ List.map hdSuccPair (extract (σ.headDeletionData ⋯).pairing)) : ↑p.2 + 1 < 2 * (q + 1)

The proper extractions preceding the terminal whole block cannot share its right endpoint. This is the precise strict-bound fact needed to use the non-junk branch of diffFactorJ.

theorem Anderson4D.PartialPairing.prefixDifferenceProduct_nonSplit {N : ℕ} (q : ℕ) (ha : 2 * (q + 1) ≤ N) (σ : PartialPairing (Fin (2 * (q + 1)))) (hσ : IsNonSplit σ) (xt : Fin (N + 2) → T4) : (List.map (fun (p : Fin (2 * (q + 1)) × Fin (2 * (q + 1))) => diffFactor xt (eaPrefixPair ha p)) (extract σ)).prod = (List.map (diffFactorJ (ambientPrefixTuple ha xt)) (extract σ)).prod * (greenFn (ambientTailTuple ha xt 0 - ambientTailTuple ha xt 1) - greenFn (ambientPrefixTuple ha xt ⟨0, ⋯⟩ - ambientTailTuple ha xt 1))

Non-split specialization of the prefix difference ledger.

theorem Anderson4D.PartialPairing.chainProduct_appendPairingTo {N a : ℕ} (ha : a ≤ N) (ha0 : 0 < a) (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin (N - a))) (xt : Fin (N + 2) → T4) (hwhole : a ∈ List.map (fun (p : Fin a × Fin a) => ↑p.2 + 1) (extract σ)) : (∏ 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)) = (greenFn (xt 0 - xt 1) * ∏ e : Fin (a - 1), if ↑e ∈ List.map (fun (p : Fin a × Fin a) => ↑p.2) (extract σ) then 1 else if h : ↑e + 1 < a then greenFn (ambientPrefixTuple ha xt ⟨↑e, ⋯⟩ - ambientPrefixTuple ha xt ⟨↑e + 1, h⟩) else 1) * ∏ e : Fin (N - a), if ↑e.succ ∈ List.map (fun (p : Fin (N - a) × Fin (N - a)) => ↑p.2 + 1) (extract τ) then 1 else greenFn (ambientTailTuple ha xt e.succ.castSucc - ambientTailTuple ha xt e.succ.succ)

theorem Anderson4D.PartialPairing.nonSplit_whole_extractedRightValue (q : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (hσ : IsNonSplit σ) : 2 * (q + 1) ∈ List.map (fun (p : Fin (2 * (q + 1)) × Fin (2 * (q + 1))) => ↑p.2 + 1) (extract σ)

The terminal whole-prefix extraction removes the chain edge numbered by the prefix length.

theorem Anderson4D.PartialPairing.detIntegrand_appendPairingTo_nonSplit (ρ : SmoothCutoff) (ε : ℝ) {N : ℕ} (q : ℕ) (ha : 2 * (q + 1) ≤ N) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin (N - 2 * (q + 1)))) (hσ : IsNonSplit σ) (xt : Fin (N + 2) → T4) : detIntegrand ρ ε N (appendPairingTo ha σ τ) xt = greenFn (xt 0 - xt 1) * detJintegrand ρ ε (q + 1) σ (ambientPrefixTuple ha xt) * (greenFn (ambientTailTuple ha xt 0 - ambientTailTuple ha xt 1) - greenFn (ambientPrefixTuple ha xt ⟨0, ⋯⟩ - ambientTailTuple ha xt 1)) * detIntegrandAfterFirst ρ ε (N - 2 * (q + 1)) τ (ambientTailTuple ha xt)

Deterministic closed-form compatibility for a non-split fully paired prefix followed by an arbitrary tail. The terminal extraction is exactly the boundary difference missing from the internal J chain.

theorem Anderson4D.PartialPairing.randIntegrand_appendPairingTo_nonSplit (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {N : ℕ} (q : ℕ) (ha : 2 * (q + 1) ≤ N) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin (N - 2 * (q + 1)))) (hσ : IsNonSplit σ) (xt : Fin (N + 2) → T4) (ω : M.Ω) : randIntegrand M ρ ε (appendPairingTo ha σ τ) xt ω = greenFn (xt 0 - xt 1) * detJintegrand ρ ε (q + 1) σ (ambientPrefixTuple ha xt) * (randIntegrand M ρ ε τ (ambientTailTuple ha xt) ω - randIntegrand M ρ ε τ (setTupleFirst (ambientPrefixTuple ha xt ⟨0, ⋯⟩) (ambientTailTuple ha xt)) ω)

Random closed-form compatibility for the same block decomposition. The boundary difference is represented canonically as the difference of two tail random integrands, exactly the (J-Cδ)+Cδ split used in the paper's case-(3) reduction.

theorem Anderson4D.PartialPairing.rawBlock_eq_ambient_add_diagonal (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {N : ℕ} (q : ℕ) (ha : 2 * (q + 1) ≤ N) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin (N - 2 * (q + 1)))) (hσ : IsNonSplit σ) (xt : Fin (N + 2) → T4) (ω : M.Ω) : greenFn (xt 0 - xt 1) * detJintegrand ρ ε (q + 1) σ (ambientPrefixTuple ha xt) * randIntegrand M ρ ε τ (ambientTailTuple ha xt) ω = randIntegrand M ρ ε (appendPairingTo ha σ τ) xt ω + greenFn (xt 0 - xt 1) * detJintegrand ρ ε (q + 1) σ (ambientPrefixTuple ha xt) * randIntegrand M ρ ε τ (setTupleFirst (ambientPrefixTuple ha xt ⟨0, ⋯⟩) (ambientTailTuple ha xt)) ω

Rearranged pointwise form used directly in paper (3.18): the raw J × tail block is the ambient renormalized integrand plus the diagonal tail block.

def Anderson4D.PartialPairing.arithmeticTailEquiv (a r : ℕ) : Fin r ≃ Fin (a + r - a)

Equations

• Anderson4D.PartialPairing.arithmeticTailEquiv a r = (Fin.castOrderIso ⋯).toEquiv

def Anderson4D.PartialPairing.arithmeticTailPairing {a r : ℕ} (τ : PartialPairing (Fin r)) : PartialPairing (Fin (a + r - a))

Equations

• τ.arithmeticTailPairing = (Anderson4D.PartialPairing.congr (Anderson4D.PartialPairing.arithmeticTailEquiv a r)) τ

@[simp]

theorem Anderson4D.PartialPairing.arithmeticTailPairing_apply {a r : ℕ} (τ : PartialPairing (Fin r)) (j : Fin r) : τ.arithmeticTailPairing ((arithmeticTailEquiv a r) j) = (arithmeticTailEquiv a r) (τ j)

@[simp]

theorem Anderson4D.PartialPairing.arithmeticTailEquiv_val (a r : ℕ) (j : Fin r) : ↑((arithmeticTailEquiv a r) j) = ↑j

theorem Anderson4D.PartialPairing.appendPairingTo_arithmeticTailPairing {a r : ℕ} (σ : PartialPairing (Fin a)) (τ : PartialPairing (Fin r)) : appendPairingTo ⋯ σ τ.arithmeticTailPairing = σ.appendPairing τ

Transport across propositionally equal finite cardinalities

def Anderson4D.PartialPairing.arithmeticCastPairing {m n : ℕ} (h : m = n) (κ : PartialPairing (Fin m)) : PartialPairing (Fin n)

Equations

• Anderson4D.PartialPairing.arithmeticCastPairing h κ = (Anderson4D.PartialPairing.congr (Fin.castOrderIso h).toEquiv) κ

def Anderson4D.PartialPairing.arithmeticCastTuple {m n : ℕ} (h : m = n) (xt : Fin (m + 2) → T4) : Fin (n + 2) → T4

Equations

• Anderson4D.PartialPairing.arithmeticCastTuple h xt j = xt (Fin.cast ⋯ j)

@[simp]

theorem Anderson4D.PartialPairing.arithmeticCastPairing_rfl {m : ℕ} (κ : PartialPairing (Fin m)) : arithmeticCastPairing ⋯ κ = κ

@[simp]

theorem Anderson4D.PartialPairing.arithmeticCastTuple_rfl {m : ℕ} (xt : Fin (m + 2) → T4) : arithmeticCastTuple ⋯ xt = xt

theorem Anderson4D.PartialPairing.detIntegrandAfterFirst_arithmeticCast (ρ : SmoothCutoff) (ε : ℝ) {m n : ℕ} (h : m = n) (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) : detIntegrandAfterFirst ρ ε n (arithmeticCastPairing h κ) (arithmeticCastTuple h xt) = detIntegrandAfterFirst ρ ε m κ xt

theorem Anderson4D.PartialPairing.wickAt_arithmeticCast (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {m n : ℕ} (h : m = n) (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) (ω : M.Ω) : wickAt M ρ ε (arithmeticCastPairing h κ) (arithmeticCastTuple h xt) ω = wickAt M ρ ε κ xt ω

theorem Anderson4D.PartialPairing.detIntegrand_arithmeticCast (ρ : SmoothCutoff) (ε : ℝ) {m n : ℕ} (h : m = n) (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) : detIntegrand ρ ε n (arithmeticCastPairing h κ) (arithmeticCastTuple h xt) = detIntegrand ρ ε m κ xt

theorem Anderson4D.PartialPairing.randIntegrand_arithmeticCast (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {m n : ℕ} (h : m = n) (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) (ω : M.Ω) : randIntegrand M ρ ε (arithmeticCastPairing h κ) (arithmeticCastTuple h xt) ω = randIntegrand M ρ ε κ xt ω

The actual case-(3) spatial tuple

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

@[simp]

theorem Anderson4D.PartialPairing.detJTupleSucc_last (q : ℕ) (z w : T4) (u : Fin (2 * q) → T4) : detJTupleSucc q z w u (Fin.last (2 * (q + 1) - 1)) = w

theorem Anderson4D.PartialPairing.ambientTailTuple_caseThree_cast_apply (q r : ℕ) (x z w y : T4) (t : Fin (2 * q + r) → T4) (j : Fin (r + 2)) : ambientTailTuple ⋯ (assemble x y (caseThreeAmbientInternal q r z w t)) (Fin.cast ⋯ j) = caseThreeTailTuple q r w y t j

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

theorem Anderson4D.PartialPairing.arithmeticTailPairing_eq_cast {a r : ℕ} (τ : PartialPairing (Fin r)) : τ.arithmeticTailPairing = arithmeticCastPairing ⋯ τ

Pointwise deterministic case-(3) specialization

theorem Anderson4D.PartialPairing.detIntegrand_caseThreeAmbient (ρ : 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) (σ.appendPairing τ) (assemble x y (caseThreeAmbientInternal q r z w t)) = greenFn (x - z) * detJintegrand ρ ε (q + 1) σ (detJTupleSucc q z w fun (i : Fin (2 * q)) => t (Fin.castAdd r i)) * (greenFn (caseThreeTailTuple q r w y t 0 - caseThreeTailTuple q r w y t 1) - greenFn (z - caseThreeTailTuple q r w y t 1)) * detIntegrandAfterFirst ρ ε r τ (caseThreeTailTuple q r w y t)

theorem Anderson4D.PartialPairing.randIntegrand_caseThreeAmbient (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.Ω) : randIntegrand M ρ ε (σ.appendPairing τ) (assemble x y (caseThreeAmbientInternal q r z w t)) ω = greenFn (x - z) * detJintegrand ρ ε (q + 1) σ (detJTupleSucc q z w fun (i : Fin (2 * q)) => t (Fin.castAdd r i)) * (greenFn (caseThreeTailTuple q r w y t 0 - caseThreeTailTuple q r w y t 1) - greenFn (z - caseThreeTailTuple q r w y t 1)) * (detIntegrandAfterFirst ρ ε r τ (caseThreeTailTuple q r w y t) * wickAt M ρ ε τ (caseThreeTailTuple q r w y t) ω)

theorem Anderson4D.PartialPairing.randIntegrand_caseThreeAmbient_eq_tail_sub (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.Ω) : randIntegrand M ρ ε (σ.appendPairing τ) (assemble x y (caseThreeAmbientInternal q r z w t)) ω = greenFn (x - z) * detJintegrand ρ ε (q + 1) σ (detJTupleSucc q z w fun (i : Fin (2 * q)) => t (Fin.castAdd r i)) * (randIntegrand M ρ ε τ (caseThreeTailTuple q r w y t) ω - randIntegrand M ρ ε τ (setTupleFirst z (caseThreeTailTuple q r w y t)) ω)

Paper-facing form: the boundary Green difference is exactly the subtraction produced by replacing the tail's left endpoint w by z.

theorem Anderson4D.PartialPairing.caseThreeJointCore_eq_ambient_add_diagonal (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.Ω) : greenFn (x - z) * caseThreeJointCore M ρ ε q r σ τ z w y ω t = randIntegrand M ρ ε (σ.appendPairing τ) (assemble x y (caseThreeAmbientInternal q r z w t)) ω + greenFn (x - z) * detJintegrand ρ ε (q + 1) σ (detJTupleSucc q z w fun (i : Fin (2 * q)) => t (Fin.castAdd r i)) * randIntegrand M ρ ε τ (setTupleFirst z (caseThreeTailTuple q r w y t)) ω

Raw J × tail = ambient + diagonal, the pointwise paper (3.18) rearrangement before any spatial integration.