Reductio.lean — FrcCore

1import FrcCore.Nat2import FrcCore.Pigeonhole3import FrcCore.Shell4import FrcCore.Frame5import FrcCore.Sum6import FrcCore.Theme.Logic7import FrcCore.Keys.Logic89/-!10# 5-red — paradoxes of infinity as reductio: the ledger predicates with no axioms1112Rows of the predicate ledger of *Paradoxes of Infinity as Reductio ad Absurdum* (tree `5-reductio-20260706`).13What the finite exit asserts is finite mathematics, and it is proved here on the kernel alone: the bounded14stability schema for an explicit language of `Δ₀` formulas with two evaluators (over `ℕ`, and in a frame `W_N`15where overflow makes an atom false) — every formula takes its standard value in every frame above its bound;16the counting behind the migration (fewer than `s^(K+1)` records of length `≤ K`, so a bounded part cannot mirror17a larger frame); the pigeonhole behind periodic König and the horizon separation of bounded halting (an18iteration on `n` states repeats within `n` steps, so halting is decided by `n` steps); Cantor's theorem on the19finite frame; definable choice by the least element; the equivariant obstruction on `𝔽₅`.  Every declaration20prints "does not depend on any axioms".2122Since the ledger migration (task LM17) the language, its evaluation, the stability schema and the counting live in23the logic theme (`Theme/Logic.lean`, namespace `FRC.Logic`); this module keeps the worked instance, the obstruction on24`𝔽₅` and every old name as an alias.25-/2627namespace FRC.Reductio2829section30open FRC.Logic3132/-! ### 5:B6 — the worked instance: Goldbach below 10 in the frames -/3334/-- The numeral `n` as a term, `((0 + 1) + 1) + …`. -/35def num : Nat → Term36  | 0 => Term.zero37  | n + 1 => Term.add (num n) Term.one3839/-- `∃ x ≤ t, φ` as `¬∀ x ≤ t, ¬φ`. -/40def bex (t : Term) (φ : Form) : Form := Form.neg (Form.ball t (Form.neg φ))4142/-- "variable `i` is prime": `1 < x ∧ ∀ d ≤ x, ∀ e ≤ x, ¬(d·e = x ∧ d ≠ 1 ∧ d ≠ x)`. -/43def prime (i : Nat) : Form :=44  Form.conj (Form.lt Term.one (Term.var i))45    (Form.ball (Term.var i) (Form.ball (Term.var (i + 1))46      (Form.neg (Form.conj (Form.eq (Term.mul (Term.var 1) (Term.var 0)) (Term.var (i + 2)))47        (Form.conj (Form.neg (Form.eq (Term.var 1) Term.one)) (Form.neg (Form.eq (Term.var 1) (Term.var (i + 2)))))))))4849/-- "variable `0` is even": `∃ k ≤ m, k + k = m`. -/50def even0 : Form := bex (Term.var 0) (Form.eq (Term.add (Term.var 0) (Term.var 0)) (Term.var 1))5152/-- Goldbach below `M`: every even `m ≤ M` with `4 ≤ m` is a sum of two primes `x, y ≤ m` — a `Δ₀` sentence. -/53def goldbach (M : Nat) : Form :=54  Form.ball (num M) (Form.neg (Form.conj (Form.conj even0 (Form.neg (Form.lt (Term.var 0) (num 4))))55    (Form.neg (bex (Term.var 0) (bex (Term.var 1)56      (Form.conj (prime 1) (Form.conj (prime 0) (Form.eq (Term.add (Term.var 1) (Term.var 0)) (Term.var 2)))))))))5758/-- 5:B6 (Example schema-instance) — Goldbach below `10` is true over `ℕ`, decided by the kernel. -/59theorem goldbach_ten : evalF (fun _ => 0) (goldbach 10) = true := by decide +kernel6061/-- 5:B6 (Example schema-instance) — its bound: the evaluation touches `100 = 10·10` and nothing larger. -/62theorem goldbach_ten_bound : boundF (fun _ => 0) (goldbach 10) = 100 := by decide +kernel6364/-- 5:B6 (Example schema-instance) — hence, by `stable`, every frame `W_N` with `N > 100` gives the sentence its65standard value; `W_101` does so by direct evaluation as well. -/66theorem goldbach_ten_frame : evalF? 101 (fun _ => 0) (goldbach 10) = true := by decide +kernel6768/-- 5:B6 — the schema instance `St(goldbach 10, M)` for every `M`: all frames `100 < N` agree with `ℕ`. -/69theorem goldbach_ten_stable (N : Nat) (hN : 100 < N) : evalF? N (fun _ => 0) (goldbach 10) = true := by70  rw [stable N (goldbach 10) (fun _ => 0) (goldbach_ten_bound ▸ hN)]; exact goldbach_ten7172/-! ### 5:E4 — the equivariant obstruction on `𝔽₅` -/7374/-- 5:E4 (Example basis-obstruction) — on the line over `𝔽₅` the map `v ↦ −v` fixes no basis: `−v ≠ v` for every75`v ≠ 0`; over `𝔽₂` it fixes `1`, so the obstruction is arithmetic. -/76theorem obstruction_five :77    (-(1 : Shell 5) ≠ 1) ∧ (-(2 : Shell 5) ≠ 2) ∧ (-(3 : Shell 5) ≠ 3) ∧ (-(4 : Shell 5) ≠ 4) ∧ (-(1 : Shell 2) = 1) := by78  decide7980/-! ## Old names (ledger migration, task LM17): the declarations moved to the themes, each under its old name -/81end8283section aliases84variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}8586/-- `mx a b`, the larger of two naturals, with its two bounds proved from the definition. -/87@[reducible] def mx (a b : Nat) : Nat :=88  FRC.Logic.mx a b8990theorem le_mx_left (a b : Nat) : a ≤ mx a b :=91  FRC.Logic.le_mx_left a b9293theorem le_mx_right (a b : Nat) : b ≤ mx a b :=94  FRC.Logic.le_mx_right a b9596theorem lt_of_mx_lt_left {a b N : Nat} (h : mx a b < N) : a < N :=97  FRC.Logic.lt_of_mx_lt_left h9899theorem lt_of_mx_lt_right {a b N : Nat} (h : mx a b < N) : b < N :=100  FRC.Logic.lt_of_mx_lt_right h101102/-- Terms: variables (de Bruijn indices), `0`, `1`, sum, product. -/103@[reducible] def Term := @FRC.Logic.Term104105/-- `Δ₀` formulas: atoms `s = t`, `s < t`, negation, conjunction, and the bounded quantifier `∀ x ≤ t, φ`106(`x` is variable `0` in `φ`, the other variables shift up; `t` is read in the outer environment). -/107@[reducible] def Form := @FRC.Logic.Form108109/-- The environment extended by a value for variable `0`. -/110@[reducible] def cons (x : Nat) (env : Nat → Nat) : Nat → Nat :=111  FRC.Logic.cons x env112113/-- Terms over `ℕ`. -/114@[reducible] def evalT (env : Nat → Nat) : Term → Nat :=115  FRC.Logic.evalT env116117/-- `f 0 && … && f (n − 1)`. -/118@[reducible] def allBelow (f : Nat → Bool) : Nat → Bool :=119  FRC.Logic.allBelow f120121/-- Formulas over `ℕ` (the standard value). -/122@[reducible] def evalF (env : Nat → Nat) : Form → Bool :=123  FRC.Logic.evalF env124125/-- Terms in the frame `W_N`: a value is defined only while every intermediate value stays below `N`126(overflow: `A(x, y, z)` fails for `x + y ≥ N`). -/127@[reducible] def evalT? (N : Nat) (env : Nat → Nat) : Term → Option Nat :=128  FRC.Logic.evalT? N env129130/-- Formulas in the frame `W_N`: an atom with an undefined term is false, a bounded quantifier is guarded by131the definedness of its bound (the transcription `φ*` of the paper). -/132@[reducible] def evalF? (N : Nat) (env : Nat → Nat) : Form → Bool :=133  FRC.Logic.evalF? N env134135/-- The largest value a term's evaluation touches. -/136@[reducible] def boundT (env : Nat → Nat) : Term → Nat :=137  FRC.Logic.boundT env138139/-- `max (f 0, …, f (n − 1))`. -/140@[reducible] def maxBelow (f : Nat → Nat) : Nat → Nat :=141  FRC.Logic.maxBelow f142143/-- `t(φ)`, the largest integer referenced in the evaluation of `φ` over `ℕ`. -/144@[reducible] def boundF (env : Nat → Nat) : Form → Nat :=145  FRC.Logic.boundF env146147theorem le_maxBelow (f : Nat → Nat) : ∀ {n x : Nat}, x < n → f x ≤ maxBelow f n :=148  FRC.Logic.le_maxBelow f149150theorem allBelow_congr {f g : Nat → Bool} : ∀ {n : Nat}, (∀ x, x < n → f x = g x) → allBelow f n = allBelow g n :=151  FRC.Logic.allBelow_congr152153/-- 5:B6 (terms) — below its bound a term is defined in the frame, with its standard value. -/154theorem evalT_frame (N : Nat) (env : Nat → Nat) : ∀ (t : Term), boundT env t < N → evalT? N env t = some (evalT env t) :=155  FRC.Logic.evalT_frame N env156157/-- 5:B6 (Theorem stability, schema form) — every `Δ₀` formula takes its standard value in every frame `W_N`158with `N > t(φ)`: `W_N ⊨ φ* ⟺ ℕ ⊨ φ`, for every environment, by induction on the formula. -/159theorem stable (N : Nat) : ∀ (φ : Form) (env : Nat → Nat), boundF env φ < N → evalF? N env φ = evalF env φ :=160  FRC.Logic.stable N161162/-- The number of strings of length at most `K` over `s` letters, `Σ_{i ≤ K} s^i`. -/163@[reducible] def records (s : Nat) : Nat → Nat :=164  FRC.Logic.records s165166/-- 5:C2 (the count) — fewer than `s^(K+1)` records exist for an alphabet of `s ≥ 2` letters. -/167theorem records_lt (s : Nat) (hs : 2 ≤ s) : ∀ K, records s K < s ^ (K + 1) :=168  FRC.Logic.records_lt s hs169170/-- 5:C2 (Proposition mirror) — a part with fewer records than the frame has elements holds no injective171representation of the frame's domain: no `f : [0, N) → [0, R)` is injective when `R < N`. -/172theorem no_mirror {N R : Nat} (hR : R < N) (f : Nat → Nat) (hf : ∀ i, i < N → f i < R)173    (hinj : ∀ i j, i < N → j < N → f i = f j → i = j) : False :=174  FRC.Logic.no_mirror hR f hf hinj175176/-- `iter f x k = f^k x`. -/177@[reducible] def iter (f : Nat → Nat) (x : Nat) : Nat → Nat :=178  FRC.Logic.iter f x179180theorem iter_lt (f : Nat → Nat) {n : Nat} (hf : ∀ y, y < n → f y < n) {x : Nat} (hx : x < n) :181    ∀ k, iter f x k < n :=182  FRC.Logic.iter_lt f hf hx183184theorem iter_add (f : Nat → Nat) (x : Nat) (i : Nat) : ∀ k, iter f x (i + k) = iter f (iter f x i) k :=185  FRC.Logic.iter_add f x i186187/-- 5:E5, 5:C5 (Lemma periodic König, the pigeonhole) — on `n` states the iteration from `x` revisits a state within188`n` steps: some `i < j ≤ n` have `f^i x = f^j x`. -/189theorem repeat_below (f : Nat → Nat) (n : Nat) (hf : ∀ y, y < n → f y < n) (x : Nat) (hx : x < n) :190    ∃ i j, i < j ∧ j ≤ n ∧ iter f x i = iter f x j :=191  FRC.Logic.repeat_below f n hf x hx192193theorem sub_pos {i j : Nat} (h : i < j) : 0 < j - i :=194  FRC.Logic.sub_pos h195196/-- 5:E5 — the walk is eventually periodic: from step `i` on, period `p = j − i` with `0 < p ≤ n`,197`f^(i+k+p) x = f^(i+k) x` for every `k`. -/198theorem eventually_periodic (f : Nat → Nat) (n : Nat) (hf : ∀ y, y < n → f y < n) (x : Nat) (hx : x < n) :199    ∃ i p, 0 < p ∧ p ≤ n ∧ ∀ k, iter f x (i + k + p) = iter f x (i + k) :=200  FRC.Logic.eventually_periodic f n hf x hx201202/-- 5:C5 (horizon separation) — a run on `n` states reaches a state `h` iff it reaches it within `n` steps: halting for bounded space is decided from above by `n` steps of simulation. -/203theorem halts_iff_halts_below (f : Nat → Nat) (n : Nat) (hf : ∀ y, y < n → f y < n) (h : Nat)204    (x : Nat) (hx : x < n) : (∃ k, iter f x k = h) ↔ ∃ k, k ≤ n ∧ iter f x k = h :=205  FRC.Logic.halts_iff_halts_below f n hf h x hx206207/-- 5:D3 (Remark, the external diagonal) — Cantor's theorem holds in every finite frame: `n < 2^n`. -/208theorem cantor_finite (n : Nat) : n < 2 ^ n :=209  FRC.Logic.cantor_finite n210211/-- The least `x < n` with `P x`, if any: the choice function `ch(A) = min A` of Definition global-choice. -/212@[reducible] def leastBelow (P : Nat → Bool) : Nat → Option Nat :=213  FRC.Logic.leastBelow P214215/-- 5:E1 — a nonempty family has a choice: if some `x < n` has `P x`, `leastBelow P n` is defined. -/216theorem leastBelow_some (P : Nat → Bool) : ∀ (n x : Nat), x < n → P x = true → ∃ y, leastBelow P n = some y :=217  FRC.Logic.leastBelow_some P218219/-- 5:E1 (Proposition finite-choice) — the choice is a member, below the bound, and the least one. -/220theorem leastBelow_spec (P : Nat → Bool) : ∀ (n x : Nat), leastBelow P n = some x →221    x < n ∧ P x = true ∧ ∀ y, y < x → P y = false :=222  FRC.Logic.leastBelow_spec P223224/-- 5:E2 (Lemma periodic choice) — the choice depends on the set alone: pointwise equal families choose alike,225so an equality-periodic family `A_{i+N} = A_i` has a choice function of the same period. -/226theorem leastBelow_congr {P Q : Nat → Bool} : ∀ {n : Nat}, (∀ x, x < n → P x = Q x) → leastBelow P n = leastBelow Q n :=227  FRC.Logic.leastBelow_congr228229end aliases230231-- Ledger predicates of 5-reductio (generated by make_predicates.py from docs/5-reductio/5-reductio-ledger.json; edit the ledger, not this section)232/-- 5:B6 (p05010) — Bounded stability, schema form: a $\Delta_0$ sentence $\varphi$ with bound $t(\varphi)$ has $W_N\models\varphi^{*}\iff\N\models\varphi$ for every $N>t(\varphi)$, each instance $\mathrm{St}(\varphi,M)$ a finite conjunction of finite checks; proved for an explicit $\Delta_0$ language with $t(\varphi)$ computed; Goldbach below $20$ has $t=400$ and value true (below $10$, $t=100$, decided by the kernel). -/233theorem p05010 : (∀ (N : Nat) (φ : FRC.Reductio.Form) (env : Nat → Nat), FRC.Reductio.boundF env φ < N → FRC.Reductio.evalF? N env φ = FRC.Reductio.evalF env φ) ∧ (∀ (N : Nat) (env : Nat → Nat) (t : FRC.Reductio.Term), FRC.Reductio.boundT env t < N → FRC.Reductio.evalT? N env t = some (FRC.Reductio.evalT env t)) ∧ ∀ (N : Nat), (100 : Nat) < N → FRC.Reductio.evalF? N (fun x => (0 : Nat)) (FRC.Reductio.goldbach (10 : Nat)) = true :=234  And.intro @FRC.Reductio.stable (And.intro @FRC.Reductio.evalT_frame (@FRC.Reductio.goldbach_ten_stable))235/-- 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). -/236theorem p05013 : (∀ (s : Nat), (2 : Nat) ≤ s → ∀ (K : Nat), FRC.Reductio.records s K < s ^ (K + (1 : Nat))) ∧ ∀ {N R : Nat}, R < N → ∀ (f : Nat → Nat), (∀ (i : Nat), i < N → f i < R) → (∀ (i j : Nat), i < N → j < N → f i = f j → i = j) → False :=237  @FRC.Ledger.p05013238/-- 5:C5 (p05016) — Horizon separation: halting for machines of bounded space $K$ is decided from above within $|Q|\,K\,s^{K}$ steps (a configuration repeats) and never from within (diagonalisation); Turing's theorem is an external non-existence theorem, classified with Cantor's, not an instance of the bundle. -/239theorem p05016 : (∀ (f : Nat → Nat) (n : Nat), (∀ (y : Nat), y < n → f y < n) → ∀ (x : Nat), x < n → ∃ i j, i < j ∧ j ≤ n ∧ FRC.Reductio.iter f x i = FRC.Reductio.iter f x j) ∧ ∀ (f : Nat → Nat) (n : Nat), (∀ (y : Nat), y < n → f y < n) → ∀ (h x : Nat), x < n → ((∃ k, FRC.Reductio.iter f x k = h) ↔ ∃ k, k ≤ n ∧ FRC.Reductio.iter f x k = h) :=240  @FRC.Ledger.p05016241/-- 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. -/242theorem p05019 : ∀ (n : Nat), n < (2 : Nat) ^ n :=243  @FRC.Ledger.p05019244/-- 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. -/245theorem p05027 : (∀ (P : Nat → Bool) (n x : Nat), FRC.Reductio.leastBelow P n = some x → x < n ∧ P x = true ∧ ∀ (y : Nat), y < x → P y = false) ∧ ∀ (P : Nat → Bool) (n x : Nat), x < n → P x = true → ∃ y, FRC.Reductio.leastBelow P n = some y :=246  @FRC.Ledger.p05027247/-- 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. -/248theorem p05028 : ∀ {P Q : Nat → Bool} {n : Nat}, (∀ (x : Nat), x < n → P x = Q x) → FRC.Reductio.leastBelow P n = FRC.Reductio.leastBelow Q n :=249  @FRC.Ledger.p05028250/-- 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. -/251theorem p05030 : (-1 : FRC.Shell (5 : Nat)) ≠ (1 : FRC.Shell (5 : Nat)) ∧ (-2 : FRC.Shell (5 : Nat)) ≠ (2 : FRC.Shell (5 : Nat)) ∧ (-3 : FRC.Shell (5 : Nat)) ≠ (3 : FRC.Shell (5 : Nat)) ∧ (-4 : FRC.Shell (5 : Nat)) ≠ (4 : FRC.Shell (5 : Nat)) ∧ (-1 : FRC.Shell (2 : Nat)) = (1 : FRC.Shell (2 : Nat)) :=252  @FRC.Reductio.obstruction_five253/-- 5:E5 (p05031) — Periodic K\H{o}nig: in a finite digraph with out-degree $\ge1$ the greedy walk repeats a vertex within $|D|+1$ steps and is eventually periodic with period $\le|D|$ --- the pigeonhole on an iteration over finitely many states. -/254theorem p05031 : (∀ (f : Nat → Nat) (n : Nat), (∀ (y : Nat), y < n → f y < n) → ∀ (x : Nat), x < n → ∃ i j, i < j ∧ j ≤ n ∧ FRC.Reductio.iter f x i = FRC.Reductio.iter f x j) ∧ ∀ (f : Nat → Nat) (n : Nat), (∀ (y : Nat), y < n → f y < n) → ∀ (x : Nat), x < n → ∃ i p, (0 : Nat) < p ∧ p ≤ n ∧ ∀ (k : Nat), FRC.Reductio.iter f x (i + k + p) = FRC.Reductio.iter f x (i + k) :=255  @FRC.Ledger.p05031256-- end ledger predicates257258end FRC.Reductio259