The three head cases in the proof of Proposition 3.4

The paper indexes a pairing by [1, m]. Here a pairing of Fin (m + 1) uses zero-based indices, so its distinguished new index is 0, and the paper prefix [1, 2q] is exactly the finset of indices i < 2q, whose last element is 2q - 1.

def Anderson4D.PartialPairing.headEvenPrefix (m q : ℕ) : Finset (Fin (m + 1))

The zero-based prefix corresponding to the paper interval [1, 2q]. The bound 2q ≤ m + 1 is deliberately not built into the definition.

Equations

• Anderson4D.PartialPairing.headEvenPrefix m q = {i : Fin (m + 1) | ↑i < 2 * q}

@[simp]

theorem Anderson4D.PartialPairing.mem_headEvenPrefix {m q : ℕ} {i : Fin (m + 1)} : i ∈ headEvenPrefix m q ↔ ↑i < 2 * q

theorem Anderson4D.PartialPairing.card_headEvenPrefix {m q : ℕ} (hq : 2 * q ≤ m + 1) : (headEvenPrefix m q).card = 2 * q

def Anderson4D.PartialPairing.headEvenPrefixLast {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) : Fin (m + 1)

The endpoint 2q - 1 of the zero-based realization of [1, 2q].

Equations

• Anderson4D.PartialPairing.headEvenPrefixLast hqpos hq = ⟨2 * q - 1, ⋯⟩

theorem Anderson4D.PartialPairing.headEvenPrefix_eq_Icc {m q : ℕ} (hqpos : 1 ≤ q) (hq : 2 * q ≤ m + 1) : headEvenPrefix m q = Finset.Icc 0 (headEvenPrefixLast hqpos hq)

def Anderson4D.PartialPairing.IsFullyPairedHeadPrefix {m : ℕ} (κ : PartialPairing (Fin (m + 1))) (q : ℕ) : Prop

A positive even prefix which is fully paired under κ.

Equations

• κ.IsFullyPairedHeadPrefix q = (1 ≤ q ∧ 2 * q ≤ m + 1 ∧ Anderson4D.IsFullyPairedOn κ (Anderson4D.PartialPairing.headEvenPrefix m q))

@[implicit_reducible]

instance Anderson4D.PartialPairing.instDecidablePredNatIsFullyPairedHeadPrefix {m : ℕ} (κ : PartialPairing (Fin (m + 1))) : DecidablePred κ.IsFullyPairedHeadPrefix

Equations

• κ.instDecidablePredNatIsFullyPairedHeadPrefix q = decidable_of_iff (1 ≤ q ∧ 2 * q ≤ m + 1 ∧ Anderson4D.IsFullyPairedOn κ (Anderson4D.PartialPairing.headEvenPrefix m q)) ⋯

def Anderson4D.PartialPairing.HasFullyPairedHeadPrefix {m : ℕ} (κ : PartialPairing (Fin (m + 1))) : Prop

There is a paper-style fully paired prefix [1, 2q].

Equations

• κ.HasFullyPairedHeadPrefix = ∃ (q : ℕ), κ.IsFullyPairedHeadPrefix q

@[implicit_reducible]

noncomputable instance Anderson4D.PartialPairing.instDecidableHasFullyPairedHeadPrefix {m : ℕ} (κ : PartialPairing (Fin (m + 1))) : Decidable κ.HasFullyPairedHeadPrefix

Equations

• κ.instDecidableHasFullyPairedHeadPrefix = Classical.dec κ.HasFullyPairedHeadPrefix

def Anderson4D.PartialPairing.HeadIsSingle {m : ℕ} (κ : PartialPairing (Fin (m + 1))) : Prop

Case (1): the distinguished head index is a single.

Equations

• κ.HeadIsSingle = (κ 0 = 0)

@[implicit_reducible]

noncomputable instance Anderson4D.PartialPairing.instDecidableHeadIsSingle {m : ℕ} (κ : PartialPairing (Fin (m + 1))) : Decidable κ.HeadIsSingle

Equations

• κ.instDecidableHeadIsSingle = Classical.dec κ.HeadIsSingle

def Anderson4D.PartialPairing.HeadPairedNoPrefix {m : ℕ} (κ : PartialPairing (Fin (m + 1))) : Prop

Case (2): the head is paired, but no [1, 2q] is fully paired.

Equations

