L0 combinatorics: partial pairings and fully paired subintervals

Paper: D-pair — Def 2.2 / Def 2.3 — pairings, intervals, primitivity

Formalization of Definitions 2.2–2.3 of Deng–Shen (arXiv:2607.10105), PAPER_MAP nodes D-pair and D-int, together with the operations on pairings that the proof of Prop 3.4 and the Dyck-word bookkeeping of §4.1 require (node D-RI's interval-removal step, Def 3.1(2)).

Design

• A partial pairing of a finite index type ι is represented as an involution κ : ι → ι (PartialPairing): the singles of the paper are its fixed points (PartialPairing.singles), the pairs are its 2-cycles, recorded as unordered pairs (PartialPairing.pairs : Finset (Sym2 ι)).
• The ordered layer (subintervals of the paper's [1, m]) is developed on ι := Fin m with intervals Finset.Icc a b. IsFullyPairedOn κ B says that B contains no single and is closed under κ; IsPrimitive says that no proper fully paired subinterval exists (paper Def 2.3; for a primitive full pairing the whole of [1, m] is still fully paired). The selector of paper Def 3.1(2) — the smallest-length, leftmost fully paired subinterval, the whole interval being allowed — is leastFullyPairedSubinterval, with hypothesis HasFullyPairedSubinterval (no properness requirement); the properness-aware variant used to characterize primitivity is HasProperFullyPairedSubinterval.
• Interval removal (Def 3.1(2a)) is implemented on the complement subtype: PartialPairing.removeInterval produces a pairing of {i : Fin m // i ∉ Finset.Icc a b}, avoiding Fin re-indexing arithmetic in the primary API. The transported version on Fin (m - (Icc a b).card) is provided as removeIntervalFin via the order isomorphism complOrderIso.

Everything in this file is fully proved; the enumeration instances are computable and the expected small cardinalities are checked both by #guard and by kernel-reduced decide examples.

structure Anderson4D.PartialPairing (ι : Type u_1) : Type u_1

Paper Def 2.2 (node D-pair). A partial pairing of the index type ι is an involution κ : ι → ι. Indices with κ i = i are the singles; the 2-cycles {i, κ i} (for κ i ≠ i) are the pairs.

• toFun : ι → ι

  The underlying involutive map.

• involutive : Function.Involutive self.toFun

  The map is an involution.

@[implicit_reducible]

instance Anderson4D.PartialPairing.instFunLike {ι : Type u_1} : FunLike (PartialPairing ι) ι ι

Equations

• Anderson4D.PartialPairing.instFunLike = { coe := Anderson4D.PartialPairing.toFun, coe_injective := ⋯ }

@[simp]

theorem Anderson4D.PartialPairing.coe_mk {ι : Type u_1} (f : ι → ι) (hf : Function.Involutive f) : ⇑{ toFun := f, involutive := hf } = f

theorem Anderson4D.PartialPairing.ext {ι : Type u_1} {κ₁ κ₂ : PartialPairing ι} (h : ∀ (i : ι), κ₁ i = κ₂ i) : κ₁ = κ₂

theorem Anderson4D.PartialPairing.ext_iff {ι : Type u_1} {κ₁ κ₂ : PartialPairing ι} : κ₁ = κ₂ ↔ ∀ (i : ι), κ₁ i = κ₂ i

@[simp]

theorem Anderson4D.PartialPairing.apply_apply {ι : Type u_1} (κ : PartialPairing ι) (i : ι) : κ (κ i) = i

theorem Anderson4D.PartialPairing.injective {ι : Type u_1} (κ : PartialPairing ι) : Function.Injective ⇑κ

theorem Anderson4D.PartialPairing.surjective {ι : Type u_1} (κ : PartialPairing ι) : Function.Surjective ⇑κ

theorem Anderson4D.PartialPairing.bijective {ι : Type u_1} (κ : PartialPairing ι) : Function.Bijective ⇑κ

theorem Anderson4D.PartialPairing.apply_eq_iff {ι : Type u_1} (κ : PartialPairing ι) {i j : ι} : κ i = j ↔ i = κ j

An involution moves i to j iff it moves j to i.

def Anderson4D.PartialPairing.toPerm {ι : Type u_1} (κ : PartialPairing ι) : Equiv.Perm ι

The permutation underlying a partial pairing.

Equations

• κ.toPerm = Function.Involutive.toPerm κ.toFun ⋯

@[simp]

theorem Anderson4D.PartialPairing.coe_toPerm {ι : Type u_1} (κ : PartialPairing ι) : ⇑κ.toPerm = ⇑κ

def Anderson4D.PartialPairing.id {ι : Type u_1} : PartialPairing ι

The identity involution: the empty pairing, in which every index is a single.

Equations

• Anderson4D.PartialPairing.id = { toFun := fun (i : ι) => i, involutive := ⋯ }

@[implicit_reducible]

instance Anderson4D.PartialPairing.instInhabited {ι : Type u_1} : Inhabited (PartialPairing ι)

Equations

• Anderson4D.PartialPairing.instInhabited = { default := Anderson4D.PartialPairing.id }

@[simp]

theorem Anderson4D.PartialPairing.id_apply {ι : Type u_1} (i : ι) : PartialPairing.id i = i

theorem Anderson4D.PartialPairing.apply_notMem {ι : Type u_1} (κ : PartialPairing ι) {B : Finset ι} (hB : ∀ j ∈ B, κ j ∈ B) {i : ι} (hi : i ∉ B) : κ i ∉ B

If κ maps B into B, then it maps the complement of B into the complement of B (using κ ∘ κ = id).

def Anderson4D.PartialPairing.restrictCompl {ι : Type u_1} (κ : PartialPairing ι) {B : Finset ι} (hB : ∀ j ∈ B, κ j ∈ B) : PartialPairing { i : ι // i ∉ B }

Restrict a partial pairing to the complement of a κ-closed finset, as a pairing of the complement subtype. This is the engine behind interval removal (paper Def 3.1(2a)).

Equations

• κ.restrictCompl hB = { toFun := fun (i : { i : ι // i ∉ B }) => ⟨κ ↑i, ⋯⟩, involutive := ⋯ }

@[simp]

theorem Anderson4D.PartialPairing.restrictCompl_apply_coe {ι : Type u_1} (κ : PartialPairing ι) {B : Finset ι} (hB : ∀ j ∈ B, κ j ∈ B) (i : { i : ι // i ∉ B }) : ↑((κ.restrictCompl hB) i) = κ ↑i

def Anderson4D.PartialPairing.congr {ι : Type u_1} {ι' : Type u_2} (e : ι ≃ ι') : PartialPairing ι ≃ PartialPairing ι'

Transport of partial pairings along an equivalence of index types (conjugation), as an equivalence. Used to move the induced pairing of removeInterval to a Fin index set, and later for the pairing manipulations in the proof of Prop 3.4.

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.congr_apply_apply {ι : Type u_1} {ι' : Type u_2} (e : ι ≃ ι') (κ : PartialPairing ι) (j : ι') : ((congr e) κ) j = e (κ (e.symm j))

def Anderson4D.PartialPairing.singles {ι : Type u_1} [Fintype ι] [DecidableEq ι] (κ : PartialPairing ι) : Finset ι

The singles of a partial pairing: its fixed points (paper Def 2.2, the set S).

Equations

• κ.singles = {i : ι | κ i = i}

def Anderson4D.PartialPairing.pairSupport {ι : Type u_1} [Fintype ι] [DecidableEq ι] (κ : PartialPairing ι) : Finset ι

The indices moved by the pairing: the union of its pairs (complement of the singles).

Equations

• κ.pairSupport = {i : ι | κ i ≠ i}

@[simp]

theorem Anderson4D.PartialPairing.mem_singles {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : PartialPairing ι} {i : ι} : i ∈ κ.singles ↔ κ i = i

@[simp]

theorem Anderson4D.PartialPairing.mem_pairSupport {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : PartialPairing ι} {i : ι} : i ∈ κ.pairSupport ↔ κ i ≠ i

theorem Anderson4D.PartialPairing.apply_mem_pairSupport {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : PartialPairing ι} {i : ι} (hi : i ∈ κ.pairSupport) : κ i ∈ κ.pairSupport

theorem Anderson4D.PartialPairing.singles_union_pairSupport {ι : Type u_1} [Fintype ι] [DecidableEq ι] (κ : PartialPairing ι) : κ.singles ∪ κ.pairSupport = Finset.univ

theorem Anderson4D.PartialPairing.disjoint_singles_pairSupport {ι : Type u_1} [Fintype ι] [DecidableEq ι] (κ : PartialPairing ι) : Disjoint κ.singles κ.pairSupport

theorem Anderson4D.PartialPairing.card_singles_add_card_pairSupport {ι : Type u_1} [Fintype ι] [DecidableEq ι] (κ : PartialPairing ι) : κ.singles.card + κ.pairSupport.card = Fintype.card ι

def Anderson4D.PartialPairing.pairs {ι : Type u_1} [Fintype ι] [DecidableEq ι] (κ : PartialPairing ι) : Finset (Sym2 ι)

The pairs of a partial pairing, as unordered pairs (paper Def 2.2, the set P).

Equations

• κ.pairs = Finset.image (fun (i : ι) => s(i, κ i)) κ.pairSupport

theorem Anderson4D.PartialPairing.mem_pairs {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : PartialPairing ι} {p : Sym2 ι} : p ∈ κ.pairs ↔ ∃ (i : ι), κ i ≠ i ∧ s(i, κ i) = p

theorem Anderson4D.PartialPairing.pairSupport_filter_eq_pair {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : PartialPairing ι} {a : ι} (ha : κ a ≠ a) : {i ∈ κ.pairSupport | s(i, κ i) = s(a, κ a)} = {a, κ a}

The fiber of the pair {a, κ a} inside the pair support is exactly {a, κ a}.

theorem Anderson4D.PartialPairing.card_pairSupport {ι : Type u_1} [Fintype ι] [DecidableEq ι] (κ : PartialPairing ι) : κ.pairSupport.card = 2 * κ.pairs.card

The pairs partition the pair support into 2-cycles: counting version.

theorem Anderson4D.PartialPairing.even_card_pairSupport {ι : Type u_1} [Fintype ι] [DecidableEq ι] (κ : PartialPairing ι) : Even κ.pairSupport.card

theorem Anderson4D.PartialPairing.card_singles_add_two_mul_card_pairs {ι : Type u_1} [Fintype ι] [DecidableEq ι] (κ : PartialPairing ι) : κ.singles.card + 2 * κ.pairs.card = Fintype.card ι

Counting form of Def 2.2: #S + 2 #P = m.

def Anderson4D.PartialPairing.IsFull {ι : Type u_1} (κ : PartialPairing ι) : Prop

Paper Def 2.2 (node D-pair). A partial pairing is full if it has no singles: every index belongs to a pair.

Equations

• κ.IsFull = ∀ (i : ι), κ i ≠ i

@[implicit_reducible]

instance Anderson4D.PartialPairing.instDecidablePredIsFullOfFintypeOfDecidableEq {ι : Type u_1} [Fintype ι] [DecidableEq ι] : DecidablePred IsFull

Equations

• κ.instDecidablePredIsFullOfFintypeOfDecidableEq = decidable_of_iff (∀ (i : ι), κ i ≠ i) ⋯

theorem Anderson4D.PartialPairing.isFull_iff_singles_eq_empty {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : PartialPairing ι} : κ.IsFull ↔ κ.singles = ∅

theorem Anderson4D.PartialPairing.isFull_iff_pairSupport_eq_univ {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : PartialPairing ι} : κ.IsFull ↔ κ.pairSupport = Finset.univ

theorem Anderson4D.PartialPairing.IsFull.even_card {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : PartialPairing ι} (hκ : κ.IsFull) : Even (Fintype.card ι)

A full pairing forces an even number of indices.

def Anderson4D.PartialPairing.equivInvolutive {ι : Type u_1} : PartialPairing ι ≃ { f : ι → ι // Function.Involutive f }

A partial pairing is the same data as an involutive self-map.

Equations

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

@[implicit_reducible]

instance Anderson4D.PartialPairing.instDecidableEqOfFintype {ι : Type u_1} [Fintype ι] [DecidableEq ι] : DecidableEq (PartialPairing ι)

Equations

• x✝¹.instDecidableEqOfFintype x✝ = decidable_of_iff (∀ (x : ι), x✝¹ x = x✝ x) ⋯

@[implicit_reducible]

instance Anderson4D.PartialPairing.instDecidablePredForallInvolutiveOfFintypeOfDecidableEq {α : Type u_2} [Fintype α] [DecidableEq α] : DecidablePred Function.Involutive

Equations

• Anderson4D.PartialPairing.instDecidablePredForallInvolutiveOfFintypeOfDecidableEq f = decidable_of_iff (∀ (x : α), f (f x) = x) ⋯

@[implicit_reducible]

instance Anderson4D.PartialPairing.instFintypeOfDecidableEq {ι : Type u_1} [Fintype ι] [DecidableEq ι] : Fintype (PartialPairing ι)

Equations

• Anderson4D.PartialPairing.instFintypeOfDecidableEq = Fintype.ofEquiv { f : ι → ι // Function.Involutive f } Anderson4D.PartialPairing.equivInvolutive.symm

The ordered layer: fully paired subintervals of Fin m

Paper Def 2.3 (node D-int). Subintervals of [1, m] are Finset.Icc a b with a b : Fin m, a ≤ b.

def Anderson4D.IsFullyPairedOn {m : ℕ} (κ : PartialPairing (Fin m)) (B : Finset (Fin m)) : Prop

Paper Def 2.3 (node D-int). B is fully paired under κ if it contains no single of κ and is closed under κ (so the pairs meeting B lie entirely inside B). Stated for an arbitrary finset B; the paper's notion is the special case B = Finset.Icc a b.

Equations

• Anderson4D.IsFullyPairedOn κ B = ((∀ i ∈ B, κ i ≠ i) ∧ ∀ i ∈ B, κ i ∈ B)

@[implicit_reducible]

instance Anderson4D.instDecidableIsFullyPairedOn {m : ℕ} (κ : PartialPairing (Fin m)) (B : Finset (Fin m)) : Decidable (IsFullyPairedOn κ B)

Equations

• Anderson4D.instDecidableIsFullyPairedOn κ B = decidable_of_iff ((∀ i ∈ B, κ i ≠ i) ∧ ∀ i ∈ B, κ i ∈ B) ⋯

theorem Anderson4D.IsFullyPairedOn.ne_of_mem {m : ℕ} {κ : PartialPairing (Fin m)} {B : Finset (Fin m)} (h : IsFullyPairedOn κ B) {i : Fin m} (hi : i ∈ B) : κ i ≠ i

theorem Anderson4D.IsFullyPairedOn.apply_mem {m : ℕ} {κ : PartialPairing (Fin m)} {B : Finset (Fin m)} (h : IsFullyPairedOn κ B) {i : Fin m} (hi : i ∈ B) : κ i ∈ B

theorem Anderson4D.IsFullyPairedOn.apply_notMem {m : ℕ} {κ : PartialPairing (Fin m)} {B : Finset (Fin m)} (h : IsFullyPairedOn κ B) {i : Fin m} (hi : i ∉ B) : κ i ∉ B

theorem Anderson4D.IsFullyPairedOn.inter {m : ℕ} {κ : PartialPairing (Fin m)} {B₁ B₂ : Finset (Fin m)} (h₁ : IsFullyPairedOn κ B₁) (h₂ : IsFullyPairedOn κ B₂) : IsFullyPairedOn κ (B₁ ∩ B₂)

The intersection of two fully paired sets is fully paired.

theorem Anderson4D.IsFullyPairedOn.union {m : ℕ} {κ : PartialPairing (Fin m)} {B₁ B₂ : Finset (Fin m)} (h₁ : IsFullyPairedOn κ B₁) (h₂ : IsFullyPairedOn κ B₂) : IsFullyPairedOn κ (B₁ ∪ B₂)

The union of two fully paired sets is fully paired.

@[simp]

theorem Anderson4D.isFullyPairedOn_empty {m : ℕ} (κ : PartialPairing (Fin m)) : IsFullyPairedOn κ ∅

theorem Anderson4D.isFullyPairedOn_univ_iff {m : ℕ} {κ : PartialPairing (Fin m)} : IsFullyPairedOn κ Finset.univ ↔ κ.IsFull

theorem Anderson4D.isFullyPairedOn_Icc_inter_union {m : ℕ} {κ : PartialPairing (Fin m)} {a b c d : Fin m} (h₁ : IsFullyPairedOn κ (Finset.Icc a b)) (h₂ : IsFullyPairedOn κ (Finset.Icc c d)) : IsFullyPairedOn κ (Finset.Icc a b ∩ Finset.Icc c d) ∧ IsFullyPairedOn κ (Finset.Icc a b ∪ Finset.Icc c d)

Structural lemma for the §4.1 Dyck-word bookkeeping: two fully paired subintervals always have fully paired intersection and union (this strengthens the paper's silent "disjoint or nested or overlapping" case analysis: in the overlapping case both ∩ and ∪ are again fully paired).

def Anderson4D.HasFullyPairedSubinterval {m : ℕ} (κ : PartialPairing (Fin m)) : Prop

κ admits a fully paired subinterval, the whole index interval being allowed. This is the hypothesis of the Def 3.1(2) selector leastFullyPairedSubinterval.

Equations

• Anderson4D.HasFullyPairedSubinterval κ = ∃ (a : Fin m) (b : Fin m), a ≤ b ∧ Anderson4D.IsFullyPairedOn κ (Finset.Icc a b)

@[implicit_reducible]

instance Anderson4D.instDecidableHasFullyPairedSubinterval {m : ℕ} (κ : PartialPairing (Fin m)) : Decidable (HasFullyPairedSubinterval κ)

Equations

• Anderson4D.instDecidableHasFullyPairedSubinterval κ = decidable_of_iff (∃ (a : Fin m) (b : Fin m), a ≤ b ∧ Anderson4D.IsFullyPairedOn κ (Finset.Icc a b)) ⋯

def Anderson4D.HasProperFullyPairedSubinterval {m : ℕ} (κ : PartialPairing (Fin m)) : Prop

κ admits a proper fully paired subinterval (one that is not the whole index interval). Its negation is primitivity, paper Def 2.3.

Equations

• Anderson4D.HasProperFullyPairedSubinterval κ = ∃ (a : Fin m) (b : Fin m), a ≤ b ∧ Finset.Icc a b ≠ Finset.univ ∧ Anderson4D.IsFullyPairedOn κ (Finset.Icc a b)

@[implicit_reducible]

instance Anderson4D.instDecidableHasProperFullyPairedSubinterval {m : ℕ} (κ : PartialPairing (Fin m)) : Decidable (HasProperFullyPairedSubinterval κ)

Equations

• Anderson4D.instDecidableHasProperFullyPairedSubinterval κ = decidable_of_iff (∃ (a : Fin m) (b : Fin m), a ≤ b ∧ Finset.Icc a b ≠ Finset.univ ∧ Anderson4D.IsFullyPairedOn κ (Finset.Icc a b)) ⋯

theorem Anderson4D.HasProperFullyPairedSubinterval.hasFullyPairedSubinterval {m : ℕ} {κ : PartialPairing (Fin m)} (h : HasProperFullyPairedSubinterval κ) : HasFullyPairedSubinterval κ

def Anderson4D.IsPrimitive {m : ℕ} (κ : PartialPairing (Fin m)) : Prop

Paper Def 2.3 (node D-int). A partial pairing of Fin m is primitive if it has no proper fully paired subinterval: every fully paired subinterval is the whole of Fin m. (For a primitive full pairing the whole interval is itself fully paired, so primitivity does not exclude it.)

Equations

• Anderson4D.IsPrimitive κ = ∀ (a b : Fin m), a ≤ b → Anderson4D.IsFullyPairedOn κ (Finset.Icc a b) → Finset.Icc a b = Finset.univ

@[implicit_reducible]

instance Anderson4D.instDecidableIsPrimitive {m : ℕ} (κ : PartialPairing (Fin m)) : Decidable (IsPrimitive κ)

Equations

• Anderson4D.instDecidableIsPrimitive κ = decidable_of_iff (∀ (a b : Fin m), a ≤ b → Anderson4D.IsFullyPairedOn κ (Finset.Icc a b) → Finset.Icc a b = Finset.univ) ⋯

theorem Anderson4D.isPrimitive_iff_not_hasProperFullyPairedSubinterval {m : ℕ} {κ : PartialPairing (Fin m)} : IsPrimitive κ ↔ ¬HasProperFullyPairedSubinterval κ

theorem Anderson4D.Icc_zero_last_eq_univ {m : ℕ} : Finset.Icc 0 (Fin.last m) = Finset.univ

theorem Anderson4D.PartialPairing.IsFull.hasFullyPairedSubinterval {m : ℕ} {κ : PartialPairing (Fin (m + 1))} (hκ : κ.IsFull) : HasFullyPairedSubinterval κ

A full pairing of a nonempty index interval always has a fully paired subinterval, namely the whole interval — the situation in which the Def 3.1 induction keeps running until the interval itself is removed.

The Def 3.1(2) selector: smallest, leftmost fully paired subinterval

def Anderson4D.fpIntervals {m : ℕ} (κ : PartialPairing (Fin m)) : Finset (Fin m × Fin m)

Endpoint pairs (a, b), a ≤ b, of fully paired subintervals of κ.

Equations

• Anderson4D.fpIntervals κ = {p : Fin m × Fin m | p.1 ≤ p.2 ∧ Anderson4D.IsFullyPairedOn κ (Finset.Icc p.1 p.2)}

theorem Anderson4D.mem_fpIntervals {m : ℕ} {κ : PartialPairing (Fin m)} {p : Fin m × Fin m} : p ∈ fpIntervals κ ↔ p.1 ≤ p.2 ∧ IsFullyPairedOn κ (Finset.Icc p.1 p.2)

theorem Anderson4D.fpIntervals_nonempty_iff {m : ℕ} {κ : PartialPairing (Fin m)} : (fpIntervals κ).Nonempty ↔ HasFullyPairedSubinterval κ

def Anderson4D.minPairedLength {m : ℕ} (κ : PartialPairing (Fin m)) (h : HasFullyPairedSubinterval κ) : ℕ

The minimal length b - a over all fully paired subintervals Finset.Icc a b of κ.

Equations

• Anderson4D.minPairedLength κ h = (Finset.image (fun (p : Fin m × Fin m) => ↑p.2 - ↑p.1) (Anderson4D.fpIntervals κ)).min' ⋯

theorem Anderson4D.minPairedLength_le {m : ℕ} {κ : PartialPairing (Fin m)} (h : HasFullyPairedSubinterval κ) {a b : Fin m} (hab : a ≤ b) (hfp : IsFullyPairedOn κ (Finset.Icc a b)) : minPairedLength κ h ≤ ↑b - ↑a

Minimality of minPairedLength.

def Anderson4D.minCands {m : ℕ} (κ : PartialPairing (Fin m)) (h : HasFullyPairedSubinterval κ) : Finset (Fin m × Fin m)

Fully paired subintervals achieving the minimal length.

Equations

• Anderson4D.minCands κ h = {p ∈ Anderson4D.fpIntervals κ | ↑p.2 - ↑p.1 = Anderson4D.minPairedLength κ h}

theorem Anderson4D.mem_minCands {m : ℕ} {κ : PartialPairing (Fin m)} {h : HasFullyPairedSubinterval κ} {p : Fin m × Fin m} : p ∈ minCands κ h ↔ (p.1 ≤ p.2 ∧ IsFullyPairedOn κ (Finset.Icc p.1 p.2)) ∧ ↑p.2 - ↑p.1 = minPairedLength κ h

theorem Anderson4D.minCands_nonempty {m : ℕ} (κ : PartialPairing (Fin m)) (h : HasFullyPairedSubinterval κ) : (minCands κ h).Nonempty

def Anderson4D.leastLeft {m : ℕ} (κ : PartialPairing (Fin m)) (h : HasFullyPairedSubinterval κ) : Fin m

The left endpoint selected by paper Def 3.1(2): leftmost among the minimal-length fully paired subintervals.

Equations

• Anderson4D.leastLeft κ h = (Finset.image Prod.fst (Anderson4D.minCands κ h)).min' ⋯

theorem Anderson4D.exists_leastLeft_snd {m : ℕ} (κ : PartialPairing (Fin m)) (h : HasFullyPairedSubinterval κ) : ∃ (b : Fin m), (leastLeft κ h, b) ∈ minCands κ h

theorem Anderson4D.leastLeft_le {m : ℕ} {κ : PartialPairing (Fin m)} (h : HasFullyPairedSubinterval κ) {a b : Fin m} (hab : a ≤ b) (hfp : IsFullyPairedOn κ (Finset.Icc a b)) (hlen : ↑b - ↑a = minPairedLength κ h) : leastLeft κ h ≤ a

Leftmost-ness of leastLeft among minimal-length fully paired subintervals.

theorem Anderson4D.leastLeft_add_minPairedLength_lt {m : ℕ} (κ : PartialPairing (Fin m)) (h : HasFullyPairedSubinterval κ) : ↑(leastLeft κ h) + minPairedLength κ h < m

def Anderson4D.leastFullyPairedSubinterval {m : ℕ} (κ : PartialPairing (Fin m)) (h : HasFullyPairedSubinterval κ) : Fin m × Fin m

Paper Def 3.1(2) selector. Among all fully paired subintervals of κ (the whole interval allowed), the one of smallest length and, among those, the leftmost; returned as its pair of endpoints (a, b).

Equations

• Anderson4D.leastFullyPairedSubinterval κ h = (Anderson4D.leastLeft κ h, ⟨↑(Anderson4D.leastLeft κ h) + Anderson4D.minPairedLength κ h, ⋯⟩)

theorem Anderson4D.leastFullyPairedSubinterval_fst {m : ℕ} (κ : PartialPairing (Fin m)) (h : HasFullyPairedSubinterval κ) : (leastFullyPairedSubinterval κ h).1 = leastLeft κ h

theorem Anderson4D.leastFullyPairedSubinterval_mem {m : ℕ} (κ : PartialPairing (Fin m)) (h : HasFullyPairedSubinterval κ) : leastFullyPairedSubinterval κ h ∈ minCands κ h

theorem Anderson4D.leastFullyPairedSubinterval_fst_le_snd {m : ℕ} (κ : PartialPairing (Fin m)) (h : HasFullyPairedSubinterval κ) : (leastFullyPairedSubinterval κ h).1 ≤ (leastFullyPairedSubinterval κ h).2

The selected subinterval is a genuine interval: a ≤ b.

theorem Anderson4D.leastFullyPairedSubinterval_isFullyPairedOn {m : ℕ} (κ : PartialPairing (Fin m)) (h : HasFullyPairedSubinterval κ) : IsFullyPairedOn κ (Finset.Icc (leastFullyPairedSubinterval κ h).1 (leastFullyPairedSubinterval κ h).2)

The selected subinterval is fully paired.

theorem Anderson4D.leastFullyPairedSubinterval_length {m : ℕ} (κ : PartialPairing (Fin m)) (h : HasFullyPairedSubinterval κ) : ↑(leastFullyPairedSubinterval κ h).2 - ↑(leastFullyPairedSubinterval κ h).1 = minPairedLength κ h

The selected subinterval has the minimal length.

theorem Anderson4D.eq_leastFullyPairedSubinterval {m : ℕ} {κ : PartialPairing (Fin m)} (h : HasFullyPairedSubinterval κ) {a b : Fin m} (hab : a ≤ b) (_hfp : IsFullyPairedOn κ (Finset.Icc a b)) (hlen : ↑b - ↑a = minPairedLength κ h) (hfst : a = leastLeft κ h) : (a, b) = leastFullyPairedSubinterval κ h

Uniqueness: a fully paired subinterval of minimal length whose left endpoint is the selected one is the selected subinterval.

theorem Anderson4D.leastFullyPairedSubinterval_inclusion_minimal {m : ℕ} {κ : PartialPairing (Fin m)} (h : HasFullyPairedSubinterval κ) {c d : Fin m} (hcd : c ≤ d) (hfp : IsFullyPairedOn κ (Finset.Icc c d)) (hsub : Finset.Icc c d ⊆ Finset.Icc (leastFullyPairedSubinterval κ h).1 (leastFullyPairedSubinterval κ h).2) : Finset.Icc c d = Finset.Icc (leastFullyPairedSubinterval κ h).1 (leastFullyPairedSubinterval κ h).2

The selected subinterval is also smallest with respect to inclusion: a fully paired subinterval contained in it coincides with it.

Interval removal (paper Def 3.1(2a))

Primary version: the induced pairing on the complement subtype {i : Fin m // i ∉ Finset.Icc a b} — no Fin re-indexing arithmetic. The re-indexed version on Fin (m - (Finset.Icc a b).card) is obtained by transporting along the order isomorphism complOrderIso.

def Anderson4D.PartialPairing.removeInterval {m : ℕ} (κ : PartialPairing (Fin m)) {a b : Fin m} (h : IsFullyPairedOn κ (Finset.Icc a b)) : PartialPairing { i : Fin m // i ∉ Finset.Icc a b }

Remove a fully paired subinterval from a pairing: the induced pairing on the complement subtype. Well-defined because a fully paired set is κ-closed, hence so is its complement.

Equations

• κ.removeInterval h = κ.restrictCompl ⋯

@[simp]

theorem Anderson4D.PartialPairing.removeInterval_apply_coe {m : ℕ} (κ : PartialPairing (Fin m)) {a b : Fin m} (h : IsFullyPairedOn κ (Finset.Icc a b)) (i : { i : Fin m // i ∉ Finset.Icc a b }) : ↑((κ.removeInterval h) i) = κ ↑i

def Anderson4D.notMemOrderIso {m : ℕ} (B : Finset (Fin m)) : { i : Fin m // i ∉ B } ≃o ↥Bᶜ

The complement subtype of B : Finset (Fin m), rephrased as the coercion of the finset Bᶜ.

Equations

• Anderson4D.notMemOrderIso B = { toEquiv := Equiv.subtypeEquivRight ⋯, map_rel_iff' := ⋯ }

def Anderson4D.complOrderIso {m : ℕ} (B : Finset (Fin m)) : { i : Fin m // i ∉ B } ≃o Fin (m - B.card)

The order isomorphism between the complement of B : Finset (Fin m) and Fin (m - B.card), given by the unique monotone enumeration.

Equations

• Anderson4D.complOrderIso B = (Anderson4D.notMemOrderIso B).trans (Bᶜ.orderIsoOfFin ⋯).symm

def Anderson4D.removeIntervalFin {m : ℕ} (κ : PartialPairing (Fin m)) {a b : Fin m} (h : IsFullyPairedOn κ (Finset.Icc a b)) : PartialPairing (Fin (m - (Finset.Icc a b).card))

Interval removal, re-indexed over Fin (m - (Finset.Icc a b).card) by the monotone enumeration of the complement. removeInterval (the subtype version) is the primary API; this is the transported form.

Equations

• Anderson4D.removeIntervalFin κ h = (Anderson4D.PartialPairing.congr (Anderson4D.complOrderIso (Finset.Icc a b)).toEquiv) (κ.removeInterval h)

theorem Anderson4D.removeIntervalFin_def {m : ℕ} (κ : PartialPairing (Fin m)) {a b : Fin m} (h : IsFullyPairedOn κ (Finset.Icc a b)) : removeIntervalFin κ h = (PartialPairing.congr (complOrderIso (Finset.Icc a b)).toEquiv) (κ.removeInterval h)

theorem Anderson4D.removeIntervalFin_apply {m : ℕ} (κ : PartialPairing (Fin m)) {a b : Fin m} (h : IsFullyPairedOn κ (Finset.Icc a b)) (i : { i : Fin m // i ∉ Finset.Icc a b }) : (removeIntervalFin κ h) ((complOrderIso (Finset.Icc a b)) i) = (complOrderIso (Finset.Icc a b)) ⟨κ ↑i, ⋯⟩

Specification of removeIntervalFin: it is the conjugate of κ (restricted to the complement) under the monotone enumeration complOrderIso.