Theme/Sets.lean — FrcCore

1import FrcCore.Theme.Logic23/-!4# The logic theme — finite sets: the antinomy as a theorem, counting measure, no doubling, principal ultrafilters56The finite witnesses of 5-reductio's normal forms (21 October 2026): the antinomy normal form as a theorem of7separation, abstractly for any membership relation and on hereditarily finite sets built as finite trees (5:D2,85:D5); the iterated singletons `∅, {∅}, {{∅}}, …`, pairwise distinct and outrunning every set (5:D9); counting9measure on `[0, n)` — total, additive, invariant under every bijection (5:E8, 5:D9, 5:D5); no injection of `X ⊔ X`10into `X` (5:E8); every ultrafilter on a finite set is principal (5:E8). No Mathlib, no axioms, no classical logic:11the ultrafilter is Boolean-valued and its point is found by bounded search.12-/1314namespace FRC.Sets1516open FRC.Logic1718/-! ### 5:D2 — Russell's argument as a theorem of separation -/1920/-- 5:D2, 5:D5 (Proposition antinomy-NF, the theorem) — for any membership relation `M`, no class `r` satisfies21`x ∈ r ↔ x ∉ x` for every `x`: `r ∈ r ↔ r ∉ r` is contradictory. The antinomy is a theorem about the Russell class,22and a paradox only where comprehension forms it. -/23theorem no_russell_class {α : Type} (M : α → α → Prop) : ¬ ∃ r, ∀ x, M x r ↔ ¬ M x x :=24  fun ⟨r, h⟩ =>25    have hn : ¬ M r r := fun hr => (h r).mp hr hr26    hn ((h r).mpr hn)2728/-- 5:D2, 5:D5 (Proposition antinomy-NF, the inconsistent bundle) — with separation (`sep u` is `{x ∈ u | x ∉ x}` for29every `u`) no set is universal: the Russell class of a universal set would be the class of all `x ∉ x`. This is30Cns + AT + comprehension inconsistent, read on separation. -/31theorem no_universal_of_separation {α : Type} (M : α → α → Prop) (sep : α → α)32    (hsep : ∀ u x, M x (sep u) ↔ (M x u ∧ ¬ M x x)) : ¬ ∃ v, ∀ x, M x v :=33  fun ⟨v, hv⟩ => no_russell_class M ⟨sep v, fun x =>34    ⟨fun h => ((hsep v x).mp h).2, fun h => (hsep v x).mpr ⟨hv x, h⟩⟩⟩3536/-- 5:D2, 5:D5 (Proposition antinomy-NF, the witness) — bounded comprehension has no antinomy: for every set `u` the37class `r = {x ∈ u | x ∉ x}` is a set that is not a member of `u` (were `r ∈ u`, then `r ∈ r ↔ r ∉ r`). -/38theorem russell_not_mem {α : Type} (M : α → α → Prop) (u r : α) (hr : ∀ x, M x r ↔ (M x u ∧ ¬ M x x)) : ¬ M r u :=39  fun hru =>40    have hn : ¬ M r r := fun hrr => ((hr r).mp hrr).2 hrr41    hn ((hr r).mpr ⟨hru, hn⟩)4243/-! ### Hereditarily finite sets as finite trees -/4445/-- A hereditarily finite set: the finite list of its members. -/46inductive HF where47  | mk : List HF → HF4849/-- Membership in a list of sets, as a proposition. -/50def memList (x : HF) : List HF → Prop51  | [] => False52  | y :: ys => x = y ∨ memList x ys5354/-- The members of a set. -/55def HF.members : HF → List HF56  | .mk l => l5758/-- `x ∈ u`. -/59def HF.Mem (x u : HF) : Prop := memList x u.members6061mutual62/-- The rank: one more than the largest rank of a member, `0` for the empty set. -/63def HF.rank : HF → Nat64  | .mk l => rankList l65/-- The least bound above the ranks of the members of a list. -/66def rankList : List HF → Nat67  | [] => 068  | x :: xs => mx (HF.rank x + 1) (rankList xs)69end7071theorem rank_lt_of_memList {x : HF} : ∀ {l : List HF}, memList x l → HF.rank x < rankList l72  | [], h => absurd h id73  | y :: ys, h => match h with74    | Or.inl e => by75        show HF.rank x < mx (HF.rank y + 1) (rankList ys)76        rw [e]; exact Nat.lt_of_lt_of_le (Nat.lt_succ_self _) (le_mx_left _ _)77    | Or.inr h' => by78        show HF.rank x < mx (HF.rank y + 1) (rankList ys)79        exact Nat.lt_of_lt_of_le (rank_lt_of_memList h') (le_mx_right _ _)8081/-- A member has smaller rank. -/82theorem rank_lt_of_mem {x u : HF} (h : HF.Mem x u) : HF.rank x < HF.rank u := by83  match u with84  | .mk l => exact rank_lt_of_memList h8586/-- 5:D2 (Proposition antinomy-NF, the witness on hereditarily finite sets) — no set is a member of itself. -/87theorem not_mem_self (x : HF) : ¬ HF.Mem x x :=88  fun h => Nat.lt_irrefl _ (rank_lt_of_mem h)8990/-- The Russell class of `u`, `{x ∈ u | x ∉ x}`: on hereditarily finite sets it is `u` itself, since no set is a91member of itself (`mem_russell`). -/92def russell (u : HF) : HF := u9394/-- 5:D2 — the Russell class of `u` is exactly the separation `{x ∈ u | x ∉ x}`. -/95theorem mem_russell (u x : HF) : HF.Mem x (russell u) ↔ (HF.Mem x u ∧ ¬ HF.Mem x x) :=96  ⟨fun h => ⟨h, not_mem_self x⟩, fun h => h.1⟩9798/-- 5:D2, 5:D5 — every set `u` has a subset, its Russell class, that is not a member of `u`. -/99theorem russell_not_mem_hf (u : HF) : ¬ HF.Mem (russell u) u :=100  russell_not_mem HF.Mem u (russell u) (mem_russell u)101102/-- 5:D2, 5:D5 — no hereditarily finite set is universal: `v` itself is not a member of `v`. -/103theorem no_universal (v : HF) : ∃ x, ¬ HF.Mem x v := ⟨v, not_mem_self v⟩104105/-! ### 5:D9 — the iterated singletons -/106107/-- The singleton `{x}`. -/108def single (x : HF) : HF := .mk [x]109110/-- The chain `∅, {∅}, {{∅}}, …`. -/111def chain : Nat → HF112  | 0 => .mk []113  | n + 1 => single (chain n)114115theorem rank_single (x : HF) : HF.rank (single x) = HF.rank x + 1 := by116  show mx (HF.rank x + 1) 0 = HF.rank x + 1117  unfold mx; exact ite_eq_right (Nat.not_lt_zero _)118119/-- 5:D9 (Corollary AT-det) — the `n`-th iterated singleton has rank `n`. -/120theorem rank_chain : ∀ n, HF.rank (chain n) = n121  | 0 => rfl122  | n + 1 => by show HF.rank (single (chain n)) = n + 1; rw [rank_single, rank_chain n]123124/-- 5:D9 (Corollary AT-det) — the iterated singletons are pairwise distinct. -/125theorem chain_injective {a b : Nat} (h : chain a = chain b) : a = b := by126  have := congrArg HF.rank h; rwa [rank_chain, rank_chain] at this127128/-- 5:D9 (Corollary AT-det, the finite form of "a universal set is infinite") — no set holds every iterated129singleton: the one of its own rank is not among its members, since members have smaller rank. -/130theorem chain_not_mem (v : HF) : ¬ HF.Mem (chain (HF.rank v)) v :=131  fun h => Nat.lt_irrefl _ (rank_chain (HF.rank v) ▸ rank_lt_of_mem h)132133/-! ### 5:E8, 5:D9, 5:D5 — counting measure on `[0, n)` -/134135/-- The counting measure of a subset of `[0, n)`, the subset a Boolean predicate. -/136def measure (A : Nat → Bool) (n : Nat) : Nat := count A n137138theorem measure_zero (A : Nat → Bool) : measure A 0 = 0 := rfl139140theorem measure_succ (A : Nat → Bool) (n : Nat) : measure A (n + 1) = measure A n + cond (A n) 1 0 := rfl141142/-- 5:E8, 5:D9 — counting measure is total: every subset has one, at most the size of the set. -/143theorem measure_le (A : Nat → Bool) : ∀ n, measure A n ≤ n144  | 0 => Nat.le_refl 0145  | n + 1 => by146    rw [measure_succ]147    exact match h : A n with148      | true => Nat.add_le_add_right (measure_le A n) 1149      | false => Nat.le_succ_of_le (measure_le A n)150151/-- 5:E8 — the whole set has measure `n` and the empty set measure `0`. -/152theorem measure_univ (n : Nat) : measure (fun _ => true) n = n := count_full (fun _ _ => rfl)153154theorem measure_empty (n : Nat) : measure (fun _ => false) n = 0 := count_false n155156/-- 5:E8, 5:D5 (counting measure is finitely additive) — on disjoint subsets the measure of the union is the sum. -/157theorem measure_add (A B : Nat → Bool) : ∀ n, (∀ x, x < n → ¬ (A x = true ∧ B x = true)) →158    measure (fun x => A x || B x) n = measure A n + measure B n159  | 0, _ => rfl160  | n + 1, h => by161    rw [measure_succ, measure_succ, measure_succ, measure_add A B n (fun x hx => h x (Nat.lt_succ_of_lt hx))]162    cases ha : A n <;> cases hb : B n163    · rfl164    · show measure A n + measure B n + 1 = measure A n + (measure B n + 1)165      exact Nat.add_assoc _ _ _166    · show measure A n + measure B n + 1 = measure A n + 1 + measure B n167      exact Nat.add_right_comm _ _ _168    · exact absurd ⟨ha, hb⟩ (h n (Nat.lt_succ_self n))169170/-- 5:E8 — a subset and its complement share the set: `|A| + |Aᶜ| = n`. -/171theorem measure_compl (A : Nat → Bool) : ∀ n, measure A n + measure (fun x => !A x) n = n172  | 0 => rfl173  | n + 1 => by174    rw [measure_succ, measure_succ]175    cases h : A n176    · show measure A n + (measure (fun x => !A x) n + 1) = n + 1177      rw [← Nat.add_assoc, measure_compl A n]178    · show measure A n + 1 + measure (fun x => !A x) n = n + 1179      rw [Nat.add_right_comm, measure_compl A n]180181/-- The count of `A` over a list of positions. -/182def countList (A : Nat → Bool) : List Nat → Nat183  | [] => 0184  | a :: l => cond (A a) 1 0 + countList A l185186theorem countList_imageList (A : Nat → Bool) (σ : Nat → Nat) : ∀ n,187    countList A (FRC.Shell.imageList σ n) = count (fun j => A (σ j)) n188  | 0 => rfl189  | n + 1 => by190    show cond (A (σ n)) 1 0 + countList A (FRC.Shell.imageList σ n) = count (fun j => A (σ j)) n + cond (A (σ n)) 1 0191    rw [countList_imageList A σ n, Nat.add_comm]192193theorem countList_erase (A : Nat → Bool) {v : Nat} : ∀ {l : List Nat}, Pigeonhole.mem v l →194    countList A l = cond (A v) 1 0 + countList A (Pigeonhole.erase v l)195  | [], h => absurd h id196  | a :: l, h =>197    match Nat.decEq a v with198    | isTrue e => by rw [show Pigeonhole.erase v (a :: l) = l from ite_eq_left e, e]; rfl199    | isFalse e => by200        rw [show Pigeonhole.erase v (a :: l) = a :: Pigeonhole.erase v l from ite_eq_right e]201        have hm : Pigeonhole.mem v l := match h with202          | Or.inl h' => absurd h'.symm e203          | Or.inr h' => h'204        show cond (A a) 1 0 + countList A l = cond (A v) 1 0 + (cond (A a) 1 0 + countList A (Pigeonhole.erase v l))205        rw [countList_erase A hm, Nat.add_left_comm]206207/-- A count over any list of `n` distinct positions below `n` is the count over `[0, n)`. -/208theorem countList_eq_count (A : Nat → Bool) : ∀ (n : Nat) (l : List Nat), Pigeonhole.NoDup l →209    (∀ e, Pigeonhole.mem e l → e < n) → l.length = n → countList A l = count A n210  | 0, [], _, _, _ => rfl211  | 0, a :: _, _, hb, _ => absurd (hb a (Or.inl rfl)) (Nat.not_lt_zero a)212  | n + 1, l, hnd, hb, hlen => by213    have hm : Pigeonhole.mem n l := Pigeonhole.mem_of_nodup_of_length_lt (n + 1) l hnd hb hlen n (Nat.lt_succ_self n)214    rw [countList_erase A hm]215    have hb' : ∀ e, Pigeonhole.mem e (Pigeonhole.erase n l) → e < n := fun e he =>216      match Nat.lt_or_ge e n with217      | Or.inl hlt => hlt218      | Or.inr hge =>219        have : e = n := Nat.le_antisymm (Nat.le_of_lt_succ (hb e (Pigeonhole.mem_of_mem_erase he))) hge220        absurd (this ▸ he) (Pigeonhole.not_mem_erase_self n hnd)221    have hlen' : (Pigeonhole.erase n l).length = n := by222      have := Pigeonhole.length_erase_of_mem hm; rw [hlen] at this; exact Nat.succ.inj this223    rw [countList_eq_count A n (Pigeonhole.erase n l) (Pigeonhole.nodup_erase n hnd) hb' hlen']224    show cond (A n) 1 0 + count A n = count A n + cond (A n) 1 0225    exact Nat.add_comm _ _226227/-- 5:E8, 5:D9, 5:D5 (counting measure is invariant) — a bijection `σ` of `[0, n)` (injective, with values below `n`) carries228every subset to one of the same measure: `|σ⁻¹ A| = |A|`. -/229theorem measure_perm (A : Nat → Bool) (σ : Nat → Nat) (n : Nat) (hlt : ∀ j, j < n → σ j < n)230    (hinj : ∀ i j, i < n → j < n → σ i = σ j → i = j) :231    measure (fun j => A (σ j)) n = measure A n := by232  show count (fun j => A (σ j)) n = count A n233  rw [← countList_imageList]234  exact countList_eq_count A n (FRC.Shell.imageList σ n) (FRC.Shell.imageList_nodup hinj (Nat.le_refl n))235    (fun e he => match FRC.Shell.mem_imageList he with | ⟨j, hj, e'⟩ => e' ▸ hlt j hj) (FRC.Shell.imageList_length σ n)236237/-! ### 5:E8 — no decomposition doubles a finite set -/238239/-- 5:E8, 5:D5 (no paradoxical decomposition) — `X ⊔ X` does not inject into `X`: no map from `[0, 2n)` into `[0, n)`, `n ≥ 1`,240is injective. The restriction to `[0, n)` is onto (`inj_onto`), so `f n` already has a preimage below `n`. -/241theorem no_doubling (n : Nat) (hn : 0 < n) (f : Nat → Nat) (hf : ∀ x, x < 2 * n → f x < n) :242    ¬ ∀ x y, x < 2 * n → y < 2 * n → f x = f y → x = y :=243  fun hinj =>244    have hn2 : n < 2 * n := by rw [Nat.two_mul]; exact Nat.lt_add_of_pos_left hn245    have hlt : ∀ x, x < n → f x < n := fun x hx => hf x (Nat.lt_trans hx hn2)246    have hinj' : ∀ x y, x < n → y < n → f x = f y → x = y :=247      fun x y hx hy e => hinj x y (Nat.lt_trans hx hn2) (Nat.lt_trans hy hn2) e248    match inj_onto n f hlt hinj' (f n) (hf n hn2) with249    | ⟨x, hx, e⟩ => Nat.lt_irrefl n (hinj x n (Nat.lt_trans hx hn2) hn2 e ▸ hx)250251/-! ### 5:E8 — every ultrafilter on a finite set is principal -/252253/-- An ultrafilter on `[0, n)`, Boolean-valued on the subsets of `[0, n)` (Boolean predicates read below `n`): it254respects equality below `n`, excludes the empty set, is closed upward and under intersection, and holds a set or255its complement. -/256structure Ultra (n : Nat) where257  U : (Nat → Bool) → Bool258  congr : ∀ A B, (∀ x, x < n → A x = B x) → U A = true → U B = true259  proper : U (fun _ => false) = false260  up : ∀ A B, (∀ x, x < n → A x = true → B x = true) → U A = true → U B = true261  inter : ∀ A B, U A = true → U B = true → U (fun x => A x && B x) = true262  ultra : ∀ A, U A = true ∨ U (fun x => !A x) = true263264/-- The positions from `k` on, `[k, n)` within `[0, n)`. -/265def above (k : Nat) : Nat → Bool := fun y => decide (k ≤ y)266267/-- The singleton `{x}` as a predicate. -/268def pt (x : Nat) : Nat → Bool := fun y => decide (x = y)269270theorem Ultra.univ {n : Nat} (F : Ultra n) : F.U (fun _ => true) = true :=271  match F.ultra (fun _ => false) with272  | Or.inl h => absurd h (by rw [F.proper]; exact Bool.false_ne_true)273  | Or.inr h => h274275/-- `[k, n) ∖ {k} = [k + 1, n)`, pointwise. -/276theorem above_succ (k y : Nat) : (above k y && !pt k y) = above (k + 1) y :=277  match Nat.lt_or_ge y k with278  | Or.inl hlt => by279      show (decide (k ≤ y) && !decide (k = y)) = decide (k + 1 ≤ y)280      rw [decide_eq_false (Nat.not_le_of_lt hlt), decide_eq_false (Nat.not_le_of_lt (Nat.lt_succ_of_lt hlt))]; rfl281  | Or.inr hge => match Nat.eq_or_lt_of_le hge with282    | Or.inl e => by283        subst e284        show (decide (k ≤ k) && !decide (k = k)) = decide (k + 1 ≤ k)285        rw [decide_eq_true (Nat.le_refl k), decide_eq_true rfl, decide_eq_false (Nat.not_le_of_lt (Nat.lt_succ_self k))]; rfl286    | Or.inr hlt => by287        show (decide (k ≤ y) && !decide (k = y)) = decide (k + 1 ≤ y)288        have h1 : decide (k + 1 ≤ y) = true := decide_eq_true hlt289        rw [decide_eq_true (Nat.le_of_lt hlt), h1, decide_eq_false (fun e : k = y => Nat.lt_irrefl k (e ▸ hlt))]; rfl290291/-- The search: below `k` some point is in the ultrafilter, or the tail `[k, n)` is. -/292theorem Ultra.search {n : Nat} (F : Ultra n) : ∀ k, (∃ x, x < k ∧ F.U (pt x) = true) ∨ F.U (above k) = true293  | 0 => Or.inr (F.congr (fun _ => true) (above 0) (fun _ _ => rfl) F.univ)294  | k + 1 =>295    match F.search k with296    | Or.inl ⟨x, hx, h⟩ => Or.inl ⟨x, Nat.lt_succ_of_lt hx, h⟩297    | Or.inr hk =>298      match F.ultra (pt k) with299      | Or.inl h => Or.inl ⟨k, Nat.lt_succ_self k, h⟩300      | Or.inr hc =>301        Or.inr (F.congr (fun y => above k y && !pt k y) (above (k + 1)) (fun y _ => above_succ k y)302          (F.inter (above k) (fun y => !pt k y) hk hc))303304theorem and_not_self' (b : Bool) : (b && !b) = false := by cases b <;> rfl305306/-- 5:E8 (every ultrafilter on a finite set is principal) — an ultrafilter on `[0, n)` holds a point `x`, and holds a307subset exactly when the subset holds `x`. -/308theorem ultra_principal {n : Nat} (F : Ultra n) : ∃ x, x < n ∧ ∀ A, F.U A = true ↔ A x = true :=309  match F.search n with310  | Or.inr h =>311    absurd (F.congr (above n) (fun _ => false) (fun y hy => decide_eq_false (Nat.not_le_of_lt hy)) h)312      (by rw [F.proper]; exact Bool.false_ne_true)313  | Or.inl ⟨x, hx, hpt⟩ => ⟨x, hx, fun A =>314    ⟨fun hA => match h : A x with315      | true => rfl316      | false =>317        have hc : F.U (fun y => !A y) = true :=318          F.up (pt x) (fun y => !A y) (fun y _ e => by319            have e' : x = y := of_decide_eq_true e320            rw [← e', h]; rfl) hpt321        have h0 : F.U (fun y => A y && !A y) = true := F.inter A (fun y => !A y) hA hc322        absurd (F.congr (fun y => A y && !A y) (fun _ => false) (fun y _ => and_not_self' (A y)) h0)323          (by rw [F.proper]; exact Bool.false_ne_true),324     fun hAx => F.up (pt x) A (fun y _ e => by have e' : x = y := of_decide_eq_true e; rw [← e']; exact hAx) hpt⟩⟩325326end FRC.Sets327