• κ.HeadPairedNoPrefix = (κ 0 ≠ 0 ∧ ¬κ.HasFullyPairedHeadPrefix)

@[implicit_reducible]

noncomputable instance Anderson4D.PartialPairing.instDecidableHeadPairedNoPrefix {m : ℕ} (κ : PartialPairing (Fin (m + 1))) : Decidable κ.HeadPairedNoPrefix

Equations

• κ.instDecidableHeadPairedNoPrefix = Classical.dec κ.HeadPairedNoPrefix

def Anderson4D.PartialPairing.HeadPairedWithPrefix {m : ℕ} (κ : PartialPairing (Fin (m + 1))) : Prop

Case (3): the head is paired and some [1, 2q] is fully paired.

Equations

• κ.HeadPairedWithPrefix = (κ 0 ≠ 0 ∧ κ.HasFullyPairedHeadPrefix)

@[implicit_reducible]

noncomputable instance Anderson4D.PartialPairing.instDecidableHeadPairedWithPrefix {m : ℕ} (κ : PartialPairing (Fin (m + 1))) : Decidable κ.HeadPairedWithPrefix

Equations

• κ.instDecidableHeadPairedWithPrefix = Classical.dec κ.HeadPairedWithPrefix

theorem Anderson4D.PartialPairing.head_paired_of_fullyPairedHeadPrefix {m q : ℕ} {κ : PartialPairing (Fin (m + 1))} (h : κ.IsFullyPairedHeadPrefix q) : κ 0 ≠ 0

def Anderson4D.PartialPairing.firstFullyPairedHeadQ {m : ℕ} (κ : PartialPairing (Fin (m + 1))) (h : κ.HasFullyPairedHeadPrefix) : ℕ

The least q for which the paper prefix [1, 2q] is fully paired.

Equations

• κ.firstFullyPairedHeadQ h = Nat.find h

theorem Anderson4D.PartialPairing.firstFullyPairedHeadQ_spec {m : ℕ} (κ : PartialPairing (Fin (m + 1))) (h : κ.HasFullyPairedHeadPrefix) : κ.IsFullyPairedHeadPrefix (κ.firstFullyPairedHeadQ h)

theorem Anderson4D.PartialPairing.firstFullyPairedHeadQ_min {m : ℕ} (κ : PartialPairing (Fin (m + 1))) (h : κ.HasFullyPairedHeadPrefix) {r : ℕ} (hr : κ.IsFullyPairedHeadPrefix r) : κ.firstFullyPairedHeadQ h ≤ r

structure Anderson4D.PartialPairing.HeadPrefixDecomposition {m : ℕ} (κ : PartialPairing (Fin (m + 1))) : Type

Complete data attached to case (3). The minimality field is the exact formal counterpart of “choose the smallest q” in the proof of (3.16).

• q : ℕ
• q_pos : 1 ≤ self.q
• two_mul_le : 2 * self.q ≤ m + 1
• fullyPaired : IsFullyPairedOn κ (headEvenPrefix m self.q)
• minimal (r : ℕ) : κ.IsFullyPairedHeadPrefix r → self.q ≤ r

def Anderson4D.PartialPairing.headPrefixDecomposition {m : ℕ} (κ : PartialPairing (Fin (m + 1))) (h : κ.HasFullyPairedHeadPrefix) : κ.HeadPrefixDecomposition

The canonical minimal-prefix data of a case-(3) pairing.

Equations

• κ.headPrefixDecomposition h = { q := κ.firstFullyPairedHeadQ h, q_pos := ⋯, two_mul_le := ⋯, fullyPaired := ⋯, minimal := ⋯ }

theorem Anderson4D.PartialPairing.HeadPrefixDecomposition.isFullyPairedHeadPrefix {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) : κ.IsFullyPairedHeadPrefix d.q

theorem Anderson4D.PartialPairing.HeadPrefixDecomposition.head_paired {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) : κ 0 ≠ 0

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

theorem Anderson4D.PartialPairing.HeadPrefixDecomposition.no_smaller {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) {r : ℕ} (hr : r < d.q) : ¬κ.IsFullyPairedHeadPrefix r

def Anderson4D.PartialPairing.restrictTo {α : Type u_1} [DecidableEq α] (κ : PartialPairing α) {B : Finset α} (hB : ∀ i ∈ B, κ i ∈ B) : PartialPairing ↥B

