Finite-level thresholds for pure sets

Back-and-forth equivalence between an infinite pure set X and a finite pure set Y (empty language, arbitrary empty-language structure instances) is decided by a count: for tuples a, b with the same equality pattern and a natural level k,

BFEquiv k n a b ↔ k ≤ spare b,

where spare b is the number of elements of Y outside the range of b (as Set.ncard, meaningful for finite Y) (bfEquiv_natCast_iff). The positive direction answers a fresh element on the infinite side by a spare one and an old element by its match; failure is pinned exactly at spare b + 1 (not_bfEquiv_spare_succ): the infinite side plays a fresh element and the finite side must answer with a fresh one, using up a spare, until none is left.

For empty tuples of ℕ and Fin m this is k ≤ m, with failure at m + 1 (bfEquiv_nat_fin_iff, not_bfEquiv_nat_fin_succ).

Also: every tuple of any pure set has orbit rank 0 (orbitRank_pure_eq_zero), the finite counterpart of orbitRank_pureSet: a tuple with the same pattern is the image under a permutation extended from the finite matching (exists_equiv_of_matching with the trivial equivalence relation).

This module sits in the Scott layer: its import closure contains no fiber-assembly module.

theorem FirstOrder.Language.PureSet.sameAtomicType_iff {X : Type u} {Y : Type v} [Language.empty.Structure X] [Language.empty.Structure Y] {n : ℕ} (a : Fin n → X) (b : Fin n → Y) : SameAtomicType a b ↔ ∀ (i j : Fin n), a i = a j ↔ b i = b j

Atomic agreement in the empty language, between two carriers, is agreement of the equality pattern.

noncomputable def FirstOrder.Language.PureSet.spare {Y : Type v} {n : ℕ} (b : Fin n → Y) : ℕ

The number of elements outside the range of a tuple, as Set.ncard. On an infinite carrier Set.ncard of an infinite set is 0, so the threshold theorems require a finite target [Finite Y]; the count is meaningful only there.

Equations

• FirstOrder.Language.PureSet.spare b = (Set.range b)ᶜ.ncard

theorem FirstOrder.Language.PureSet.range_snoc {Y : Type v} {n : ℕ} (b : Fin n → Y) (y : Y) : Set.range (Fin.snoc b y) = insert y (Set.range b)

theorem FirstOrder.Language.PureSet.spare_snoc_of_mem {Y : Type v} {n : ℕ} (b : Fin n → Y) {y : Y} (hy : y ∈ Set.range b) : spare (Fin.snoc b y) = spare b

theorem FirstOrder.Language.PureSet.spare_snoc_of_notMem {Y : Type v} [Finite Y] {n : ℕ} (b : Fin n → Y) {y : Y} (hy : y ∉ Set.range b) : spare (Fin.snoc b y) + 1 = spare b

theorem FirstOrder.Language.PureSet.pattern_snoc {X : Type u} {Y : Type v} {n : ℕ} {a : Fin n → X} {b : Fin n → Y} (h : ∀ (i j : Fin n), a i = a j ↔ b i = b j) {x : X} {y : Y} (hxy : ∀ (i : Fin n), a i = x ↔ b i = y) (i j : Fin (n + 1)) : Fin.snoc a x i = Fin.snoc a x j ↔ Fin.snoc b y i = Fin.snoc b y j

The equality pattern after appending matched coordinates.

theorem FirstOrder.Language.PureSet.bfEquiv_of_le_spare {X : Type u} {Y : Type v} [Language.empty.Structure X] [Language.empty.Structure Y] [Infinite X] [Finite Y] (k : ℕ) {n : ℕ} (a : Fin n → X) (b : Fin n → Y) : (∀ (i j : Fin n), a i = a j ↔ b i = b j) → k ≤ spare b → BFEquiv (↑k) n a b

Positive direction: a common pattern and k ≤ spare b give BFEquiv k.

theorem FirstOrder.Language.PureSet.not_bfEquiv_spare_succ {X : Type u} {Y : Type v} [Language.empty.Structure X] [Language.empty.Structure Y] [Infinite X] [Finite Y] (s : ℕ) {n : ℕ} (a : Fin n → X) (b : Fin n → Y) : spare b = s → ¬BFEquiv (↑(s + 1)) n a b

Failure at spare b + 1, for any tuples: the infinite side plays fresh elements until the finite side has no fresh answer.

theorem FirstOrder.Language.PureSet.bfEquiv_natCast_iff {X : Type u} {Y : Type v} [Language.empty.Structure X] [Language.empty.Structure Y] [Infinite X] [Finite Y] (k : ℕ) {n : ℕ} (a : Fin n → X) (b : Fin n → Y) : BFEquiv (↑k) n a b ↔ (∀ (i j : Fin n), a i = a j ↔ b i = b j) ∧ k ≤ spare b

The threshold: at a natural level k, equivalence holds iff the patterns agree and k ≤ spare b.

theorem FirstOrder.Language.PureSet.orbitRank_pure_eq_zero {Y : Type v} [Language.empty.Structure Y] {n : ℕ} (a : Fin n → Y) : orbitRank a = 0

Every tuple of any pure set has orbit rank 0, finite or infinite.

theorem FirstOrder.Language.PureSet.isEmpty_equiv_of_infinite_finite {X : Type u} {Y : Type v} [Language.empty.Structure X] [Language.empty.Structure Y] [Infinite X] [Finite Y] : IsEmpty (Language.empty.Equiv X Y)

No isomorphism between an infinite and a finite structure.

ℕ against Fin m

@[instance_reducible]

instance FirstOrder.Language.PureSet.instStructureNat : Language.empty.Structure ℕ

Equations

• FirstOrder.Language.PureSet.instStructureNat = FirstOrder.Language.emptyStructure

@[instance_reducible]

instance FirstOrder.Language.PureSet.instStructureFin (m : ℕ) : Language.empty.Structure (Fin m)

Equations

• FirstOrder.Language.PureSet.instStructureFin m = FirstOrder.Language.emptyStructure

theorem FirstOrder.Language.PureSet.spare_elim0 (m : ℕ) : spare Fin.elim0 = m

theorem FirstOrder.Language.PureSet.bfEquiv_nat_fin_iff (k m : ℕ) : BFEquiv (↑k) 0 Fin.elim0 Fin.elim0 ↔ k ≤ m

Empty tuples of ℕ and Fin m are equivalent at k iff k ≤ m.

theorem FirstOrder.Language.PureSet.not_bfEquiv_nat_fin_succ (m : ℕ) : ¬BFEquiv (↑(m + 1)) 0 Fin.elim0 Fin.elim0

Failure pinned at m + 1.