Reductio.lean — FrcLedger

1import Mathlib2import FrcLedger.Theme.Logic3import FrcLedger.Keys.Logic45/-!6# 5-red — paradoxes of infinity as reductio: the ledger predicates in Lean (2026-09-17)78Rows of the predicate ledger of *Paradoxes of Infinity as Reductio ad Absurdum* (tree `5-reductio-20260706`).9The finite exit's properties for any finite structure in any language (the complete theory is complete, and10truth is decided by evaluation); the infinitude of every structure with an injective successor missing zero11(no finite frame interprets `Q`); Cantor's theorem; the counting of the migration propositions and the vanishing12certified fraction; definable and periodic choice; the equivariant section criterion on an orbit; the13obstruction on `𝔽₅`; the finite disappearance of the choice paradoxes; Dedekind's embedding.  Classical (tier 2)14on Mathlib's hierarchy; the finite content is proved with no axioms in `FrcCore/Reductio.lean`.15-/1617open FirstOrder FirstOrder.Language1819namespace FRC.Reductio2021section22open FRC.Logic2324section migration2526open Filter Topology in27/-- 5:C3 (Proposition fraction): the certified fraction `s^(K+1) / ⌊c^L/2⌋` of a bounded agent tends to zero as28the cohort length `L` grows, for any capacity and any `c > 1`. -/29theorem certified_fraction_tendsto (A c : ℝ) (hc : 1 < c) :30    Tendsto (fun L : ℕ => A / c ^ L) atTop (𝓝 0) :=31  tendsto_const_nhds.div_atTop (tendsto_pow_atTop_atTop_of_one_lt hc)3233end migration3435section choice3637variable {U : Type*} [LinearOrder U]3839/-- 5:E1 (Proposition finite-choice): on a finite universe with a canonical order, `ch(A) = min A` is a member of40every nonempty `A` — choice is a definable theorem, not a postulate. -/41theorem finite_choice (A : Finset U) (hA : A.Nonempty) : A.min' hA ∈ A := Finset.min'_mem A hA4243/-- 5:E2 (Lemma periodic-equality): for an equality-periodic family `A (i + N) = A i` the choice `min A i` is44periodic with the same period. -/45theorem periodic_choice (A : ℤ → Finset U) (N : ℤ) (hN : ∀ i, A (i + N) = A i) (i : ℤ) :46    (A (i + N)).min = (A i).min := by rw [hN]4748variable {G I A : Type*} [Group G] [MulAction G I] [MulAction G A]4950/-- 5:E3 (Theorem equivariant-choice, one orbit): for a `G`-family `π : A → I` over a transitive `G`-set `I`, an51equivariant section exists iff the stabiliser of a base point `i₀` fixes some point of its fibre. -/52theorem equivariant_section_iff [MulAction.IsPretransitive G I] (π : A → I)53    (hπ : ∀ (g : G) (a : A), π (g • a) = g • π a) (i₀ : I) :54    (∃ s : I → A, (∀ i, π (s i) = i) ∧ ∀ (g : G) (i : I), s (g • i) = g • s i) ↔55      ∃ a, π a = i₀ ∧ ∀ g ∈ MulAction.stabilizer G i₀, g • a = a := by56  constructor57  · rintro ⟨s, hs, heq⟩58    refine ⟨s i₀, hs i₀, fun g hg => ?_⟩59    rw [← heq, MulAction.mem_stabilizer_iff.mp hg]60  · rintro ⟨a, ha, hfix⟩61    classical62    choose g hg using fun i => MulAction.exists_smul_eq G i₀ i63    -- `s i := g i • a`, where `g i • i₀ = i`; independence of the choice is the stabiliser condition64    have key : ∀ (h : G) (i : I), h • i₀ = i → h • a = g i • a := by65      intro h i hi66      have hst : (g i)⁻¹ * h ∈ MulAction.stabilizer G i₀ := by67        rw [MulAction.mem_stabilizer_iff, mul_smul, hi]68        have e := inv_smul_smul (g i) i₀69        rw [hg i] at e70        exact e71      have := hfix _ hst72      rw [mul_smul] at this73      calc h • a = g i • (g i)⁻¹ • h • a := (smul_inv_smul _ _).symm74        _ = g i • a := by rw [this]75    refine ⟨fun i => g i • a, fun i => ?_, fun h i => ?_⟩76    · rw [hπ, ha, hg]77    · show g (h • i) • a = h • (g i • a)78      rw [← mul_smul]79      exact (key (h * g i) (h • i) (by rw [mul_smul, hg])).symm8081/-- 5:E4 (Example basis-obstruction): on the line over `𝔽₅` the involution `v ↦ −v` fixes no basis — `−v ≠ v`82for every `v ≠ 0` — while over `𝔽₂` it fixes `1`: the obstruction is arithmetic. -/83theorem obstruction_five : (∀ v : ZMod 5, v ≠ 0 → -v ≠ v) ∧ (-(1 : ZMod 2) = 1) := by decide8485/-- 5:E8 (Banach–Tarski disappears): a finite nonempty set cannot be doubled — there is no injection86`X ⊕ X ↪ X`, so no decomposition reassembles two copies of `X` from pieces of `X`. -/87theorem no_doubling {X : Type*} [Fintype X] [Nonempty X] : IsEmpty (X ⊕ X ↪ X) := by88  constructor89  intro f90  have h := Fintype.card_le_of_embedding f91  rw [Fintype.card_sum] at h92  have : 0 < Fintype.card X := Fintype.card_pos93  omega9495/-- 5:E8 (ultrafilters): on a finite set every ultrafilter is principal. -/96theorem ultrafilter_principal {X : Type*} [Finite X] (f : Ultrafilter X) : ∃ a, f = pure a :=97  Ultrafilter.eq_pure_of_finite f9899end choice100101section determinacy102103/-- 5:D8 (Proposition finiteness, the finite direction): over a finite domain a second-order quantifier over all104subsets is a finite conjunction — decided by exhaustive evaluation. -/105def decideAllSubsets {M : Type*} [Fintype M] [DecidableEq M] (P : Finset M → Prop) [DecidablePred P] :106    Decidable (∀ S : Finset M, P S) := Fintype.decidableForallFintype107108/-- 5:D8 (the infinite direction, its first step): an infinite domain carries a copy of `ℕ` — Dedekind's109embedding, from which the reduction of true second-order arithmetic proceeds. -/110theorem nat_embeds {M : Type*} [Infinite M] : Nonempty (ℕ ↪ M) := ⟨Infinite.natEmbedding M⟩111112end determinacy113114end115116/-! ## Old names (ledger migration, task LM17): the declarations moved to the themes, each under its old name -/117118section frames_aliases119variable {L : Language} {M : Type*} [L.Structure M]120121/-- 5:B5, 5:B3 (Proposition frame-complete, completeness): the theory of any structure — a finite frame `W_N` among122them — is complete: every sentence or its negation is in it. -/123theorem theory_complete [Nonempty M] : (L.completeTheory M).IsComplete :=124  FRC.Logic.theory_complete125126/-- 5:B5 (decidability): in a finite structure with decidable relations, the truth of every bounded formula is127decided by evaluation — the quantifiers range over the finitely many elements. -/128@[reducible] def decRealize {α : Type*} [Fintype M] [DecidableEq M]129    (hR : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), Decidable (Structure.RelMap R x)) :130    ∀ {n : ℕ} (φ : L.BoundedFormula α n) (v : α → M) (xs : Fin n → M), Decidable (φ.Realize v xs) :=131  FRC.Logic.decRealize hR132133/-- 5:B5 (Proposition frame-complete, decidability): membership in the theory of a finite structure is decided134by evaluating the sentence. -/135@[reducible] def decTheory [Fintype M] [DecidableEq M]136    (hR : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), Decidable (Structure.RelMap R x)) :137    DecidablePred (· ∈ L.completeTheory M) :=138  FRC.Logic.decTheory hR139140/-- 5:B3 (Theorem witnessed, exit 2 — `Th(W_N)` does not interpret `Q`): a structure with an injective141successor that never reaches zero is infinite; every model of `Q` is such a structure, and a finite frame's142definable quotients are finite. -/143theorem infinite_of_succ {A : Type*} (S : A → A) (z : A) (hinj : Function.Injective S) (hz : ∀ x, S x ≠ z) :144    Infinite A :=145  FRC.Logic.infinite_of_succ S z hinj hz146147end frames_aliases148149/-- 5:D3 (Remark cantor-diagonal): Cantor's theorem is an external diagonal — no map from a set onto its power150set, in every finite frame as `n < 2^n`. -/151theorem cantor (α : Type*) (f : α → Set α) : ¬ Function.Surjective f :=152  FRC.Logic.cantor α f153154/-- 5:D3: on the frame, `n < 2^n`. -/155theorem cantor_finite (n : ℕ) : n < 2 ^ n :=156  FRC.Logic.cantor_finite n157158/-- 5:C2 (Proposition mirror, the count): fewer than `s^(K+1)` strings of length at most `K` exist over an159alphabet of `s ≥ 2` letters. -/160theorem records_lt (s K : ℕ) (hs : 2 ≤ s) : ∑ i ∈ Finset.range (K + 1), s ^ i < s ^ (K + 1) :=161  FRC.Logic.records_lt s K hs162163/-- 5:C2 (Proposition mirror): a part with fewer distinguishable records than the frame has elements admits no164injective representation of the frame's domain. -/165theorem no_mirror {A R : Type*} [Fintype A] [Fintype R] (h : Fintype.card R < Fintype.card A) (f : A → R) :166    ¬ Function.Injective f :=167  FRC.Logic.no_mirror h f168169170-- Ledger predicates of 5-reductio (generated by make_predicates.py from docs/5-reductio/5-reductio-ledger.json; edit the ledger, not this section)171/-- 5:B3 (p05007) — Witnessed independence: every three-element subset is satisfiable --- $Q$ itself ($\neg$Cmp, consistent by finitary means, the superexponential cost exact); $\mathrm{Th}(W_N)$ ($\neg$IR: consistent, complete, decidable, singly axiomatised, interpreting no $Q$ since every model of $Q$ is infinite); the inconsistent extension ($\neg$Cns); true arithmetic ($\neg$Eff). Four legs, all load-bearing. -/172theorem p05007 : (∀ {A : Type u_1} (S : A → A) (z : A), Function.Injective S → (∀ (x : A), S x ≠ z) → Infinite A) ∧ ∀ {L : FirstOrder.Language} {M : Type u_4} [L.Structure M] [Nonempty M], (L.completeTheory M).IsComplete :=173  @FRC.LedgerML.p05007174/-- 5:B5 (p05009) — Per-frame completeness: $\mathrm{Th}(W_N)$ is consistent, complete and decidable, axiomatised by the categorical sentence $\sigma_N$; truth in any finite structure is decided by evaluation, and the theory of any structure is complete. Cited definitions (not proofs): FRC.Reductio.decRealize, FRC.Reductio.decTheory. -/175theorem p05009 : ∀ {L : FirstOrder.Language} {M : Type u_3} [L.Structure M] [Nonempty M], (L.completeTheory M).IsComplete :=176  @FRC.LedgerML.p05009177/-- 5:C2 (p05013) — No internal mirror: fewer than $s^{K+1}$ records exist, so an agent with $s^{K+1}<N$ holds no injective representation of the domain of $W_N$ --- a proper part cannot mirror the whole (pigeonhole). -/178theorem p05013 : (∀ (s K : ℕ), (2 : ℕ) ≤ s → ∑ i ∈ Finset.range (K + (1 : ℕ)), s ^ i < s ^ (K + (1 : ℕ))) ∧ ∀ {A : Type u_1} {R : Type u_2} [Fintype A] [Fintype R], Fintype.card R < Fintype.card A → ∀ (f : A → R), ¬Function.Injective f :=179  @FRC.LedgerML.p05013180/-- 5:C3 (p05014) — Vanishing certified fraction: at least $c^{L}$ normal-form sentences of length $\le L$, half of each cohort frame truths by completeness, fewer than $s^{K+1}$ certified, so the certified fraction is at most $s^{K+1}/\lfloor c^{L}/2\rfloor\to0$. -/181theorem p05014 : ∀ (A c : ℝ), (1 : ℝ) < c → Filter.Tendsto (fun L => A / c ^ L) Filter.atTop (nhds (0 : ℝ)) :=182  @FRC.Reductio.certified_fraction_tendsto183/-- 5:D3 (p05019) — Diagonal normal form: $\{$Eff, Cns, Cmp, IR$\}$ inconsistent (B2), Tarski a variant with the truth predicate for Cmp; the diagonal is a theorem when external --- Cantor's theorem, $n<2^{n}$ on every frame, uncountability, halting --- and a paradox engine only over an internalised registry with completeness demanded. -/184theorem p05019 : (∀ (α : Type u_1) (f : α → Set α), ¬Function.Surjective f) ∧ ∀ (n : ℕ), n < (2 : ℕ) ^ n :=185  @FRC.LedgerML.p05019186/-- 5:D8 (p05024) — Finiteness of determinate totalities: in ZF with every infinite set Dedekind-infinite, a structure satisfies Det iff it is finite --- finite: the full higher-order theory decided by exhaustive evaluation; infinite: a copy of $\N$ inside gives an effective reduction of true second-order arithmetic, which is not arithmetical. The real field's first-order tameness is silence about its subsets. Cited definitions (not proofs): FRC.Reductio.decideAllSubsets. -/187theorem p05024 : ∀ {M : Type u_1} [Infinite M], Nonempty (ℕ ↪ M) :=188  @FRC.Reductio.nat_embeds189/-- 5:E1 (p05027) — Global choice on a finite universe: with a canonical order, $\operatorname{ch}(A)=\min A$ is a uniform pointwise choice rule; over a fixed finite base AC is a definable theorem; finite products are nonempty without it. -/190theorem p05027 : ∀ {U : Type u_1} [LinearOrder U] (A : Finset U) (hA : A.Nonempty), A.min' hA ∈ A :=191  @FRC.Reductio.finite_choice192/-- 5:E2 (p05028) — Periodic choice: an equality-periodic family $A_{i+N}=A_i$ has the choice $f(i)=\operatorname{ch}(A_i)$ of the same period; group-periodic families as equivariant surjections $\pi:A\to I$ with equivariant sections. -/193theorem p05028 : ∀ {U : Type u_1} [LinearOrder U] (A : ℤ → Finset U) (N : ℤ), (∀ (i : ℤ), A (i + N) = A i) → ∀ (i : ℤ), (A (i + N)).min = (A i).min :=194  @FRC.Reductio.periodic_choice195set_option linter.defProp false in196/-- 5:E3 (p05029) — Equivariant periodic choice: a $G$-equivariant section exists iff each stabiliser action $G_i\curvearrowright A_i$ has a fixed point (one orbit at a time); the Fraenkel--Mostowski mechanism in positive form. -/197def p05029 := @FRC.Reductio.equivariant_section_iff198/-- 5:E4 (p05030) — The definable basis: every subspace of a finite vector space has the greedy $\min$-basis, one definable function on all subspaces; the equivariant obstruction --- $\Z/2$ acting by $v\mapsto-v$ on the line over $\F_5$ fixes no basis ($-v\neq v$), over $\F_2$ it does: arithmetic, not formal. -/199theorem p05030 : (∀ (v : ZMod (5 : ℕ)), v ≠ (0 : ZMod (5 : ℕ)) → -v ≠ v) ∧ (-1 : ZMod (2 : ℕ)) = (1 : ZMod (2 : ℕ)) :=200  @FRC.Reductio.obstruction_five201/-- 5:E8 (p05034) — The choice paradoxes vanish: on a finite set counting measure is complete and invariant, no decomposition doubles the set ($X\sqcup X$ does not inject into $X$), and every ultrafilter is principal; periodic variants inherit this on one period. -/202theorem p05034 : (∀ {X : Type u_1} [Fintype X] [Nonempty X], IsEmpty (X ⊕ X ↪ X)) ∧ ∀ {X : Type u_2} [Finite X] (f : Ultrafilter X), ∃ a, f = pure a :=203  And.intro @FRC.Reductio.no_doubling (@FRC.Reductio.ultrafilter_principal)204-- end ledger predicates205206end FRC.Reductio207