Restrict an involution to a closed finset.

Equations

• κ.restrictTo hB = { toFun := fun (i : ↥B) => ⟨κ ↑i, ⋯⟩, involutive := ⋯ }

@[simp]

theorem Anderson4D.PartialPairing.restrictTo_apply_val {α : Type u_1} [DecidableEq α] (κ : PartialPairing α) {B : Finset α} (hB : ∀ i ∈ B, κ i ∈ B) (i : ↥B) : ↑((κ.restrictTo hB) i) = κ ↑i

theorem Anderson4D.PartialPairing.IsFull.congr {α : Type u_1} {β : Type u_2} {κ : PartialPairing α} (hκ : κ.IsFull) (e : α ≃ β) : ((PartialPairing.congr e) κ).IsFull

def Anderson4D.PartialPairing.HeadPrefixDecomposition.prefixOrderIso {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) : Fin (2 * d.q) ≃o ↥(headEvenPrefix m d.q)

Increasing identification of the selected prefix with Fin (2q).

Equations

• d.prefixOrderIso = (Anderson4D.PartialPairing.headEvenPrefix m d.q).orderIsoOfFin ⋯

def Anderson4D.PartialPairing.HeadPrefixDecomposition.prefixPairing {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) : PartialPairing (Fin (2 * d.q))

Restriction of κ to its first fully paired prefix, reindexed from zero through 2q-1.

Equations

• d.prefixPairing = (Anderson4D.PartialPairing.congr d.prefixOrderIso.symm.toEquiv) (κ.restrictTo ⋯)

theorem Anderson4D.PartialPairing.HeadPrefixDecomposition.prefixPairing_isFull {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) : d.prefixPairing.IsFull

def Anderson4D.PartialPairing.HeadPrefixDecomposition.remainderOrderIso {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) : { i : Fin (m + 1) // i ∉ headEvenPrefix m d.q } ≃o Fin (m + 1 - 2 * d.q)

Increasing reindexing of the external remainder. Its source consists of the ambient indices 2q, …, m, i.e. paper indices 2q+1, …, m+1.

Equations

• d.remainderOrderIso = (Anderson4D.complOrderIso (Anderson4D.PartialPairing.headEvenPrefix m d.q)).trans (Fin.castOrderIso ⋯)

def Anderson4D.PartialPairing.HeadPrefixDecomposition.remainderPairing {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (d : κ.HeadPrefixDecomposition) : PartialPairing (Fin (m + 1 - 2 * d.q))

The external pairing σ₂ from case (3), on exactly m+1-2q reindexed positions.

Equations

• d.remainderPairing = (Anderson4D.PartialPairing.congr d.remainderOrderIso.toEquiv) (κ.restrictCompl ⋯)

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

The three cases are represented by disjoint subtypes, yielding a direct finite-sum reindexing API.

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.headCasesEquiv_symm_single {m : ℕ} (κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadIsSingle }) : (headCasesEquiv m).symm (Sum.inl κ) = ↑κ

@[simp]

theorem Anderson4D.PartialPairing.headCasesEquiv_symm_noPrefix {m : ℕ} (κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedNoPrefix }) : (headCasesEquiv m).symm (Sum.inr (Sum.inl κ)) = ↑κ

@[simp]

theorem Anderson4D.PartialPairing.headCasesEquiv_symm_withPrefix {m : ℕ} (κ : { κ : PartialPairing (Fin (m + 1)) // κ.HeadPairedWithPrefix }) : (headCasesEquiv m).symm (Sum.inr (Sum.inr κ)) = ↑κ

theorem Anderson4D.PartialPairing.headCases_complete {m : ℕ} (κ : PartialPairing (Fin (m + 1))) : κ.HeadIsSingle ∨ κ.HeadPairedNoPrefix ∨ κ.HeadPairedWithPrefix

theorem Anderson4D.PartialPairing.headCases_pairwise_disjoint {m : ℕ} (κ : PartialPairing (Fin (m + 1))) : ¬(κ.HeadIsSingle ∧ κ.HeadPairedNoPrefix) ∧ ¬(κ.HeadIsSingle ∧ κ.HeadPairedWithPrefix) ∧ ¬(κ.HeadPairedNoPrefix ∧ κ.HeadPairedWithPrefix)

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

Reindex any finite sum over pairings into the three cases of the proof of Proposition 3.4.