Godel.lean — FrcCore

1import FrcCore.Nat2import FrcCore.Pigeonhole3import FrcCore.Shell4import FrcCore.Sum5import FrcCore.Theme.Logic6import FrcCore.Keys.Logic78/-!9# 25-göd — incompleteness without infinity: the ledger predicates with no axioms1011Predicates of the ledger of *Incompleteness Without Infinity* (tree `25-godel-20260614`). What the paper proves12about a fixed finite structure is finite mathematics, and its counting core is proved here on the kernel alone.1314* 25:C1 — on a finite carrier an injective map is onto, so no successor of `Q` lives there.15* 25:C5 — `m + 1` sentences admit no injective numbering into `m` elements.16* 25:D1 — a part with fewer storage states than the structure has elements identifies two of them.17* 25:D4 — a term evaluated by table lookups takes the same value in every table that agrees on the entries18  consulted (the trace argument of the wrap lemma).19* 25:E1 — every closed term over `1` and `+` with `ℓ` leaves has the value `ℓ mod p`.20* 25:E2 — the records of length at most `B` number fewer than `a^(B+1)`, and the certified fraction falls below21  every `1/N`.22* 25:F1, 25:F3 — a formula's truth depends only on variables that occur in it. It depends on fewer coordinates23  than it has symbols, and no sentence has a subformula that reads a tuple as long as the sentence.24* 25:F2 — the diagonal formula is longer than the scale of its bound tuple and than the scale its matrix reads.25* 25:F4 — an injective coding of `a^n` strings into `k`-tuples needs `a^n ≤ m^k`.26* 25:G4 — the uniform pairing prefix decides what the coded prefix decides.2728The formulas are those of the signature of `M_p` (`0`, `1`, `+`, `×`). Every declaration prints "does not depend29on any axioms".3031Since the ledger migration (task LM17) the counting core (25:C1, C5, D1, F4 and the Boolean bookkeeping) lives in the32logic theme (`Theme/Logic.lean`, namespace `FRC.Logic`); every old name stays as an alias.33-/3435namespace FRC.Godel3637section38open FRC.Logic3940/-! ### Boolean bookkeeping, from the definitions -/4142/-! ### 25:C1 — on a finite carrier an injective map is onto -/4344/-! ### 25:D1 — the part cannot hold the whole -/4546/-! ### 25:D4, 25:E1 — closed terms, their values, and the entries an evaluation consults -/4748/-- Closed terms over one constant and one binary operation: the full binary trees. -/49inductive Tm where50  | one : Tm51  | op : Tm → Tm → Tm5253/-- The value of a term in the structure with the constant read as `u` and the operation's table `f`. -/54def val (u : Nat) (f : Nat → Nat → Nat) : Tm → Nat55  | .one => u56  | .op s t => f (val u f s) (val u f t)5758/-- `g` agrees with `f` on every table entry the evaluation of the term in `(u, f)` consults. -/59def Agree (u : Nat) (f g : Nat → Nat → Nat) : Tm → Prop60  | .one => True61  | .op s t => Agree u f g s ∧ Agree u f g t ∧ g (val u f s) (val u f t) = f (val u f s) (val u f t)6263/-- The number of leaves of a term. -/64def leaves : Tm → Nat65  | .one => 166  | .op s t => leaves s + leaves t6768/-- The number of table lookups the evaluation of a term performs: one per operation. -/69def lookups : Tm → Nat70  | .one => 071  | .op s t => lookups s + lookups t + 17273/-- 25:D4 (Lemma wrap (2), the trace argument) — a structure that agrees with `M` on the entries the evaluation74consults gives the term the same value: the verification succeeds there step for step. -/75theorem trace_transport (u : Nat) (f g : Nat → Nat → Nat) : ∀ t : Tm, Agree u f g t → val u g t = val u f t76  | .one, _ => rfl77  | .op s t, ⟨hs, ht, e⟩ => by78    show g (val u g s) (val u g t) = f (val u f s) (val u f t)79    rw [trace_transport u f g s hs, trace_transport u f g t ht]; exact e8081/-- 25:D4 (Lemma wrap (2), the end sentence) — an equation verified by evaluation in `M` is true in every other82table that agrees with `M` on the cited entries: the certificate keeps its warrant in the small world. -/83theorem wrap_equation (u : Nat) (f g : Nat → Nat → Nat) (s t : Tm) (hs : Agree u f g s) (ht : Agree u f g t)84    (h : val u f s = val u f t) : val u g s = val u g t := by85  rw [trace_transport u f g s hs, trace_transport u f g t ht]; exact h8687/-- 25:D4 (Lemma wrap (2), the size of the trace) — the evaluation of a term with `ℓ` leaves performs `ℓ − 1`88lookups. -/89theorem lookups_succ : ∀ t : Tm, lookups t + 1 = leaves t90  | .one => rfl91  | .op s t => by92    show lookups s + lookups t + 1 + 1 = leaves s + leaves t93    rw [← lookups_succ s, ← lookups_succ t]94    exact (FRC.Nat.add_add_add_comm (lookups s) 1 (lookups t) 1).symm9596/-- 25:E1 (Lemma abundance, the value) — in `M_p` the closed term over `1` and `+` with `ℓ` leaves has the97value `ℓ mod p`, whatever its shape. -/98theorem value_leaves (p : Nat) (hp : 0 < p) :99    ∀ t : Tm, val (1 % p) (fun x y => (x + y) % p) t = leaves t % p100  | .one => rfl101  | .op s t => by102    show (val (1 % p) (fun x y => (x + y) % p) s + val (1 % p) (fun x y => (x + y) % p) t) % p = (leaves s + leaves t) % p103    rw [value_leaves p hp s, value_leaves p hp t]104    exact (FRC.Nat.add_mod (leaves s) (leaves t) p hp).symm105106/-- 25:E1 (Lemma abundance, the cohort) — any two terms with the same number of leaves give a true equation107of `M_p`. -/108theorem equal_leaves_equal_value (p : Nat) (hp : 0 < p) (s t : Tm) (h : leaves s = leaves t) :109    val (1 % p) (fun x y => (x + y) % p) s = val (1 % p) (fun x y => (x + y) % p) t := by110  rw [value_leaves p hp s, value_leaves p hp t, h]111112/-! ### 25:E2 — the reach bound -/113114/-- 25:E2 (Proposition reach, the count) — the records of length at most `B` over `a ≥ 2` letters number fewer115than `a^(B+1)`. -/116theorem records_lt (a : Nat) (ha : 2 ≤ a) (B : Nat) : FRC.Logic.records a B < a ^ (B + 1) :=117  FRC.Logic.records_lt a ha B118119/-- 25:E2 (Proposition reach, the vanishing fraction in finite form) — against a cohort of `2^L` truths the120records of length at most `B` certify a fraction below `1/N` once `L ≥ a^(B+1)·N`: their number times `N` is121below `2^L`. -/122theorem reach_vanishes (a : Nat) (ha : 2 ≤ a) (B N L : Nat) (h : a ^ (B + 1) * N ≤ L) :123    FRC.Logic.records a B * N < 2 ^ L :=124  Nat.lt_of_le_of_lt125    (Nat.le_trans (Nat.mul_le_mul_right N (Nat.le_of_lt (FRC.Logic.records_lt a ha B))) h)126    Nat.lt_two_pow_self127128/-! ### 25:F1, 25:F3 — mention cost: truth depends only on variables that occur -/129130/-- Terms with variables (de Bruijn indices) over the signature of `M_p`. -/131inductive VTm where132  | var : Nat → VTm133  | zero : VTm134  | one : VTm135  | add : VTm → VTm → VTm136  | mul : VTm → VTm → VTm137138/-- First-order formulas: equations, negation, conjunction, and the quantifier over the whole structure139(the bound variable is variable `0` of the body, the others shift up). -/140inductive Fm where141  | eq : VTm → VTm → Fm142  | neg : Fm → Fm143  | conj : Fm → Fm → Fm144  | all : Fm → Fm145146/-- The value of a term in `M_p` under an assignment. -/147def tval (p : Nat) (env : Nat → Nat) : VTm → Nat148  | .var i => env i149  | .zero => 0150  | .one => 1 % p151  | .add s t => (tval p env s + tval p env t) % p152  | .mul s t => (tval p env s * tval p env t) % p153154/-- Truth in `M_p` under an assignment: the quantifier ranges over the `p` elements. -/155def holds (p : Nat) (env : Nat → Nat) : Fm → Bool156  | .eq s t => decide (tval p env s = tval p env t)157  | .neg φ => !(holds p env φ)158  | .conj φ ψ => holds p env φ && holds p env ψ159  | .all φ => allBelow (fun x => holds p (cons x env) φ) p160161/-- Variable `i` occurs in the term. -/162def occT (i : Nat) : VTm → Bool163  | .var j => decide (j = i)164  | .zero => false165  | .one => false166  | .add s t => occT i s || occT i t167  | .mul s t => occT i s || occT i t168169/-- Variable `i` occurs free in the formula. -/170def occ (i : Nat) : Fm → Bool171  | .eq s t => occT i s || occT i t172  | .neg φ => occ i φ173  | .conj φ ψ => occ i φ || occ i ψ174  | .all φ => occ (i + 1) φ175176/-- The length of a term, in symbols. -/177def tsize : VTm → Nat178  | .var _ => 1179  | .zero => 1180  | .one => 1181  | .add s t => tsize s + tsize t + 1182  | .mul s t => tsize s + tsize t + 1183184/-- The length of a formula, in symbols. -/185def size : Fm → Nat186  | .eq s t => tsize s + tsize t + 1187  | .neg φ => size φ + 1188  | .conj φ ψ => size φ + size ψ + 1189  | .all φ => size φ + 1190191theorem tval_congr (p : Nat) {env env' : Nat → Nat} :192    ∀ t : VTm, (∀ i, occT i t = true → env i = env' i) → tval p env t = tval p env' t193  | .var j, h => h j (decide_eq_true rfl)194  | .zero, _ => rfl195  | .one, _ => rfl196  | .add s t, h => by197    show (tval p env s + tval p env t) % p = (tval p env' s + tval p env' t) % p198    rw [tval_congr p s (fun i hi => h i (or_intro_left hi)), tval_congr p t (fun i hi => h i (or_intro_right hi))]199  | .mul s t, h => by200    show (tval p env s * tval p env t) % p = (tval p env' s * tval p env' t) % p201    rw [tval_congr p s (fun i hi => h i (or_intro_left hi)), tval_congr p t (fun i hi => h i (or_intro_right hi))]202203/-- 25:F1 (Lemma mention, the coincidence form) — two assignments that agree on the variables occurring free in204a formula give it the same truth value in `M_p`. -/205theorem holds_congr (p : Nat) : ∀ (φ : Fm) {env env' : Nat → Nat},206    (∀ i, occ i φ = true → env i = env' i) → holds p env φ = holds p env' φ207  | .eq s t, env, env', h => by208    show decide (tval p env s = tval p env t) = decide (tval p env' s = tval p env' t)209    rw [tval_congr p s (fun i hi => h i (or_intro_left hi)), tval_congr p t (fun i hi => h i (or_intro_right hi))]210  | .neg φ, env, env', h => by211    show (!(holds p env φ)) = (!(holds p env' φ))212    rw [holds_congr p φ h]213  | .conj φ ψ, env, env', h => by214    show (holds p env φ && holds p env ψ) = (holds p env' φ && holds p env' ψ)215    rw [holds_congr p φ (fun i hi => h i (or_intro_left hi)), holds_congr p ψ (fun i hi => h i (or_intro_right hi))]216  | .all φ, env, env', h => by217    show allBelow (fun x => holds p (cons x env) φ) p = allBelow (fun x => holds p (cons x env') φ) p218    exact allBelow_congr (fun x _ => holds_congr p φ (fun i hi =>219      match i, hi with220      | 0, _ => rfl221      | j + 1, hj => h j hj))222223/-- The assignment changed at one coordinate. -/224def upd (env : Nat → Nat) (i v : Nat) : Nat → Nat := fun j => if j = i then v else env j225226/-- 25:F1 (Lemma mention) — if the truth of a formula in `M_p` depends on coordinate `i` (reassigning it changes227the truth value), then variable `i` occurs in the formula. -/228theorem mention (p : Nat) (φ : Fm) (env : Nat → Nat) (i v : Nat)229    (hdep : holds p (upd env i v) φ ≠ holds p env φ) : occ i φ = true :=230  match h : occ i φ with231  | true => rfl232  | false => absurd (holds_congr p φ (fun j hj =>233      match Nat.decEq j i with234      | isTrue e => Bool.noConfusion ((e ▸ hj : occ i φ = true).symm.trans h)235      | isFalse e => (ite_eq_right e : (if j = i then v else env j) = env j))) hdep236237/-! #### counting the coordinates a formula can read -/238239theorem tcount_le : ∀ (t : VTm) (N : Nat), count (fun i => occT i t) N ≤ tsize t240  | .var j, N => (count_single j N).1241  | .zero, N => by show count (fun _ => false) N ≤ 1; rw [count_false N]; exact Nat.zero_le 1242  | .one, N => by show count (fun _ => false) N ≤ 1; rw [count_false N]; exact Nat.zero_le 1243  | .add s t, N =>244    Nat.le_trans (count_or_le (fun i => occT i s) (fun i => occT i t) N)245      (Nat.le_succ_of_le (Nat.add_le_add (tcount_le s N) (tcount_le t N)))246  | .mul s t, N =>247    Nat.le_trans (count_or_le (fun i => occT i s) (fun i => occT i t) N)248      (Nat.le_succ_of_le (Nat.add_le_add (tcount_le s N) (tcount_le t N)))249250theorem fcount_le : ∀ (φ : Fm) (N : Nat), count (fun i => occ i φ) N ≤ size φ251  | .eq s t, N =>252    Nat.le_trans (count_or_le (fun i => occT i s) (fun i => occT i t) N)253      (Nat.le_succ_of_le (Nat.add_le_add (tcount_le s N) (tcount_le t N)))254  | .neg φ, N => Nat.le_succ_of_le (fcount_le φ N)255  | .conj φ ψ, N =>256    Nat.le_trans (count_or_le (fun i => occ i φ) (fun i => occ i ψ) N)257      (Nat.le_succ_of_le (Nat.add_le_add (fcount_le φ N) (fcount_le ψ N)))258  | .all φ, N =>259    Nat.le_succ_of_le (Nat.le_trans (count_shift (fun i => occ i φ) N) (fcount_le φ (N + 1)))260261/-- 25:F1 (Lemma mention, the arity) — a formula in which the `N` variables `0, …, N − 1` occur has length at262least `N`. -/263theorem arity_le_size (φ : Fm) (N : Nat) (h : ∀ i, i < N → occ i φ = true) : N ≤ size φ :=264  (count_full h) ▸ fcount_le φ N265266/-- 25:F1, 25:F2 (Lemma mention, the cost) — a formula whose truth in `M_p` depends on all `N` coordinates of a267tuple (the variables `0, …, N − 1`) has length at least `N`. -/268theorem mention_cost (p : Nat) (φ : Fm) (N : Nat)269    (h : ∀ i, i < N → ∃ env v, holds p (upd env i v) φ ≠ holds p env φ) : N ≤ size φ :=270  arity_le_size φ N (fun i hi => match h i hi with271    | ⟨env, v, hdep⟩ => mention p φ env i v hdep)272273theorem fcount_lt : ∀ (φ : Fm) (N : Nat), count (fun i => occ i φ) N < size φ274  | .eq s t, N =>275    Nat.lt_succ_of_le (Nat.le_trans (count_or_le (fun i => occT i s) (fun i => occT i t) N)276      (Nat.add_le_add (tcount_le s N) (tcount_le t N)))277  | .neg φ, N => Nat.lt_succ_of_lt (fcount_lt φ N)278  | .conj φ ψ, N =>279    Nat.lt_succ_of_le (Nat.le_trans (count_or_le (fun i => occ i φ) (fun i => occ i ψ) N)280      (Nat.add_le_add (Nat.le_of_lt (fcount_lt φ N)) (Nat.le_of_lt (fcount_lt ψ N))))281  | .all φ, N =>282    Nat.lt_succ_of_lt (Nat.lt_of_le_of_lt (count_shift (fun i => occ i φ) N) (fcount_lt φ (N + 1)))283284/-- 25:F3 (Corollary quotation, the arity) — a formula in which the `N` variables `j, …, j + N − 1` occur has more285than `N` symbols: a formula's arity is below its length. -/286theorem arity_lt_size (φ : Fm) (j N : Nat) (h : ∀ i, i < N → occ (i + j) φ = true) : N < size φ :=287  have h1 : count (fun i => occ (i + j) φ) N = N := count_full h288  Nat.lt_of_le_of_lt (Nat.le_trans (Nat.le_of_eq h1.symm) (count_shift_by j (fun i => occ i φ) N)) (fcount_lt φ (N + j))289290/-- 25:F3 (Corollary quotation, the cost) — a formula whose truth in `M_p` depends on all `N` coordinates of a291tuple, the variables `j, …, j + N − 1`, has more than `N` symbols. -/292theorem mention_cost_lt (p : Nat) (φ : Fm) (j N : Nat)293    (h : ∀ i, i < N → ∃ env v, holds p (upd env (i + j) v) φ ≠ holds p env φ) : N < size φ :=294  arity_lt_size φ j N (fun i hi => match h i hi with295    | ⟨env, v, hdep⟩ => mention p φ env (i + j) v hdep)296297/-- `Subformula ψ φ`: `ψ` is a subformula of `φ`. -/298inductive Subformula (ψ : Fm) : Fm → Prop where299  | refl : Subformula ψ ψ300  | neg {φ : Fm} : Subformula ψ φ → Subformula ψ (.neg φ)301  | conjL {φ χ : Fm} : Subformula ψ φ → Subformula ψ (.conj φ χ)302  | conjR {φ χ : Fm} : Subformula ψ χ → Subformula ψ (.conj φ χ)303  | all {φ : Fm} : Subformula ψ φ → Subformula ψ (.all φ)304305theorem sub_size {ψ : Fm} : ∀ {φ : Fm}, Subformula ψ φ → size ψ ≤ size φ306  | _, .refl => Nat.le_refl _307  | _, .neg h => Nat.le_succ_of_le (sub_size h)308  | .conj φ χ, .conjL h => Nat.le_succ_of_le (Nat.le_trans (sub_size h) (Nat.le_add_right (size φ) (size χ)))309  | .conj φ χ, .conjR h => Nat.le_succ_of_le (Nat.le_trans (sub_size h) (Nat.le_add_left (size χ) (size φ)))310  | _, .all h => Nat.le_succ_of_le (sub_size h)311312/-- 25:F3 (Corollary quotation) — no sentence `lam` contains a subformula whose truth depends on all coordinates313of a tuple of arity `N ≥ |lam|`, wherever the tuple's variables `j, …, j + N − 1` sit in the subformula's frame:314the subformula would have more than `N` symbols, and it is no longer than `lam`. -/315theorem no_self_reading (p : Nat) {ψ lam : Fm} (hsub : Subformula ψ lam) (j N : Nat) (hN : size lam ≤ N) :316    ¬ ∀ i, i < N → ∃ env v, holds p (upd env (i + j) v) ψ ≠ holds p env ψ := fun h =>317  Nat.lt_irrefl N (Nat.lt_of_lt_of_le (mention_cost_lt p ψ j N h) (Nat.le_trans (sub_size hsub) hN))318319/-! ### 25:F2 — the diagonal template does not fit at any scale -/320321/-- `∃ x, φ`, written with the language's one quantifier: `¬ ∀ x, ¬ φ`. -/322def ex (φ : Fm) : Fm := .neg (.all (.neg φ))323324/-- A block of `n` existential quantifiers in front of a formula. -/325def exBlock : Nat → Fm → Fm326  | 0, φ => φ327  | n + 1, φ => ex (exBlock n φ)328329/-- 25:F1 (Lemma mention, the quantifier block) — a block binding an `n`-tuple contributes `3n` symbols in this330syntax, at least `n`. -/331theorem size_exBlock : ∀ (n : Nat) (φ : Fm), size (exBlock n φ) = size φ + 3 * n332  | 0, _ => rfl333  | n + 1, φ => by334    show size (exBlock n φ) + 1 + 1 + 1 = size φ + 3 * (n + 1)335    rw [size_exBlock n φ, Nat.mul_succ]; rfl336337/-- 25:F2 (Theorem nocompress, the accounting) — the diagonal formula `δ = ∃ v (Diag_N ∧ θ)`, with a block of `N`338quantifiers and a diagonal relation whose truth depends on all `2N` coordinates, has length at least339`2N + |θ| + 3N`: `2N` for the relation (mention cost), then `θ`, and three symbols for each quantifier of the340block (the paper counts one, which gives its `3N + |θ|`). -/341theorem template_size (p N : Nat) (diag θ : Fm)342    (hdep : ∀ i, i < 2 * N → ∃ env v, holds p (upd env i v) diag ≠ holds p env diag) :343    2 * N + size θ + 3 * N ≤ size (exBlock N (.conj diag θ)) := by344  have h2 : 2 * N ≤ size diag := mention_cost p diag (2 * N) hdep345  rw [size_exBlock]346  show 2 * N + size θ + 3 * N ≤ size diag + size θ + 1 + 3 * N347  exact Nat.add_le_add_right (Nat.le_trans (Nat.add_le_add_right h2 (size θ)) (Nat.le_succ _)) (3 * N)348349/-- 25:F2 (Theorem nocompress, the scale) — a formula that binds an `N`-tuple, `N ≥ 1`, is longer than `N`: the350diagonal formula `∃ v (Diag_N ∧ θ)` has no code in `M^N`.  The block alone gives this clause; no hypothesis on351`Diag_N` or `θ` enters. -/352theorem no_template (N : Nat) (hN : 1 ≤ N) (φ : Fm) : ¬ size (exBlock N φ) ≤ N := fun hle => by353  rw [size_exBlock] at hle354  have h3 : 3 * N ≤ N := Nat.le_trans (Nat.le_add_left (3 * N) (size φ)) hle355  have h4 : N + 1 ≤ 3 * N := by356    have : N + N ≤ 3 * N := by rw [← Nat.two_mul]; exact Nat.mul_le_mul_right N (by decide)357    exact Nat.le_trans (Nat.add_le_add_left hN N) this358  exact Nat.not_succ_le_self N (Nat.le_trans h4 h3)359360/-- 25:F2 (Theorem nocompress, splitting the scales) — if `θ` reads all `N₂` coordinates of its argument (the361non-degeneracy clause, at the scale `N₂` of the code of the fixed point), the diagonal formula is longer than362`N₂`, whatever the scale `N` of its own block: here the mention cost is what excludes the instance. -/363theorem split_scale (p N N₂ : Nat) (diag θ : Fm)364    (hθ : ∀ i, i < N₂ → ∃ env v, holds p (upd env i v) θ ≠ holds p env θ) :365    N₂ < size (exBlock N (.conj diag θ)) := by366  have h : N₂ ≤ size θ := mention_cost p θ N₂ hθ367  rw [size_exBlock]368  show N₂ < size diag + size θ + 1 + 3 * N369  exact Nat.lt_of_le_of_lt h (Nat.lt_of_lt_of_le (Nat.lt_succ_of_le (Nat.le_add_left (size θ) (size diag))) (Nat.le_add_right _ (3 * N)))370371/-! ### 25:F4 — density does not rescue the template -/372373/-! ### 25:G4 — the prefix simulation -/374375/-- The coded prefix evaluated directly over a structure of `m` elements: `true` codes `∀`, `false` codes `∃`;376the matrix `ψ` reads the chosen values (the last chosen first). -/377def direct (m : Nat) (ψ : List Nat → Bool) : List Bool → List Nat → Bool378  | [], acc => ψ acc379  | true :: pat, acc => allBelow (fun x => direct m ψ pat (x :: acc)) m380  | false :: pat, acc => anyBelow (fun x => direct m ψ pat (x :: acc)) m381382/-- The uniform prefix `∀ y₁ ∃ x₁ … ∀ y_d ∃ x_d` with the clause `x_i = y_i` conjoined at the coded universal383positions and the matrix read on the `x`s; `c` carries the clauses collected so far. -/384def paired (m : Nat) (ψ : List Nat → Bool) : List Bool → List Nat → Bool → Bool385  | [], acc, c => c && ψ acc386  | q :: pat, acc, c =>387    allBelow (fun y => anyBelow (fun x => paired m ψ pat (x :: acc) (c && (!q || decide (x = y)))) m) m388389/-- 25:G4 (Lemma prefix) — the prefix simulation: over a structure of `m ≥ 1` elements the uniform pairing390prefix with the copy clauses decides exactly what the coded prefix `Q₁ … Q_d` decides, for every pattern and391every matrix. -/392theorem prefix_simulation (m : Nat) (hm : 0 < m) (ψ : List Nat → Bool) :393    ∀ (pat : List Bool) (acc : List Nat) (c : Bool), paired m ψ pat acc c = (c && direct m ψ pat acc)394  | [], _, _ => rfl395  | true :: pat, acc, c => by396    show allBelow (fun y => anyBelow (fun x => paired m ψ pat (x :: acc) (c && (!true || decide (x = y)))) m) m397        = (c && allBelow (fun x => direct m ψ pat (x :: acc)) m)398    rw [← allBelow_and_const c (fun x => direct m ψ pat (x :: acc)) m hm]399    refine allBelow_congr (fun y hy => ?_)400    have h1 : anyBelow (fun x => paired m ψ pat (x :: acc) (c && (!true || decide (x = y)))) m401        = anyBelow (fun x => (c && decide (x = y)) && direct m ψ pat (x :: acc)) m :=402      anyBelow_congr (fun x _ => prefix_simulation m hm ψ pat (x :: acc) (c && decide (x = y)))403    rw [h1, anyBelow_pick c (fun x => direct m ψ pat (x :: acc)) y m, ite_eq_left hy]404  | false :: pat, acc, c => by405    show allBelow (fun y => anyBelow (fun x => paired m ψ pat (x :: acc) (c && (!false || decide (x = y)))) m) m406        = (c && anyBelow (fun x => direct m ψ pat (x :: acc)) m)407    have h1 : ∀ y, anyBelow (fun x => paired m ψ pat (x :: acc) (c && (!false || decide (x = y)))) m408        = (c && anyBelow (fun x => direct m ψ pat (x :: acc)) m) := fun y => by409      rw [← anyBelow_and_const c (fun x => direct m ψ pat (x :: acc)) m]410      refine anyBelow_congr (fun x _ => ?_)411      have h2 : paired m ψ pat (x :: acc) (c && (!false || decide (x = y))) = ((c && true) && direct m ψ pat (x :: acc)) :=412        prefix_simulation m hm ψ pat (x :: acc) (c && true)413      rw [and_true' c] at h2414      exact h2415    rw [allBelow_congr (fun y _ => h1 y)]416    exact allBelow_const _ m hm417418/-- 25:G4 (Lemma prefix, the statement) — with no clause collected, the pairing prefix equals the coded prefix. -/419theorem prefix_simulation_closed (m : Nat) (hm : 0 < m) (ψ : List Nat → Bool) (pat : List Bool) :420    paired m ψ pat [] true = direct m ψ pat [] :=421  prefix_simulation m hm ψ pat [] true422423424425426/-! ## Old names (ledger migration, task LM17): the declarations moved to the themes, each under its old name -/427end428429section aliases430variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}431432open FRC.Logic (allBelow allBelow_congr cons)433434theorem or_intro_left {a b : Bool} (h : a = true) : (a || b) = true :=435  FRC.Logic.or_intro_left h436437theorem or_intro_right {a b : Bool} (h : b = true) : (a || b) = true :=438  FRC.Logic.or_intro_right h439440theorem and_true' (c : Bool) : (c && true) = c :=441  FRC.Logic.and_true' c442443theorem and_false' (c : Bool) : (c && false) = false :=444  FRC.Logic.and_false' c445446theorem and_self' (c : Bool) : (c && c) = c :=447  FRC.Logic.and_self' c448449theorem or_false' (c : Bool) : (c || false) = c :=450  FRC.Logic.or_false' c451452theorem and_assoc' (a b c : Bool) : ((a && b) && c) = (a && (b && c)) :=453  FRC.Logic.and_assoc' a b c454455/-- 25:C1 (Proposition noQ, the pigeonhole) — on `[0, n)` an injective map is onto: every `z < n` is a value. -/456theorem inj_onto (n : Nat) (S : Nat → Nat) (hS : ∀ x, x < n → S x < n)457    (hinj : ∀ x y, x < n → y < n → S x = S y → x = y) (z : Nat) (hz : z < n) : ∃ x, x < n ∧ S x = z :=458  FRC.Logic.inj_onto n S hS hinj z hz459460/-- 25:C1 (Proposition noQ) — no successor of `Q` on a finite carrier: no map of `[0, n)` into itself is461injective and omits an element, so no finite structure is a model of `Q`. -/462theorem no_finite_successor (n : Nat) (S : Nat → Nat) (hS : ∀ x, x < n → S x < n)463    (hinj : ∀ x y, x < n → y < n → S x = S y → x = y) (z : Nat) (hz : z < n) : ¬ ∀ x, x < n → S x ≠ z :=464  FRC.Logic.no_finite_successor n S hS hinj z hz465466/-- 25:D1 (Theorem part) — an agent with `R` storage states in a structure of `m > R` elements has no injective467encoding: every reading `ρ : [0, m) → [0, R)` identifies two elements. -/468theorem part_collides {m R : Nat} (hR : R < m) (ρ : Nat → Nat) (hρ : ∀ i, i < m → ρ i < R) :469    ¬ ∀ i j, i < m → j < m → ρ i = ρ j → i = j :=470  FRC.Logic.part_collides hR ρ hρ471472/-- 25:C5 (Remark Tarski scoped, the count) — `m + 1` sentences, indexed `0, …, m` (the row's sentences473`φ, ¬φ, …, ¬^m φ`), admit no injective numbering into a structure of `m` elements. -/474theorem sentences_outnumber (m : Nat) (g : Nat → Nat) (hg : ∀ i, i < m + 1 → g i < m) :475    ¬ ∀ i j, i < m + 1 → j < m + 1 → g i = g j → i = j :=476  FRC.Logic.sentences_outnumber m g hg477478/-- The number of `i < n` with `f i = true`. -/479@[reducible] def count (f : Nat → Bool) : Nat → Nat :=480  FRC.Logic.count f481482theorem count_full {f : Nat → Bool} : ∀ {n : Nat}, (∀ i, i < n → f i = true) → count f n = n :=483  FRC.Logic.count_full484485theorem cond_or_le (a b : Bool) : cond (a || b) 1 0 ≤ cond a 1 0 + cond b 1 0 :=486  FRC.Logic.cond_or_le a b487488theorem count_or_le (f g : Nat → Bool) : ∀ n, count (fun i => f i || g i) n ≤ count f n + count g n :=489  FRC.Logic.count_or_le f g490491theorem count_shift (f : Nat → Bool) : ∀ n, count (fun i => f (i + 1)) n ≤ count f (n + 1) :=492  FRC.Logic.count_shift f493494theorem count_false : ∀ n, count (fun _ => false) n = 0 :=495  FRC.Logic.count_false496497theorem count_single (j : Nat) : ∀ n, count (fun i => decide (j = i)) n ≤ 1 ∧ (n ≤ j → count (fun i => decide (j = i)) n = 0) :=498  FRC.Logic.count_single j499500theorem count_shift_by : ∀ (j : Nat) (f : Nat → Bool) (N : Nat), count (fun i => f (i + j)) N ≤ count f (N + j) :=501  FRC.Logic.count_shift_by502503/-- 25:F4 (Lemma density, the count) — an injective coding of the `a^n` strings of length `n` into `k`-tuples504over `m` elements needs `a^n ≤ m^k`. -/505theorem dense_coding {a n m k : Nat} (c : Nat → Nat) (hc : ∀ i, i < a ^ n → c i < m ^ k)506    (hinj : ∀ i j, i < a ^ n → j < a ^ n → c i = c j → i = j) : a ^ n ≤ m ^ k :=507  FRC.Logic.dense_coding c hc hinj508509/-- A strict power step: `m < b` gives `m^(k+1) < b^(k+1)`. -/510theorem pow_lt_pow_base {m b : Nat} (h : m < b) : ∀ k : Nat, m ^ (k + 1) < b ^ (k + 1) :=511  FRC.Logic.pow_lt_pow_base h512513/-- 25:F4 (Lemma density, the digit form) — if `m` has at most `d` digits in base `a` (`m < a^d`), a coding of514the strings of length `n` by tuples of `k+1` coordinates with `a^n ≤ m^(k+1)` has `n < d·(k+1)`: a tuple carries515fewer letters than `d` times its coordinates. -/516theorem digit_bound {a n m k d : Nat} (ha : 0 < a) (hm : m < a ^ d) (h : a ^ n ≤ m ^ (k + 1)) :517    n < d * (k + 1) :=518  FRC.Logic.digit_bound ha hm h519520/-- `f 0 || … || f (n − 1)`. -/521@[reducible] def anyBelow (f : Nat → Bool) : Nat → Bool :=522  FRC.Logic.anyBelow f523524theorem anyBelow_congr {f g : Nat → Bool} : ∀ {n : Nat}, (∀ x, x < n → f x = g x) → anyBelow f n = anyBelow g n :=525  FRC.Logic.anyBelow_congr526527theorem anyBelow_false : ∀ n, anyBelow (fun _ => false) n = false :=528  FRC.Logic.anyBelow_false529530theorem allBelow_const (b : Bool) : ∀ n, 0 < n → allBelow (fun _ => b) n = b :=531  FRC.Logic.allBelow_const b532533theorem anyBelow_and_const (c : Bool) (F : Nat → Bool) (n : Nat) :534    anyBelow (fun x => c && F x) n = (c && anyBelow F n) :=535  FRC.Logic.anyBelow_and_const c F n536537theorem allBelow_and_const (c : Bool) (F : Nat → Bool) (n : Nat) (hn : 0 < n) :538    allBelow (fun y => c && F y) n = (c && allBelow F n) :=539  FRC.Logic.allBelow_and_const c F n hn540541/-- Among the `x < n`, the clause `x = y` picks `y`: `∃ x < n, (c ∧ x = y ∧ F x)` is `c ∧ F y` for `y < n`. -/542theorem anyBelow_pick (c : Bool) (F : Nat → Bool) (y : Nat) :543    ∀ n, anyBelow (fun x => (c && decide (x = y)) && F x) n = (if y < n then c && F y else false) :=544  FRC.Logic.anyBelow_pick c F y545546end aliases547548-- Ledger predicates of 25-godel (generated by make_predicates.py from docs/25-godel/25-godel-ledger.json; edit the ledger, not this section)549/-- 25:C1 (p25010) — No finite structure interprets $\mathsf{Q}$: a model of $\mathsf{Q}$ has an injective successor with $0$ outside its range, and on a finite set an injective map is onto. -/550theorem p25010 : (∀ (n : Nat) (S : Nat → Nat), (∀ (x : Nat), x < n → S x < n) → (∀ (x y : Nat), x < n → y < n → S x = S y → x = y) → ∀ (z : Nat), z < n → ∃ x, x < n ∧ S x = z) ∧ ∀ (n : Nat) (S : Nat → Nat), (∀ (x : Nat), x < n → S x < n) → (∀ (x y : Nat), x < n → y < n → S x = S y → x = y) → ∀ (z : Nat), z < n → ¬∀ (x : Nat), x < n → S x ≠ z :=551  @FRC.Ledger.p25010552/-- 25:C5 (p25014) — Tarski scoped: the $m+1$ sentences $\varphi,\neg\varphi,\dots,\neg^{m}\varphi$ outnumber the $m$ elements of $\M$, so every numbering of the sentences by elements of $\M$ gives two of them the same number. Truth in $\M$ is defined externally by a finite table with the evaluation procedure of C2. What fails is the internalisation of truth. -/553theorem p25014 : ∀ (m : Nat) (g : Nat → Nat), (∀ (i : Nat), i < m + (1 : Nat) → g i < m) → ¬∀ (i j : Nat), i < m + (1 : Nat) → j < m + (1 : Nat) → g i = g j → i = j :=554  @FRC.Ledger.p25014555/-- 25:D1 (p25015) — Relational diagonal: an agent of storage capacity $K$ with $a^{K}<m$ has no injective encoding of the elements of $\M$ into its storage states. Every internal representation identifies distinct elements. A fortiori the agent holds no faithful model of $\M$ that also represents the model's own encoding map. -/556theorem p25015 : ∀ {m R : Nat}, R < m → ∀ (ρ : Nat → Nat), (∀ (i : Nat), i < m → ρ i < R) → ¬∀ (i j : Nat), i < m → j < m → ρ i = ρ j → i = j :=557  @FRC.Ledger.p25015558/-- 25:D4 (p25018) — Wrap, no internal trace: the steps that verify a certificate succeed in a finite $\M'$ built on its cited table entries, $\lvert \M'\rvert\le(r+1)\,p_{\D}(B)$, $r$ the largest arity. Under locally sound rules its end sentence is true there. An axiom asserted on syntactic recognition transports as a record, not as a truth. If $(r+1)\,p_{\D}(B)\le a^{K}$, no certificate marks a reading exact. -/559theorem p25018 : (∀ (u : Nat) (f g : Nat → Nat → Nat) (t : FRC.Godel.Tm), FRC.Godel.Agree u f g t → FRC.Godel.val u g t = FRC.Godel.val u f t) ∧ (∀ (u : Nat) (f g : Nat → Nat → Nat) (s t : FRC.Godel.Tm), FRC.Godel.Agree u f g s → FRC.Godel.Agree u f g t → FRC.Godel.val u f s = FRC.Godel.val u f t → FRC.Godel.val u g s = FRC.Godel.val u g t) ∧ ∀ (t : FRC.Godel.Tm), FRC.Godel.lookups t + (1 : Nat) = FRC.Godel.leaves t :=560  And.intro @FRC.Godel.trace_transport (And.intro @FRC.Godel.wrap_equation (@FRC.Godel.lookups_succ))561/-- 25:E1 (p25019) — Abundance: the closed terms over $\{1,+\}$ with $\ell$ leaves are the full binary trees, $C_{\ell-1}\ge2^{\ell-2}$ in number. In $\M_p$ all have the value $\ell\bmod p$, so any two give a true equation of length $O(\ell)$, at least $2^{\ell}$ of them for $\ell\ge6$. The true sentences of length at most $L$ number at least $2^{\alpha L}$ for large $L$, $\alpha>0$ constant. -/562theorem p25019 : (∀ (p : Nat), (0 : Nat) < p → ∀ (t : FRC.Godel.Tm), FRC.Godel.val ((1 : Nat) % p) (fun x y => (x + y) % p) t = FRC.Godel.leaves t % p) ∧ ∀ (p : Nat), (0 : Nat) < p → ∀ (s t : FRC.Godel.Tm), FRC.Godel.leaves s = FRC.Godel.leaves t → FRC.Godel.val ((1 : Nat) % p) (fun x y => (x + y) % p) s = FRC.Godel.val ((1 : Nat) % p) (fun x y => (x + y) % p) t :=563  And.intro @FRC.Godel.value_leaves (@FRC.Godel.equal_leaves_equal_value)564/-- 25:E2 (p25020) — Vanishing reach: an agent of capacity $(K,H)$ certifies at most $a^{B+1}$ sentences over all its runs, the records being strings of length at most $B$. The certified fraction of the truths of length at most $L$ (E1) is at most $a^{B+1}/2^{\alpha L}$, below $1/N$ for every $N$ once $L$ is large enough. -/565theorem p25020 : (∀ (a : Nat), (2 : Nat) ≤ a → ∀ (B : Nat), FRC.Logic.records a B < a ^ (B + (1 : Nat))) ∧ ∀ (a : Nat), (2 : Nat) ≤ a → ∀ (B N L : Nat), a ^ (B + (1 : Nat)) * N ≤ L → FRC.Logic.records a B * N < (2 : Nat) ^ L :=566  And.intro @FRC.Godel.records_lt (@FRC.Godel.reach_vanishes)567/-- 25:F1 (p25023) — Mention cost: if the truth of a formula in $\M$ depends on coordinate $i$ of a tuple of variables, then $v_{i}$ occurs in it. A formula whose truth depends on all $N$ coordinates has length at least $N$. A quantifier block binding an $N$-tuple contributes at least $N$ symbols. -/568theorem p25023 : (∀ (p : Nat) (φ : FRC.Godel.Fm) {env env' : Nat → Nat}, (∀ (i : Nat), FRC.Godel.occ i φ = true → env i = env' i) → FRC.Godel.holds p env φ = FRC.Godel.holds p env' φ) ∧ (∀ (p : Nat) (φ : FRC.Godel.Fm) (env : Nat → Nat) (i v : Nat), FRC.Godel.holds p (FRC.Godel.upd env i v) φ ≠ FRC.Godel.holds p env φ → FRC.Godel.occ i φ = true) ∧ (∀ (φ : FRC.Godel.Fm) (N : Nat), (∀ (i : Nat), i < N → FRC.Godel.occ i φ = true) → N ≤ FRC.Godel.size φ) ∧ (∀ (p : Nat) (φ : FRC.Godel.Fm) (N : Nat), (∀ (i : Nat), i < N → ∃ env v, FRC.Godel.holds p (FRC.Godel.upd env i v) φ ≠ FRC.Godel.holds p env φ) → N ≤ FRC.Godel.size φ) ∧ ∀ (n : Nat) (φ : FRC.Godel.Fm), FRC.Godel.size (FRC.Godel.exBlock n φ) = FRC.Godel.size φ + (3 : Nat) * n :=569  And.intro @FRC.Godel.holds_congr (And.intro @FRC.Godel.mention (And.intro @FRC.Godel.arity_le_size (And.intro @FRC.Godel.mention_cost (@FRC.Godel.size_exBlock))))570/-- 25:F2 (p25024) — No compression: code strings of length at most $N$ as tuples in $\M^{N}$, one coordinate per symbol, signature and alphabet fixed independently of $N$, $\theta$ non-degenerate. The G\"odel template has no instance at any scale. The diagonal formula needs $\lvert \delta\rvert\ge3N+\lvert \theta\rvert>N$ symbols, so its code is not in $\M^{N}$. Splitting the scales fails: $\delta$ outgrows the scale $\theta$ reads. -/571theorem p25024 : (∀ (p N : Nat) (diag θ : FRC.Godel.Fm), (∀ (i : Nat), i < (2 : Nat) * N → ∃ env v, FRC.Godel.holds p (FRC.Godel.upd env i v) diag ≠ FRC.Godel.holds p env diag) → (2 : Nat) * N + FRC.Godel.size θ + (3 : Nat) * N ≤ FRC.Godel.size (FRC.Godel.exBlock N (diag.conj θ))) ∧ (∀ (N : Nat), (1 : Nat) ≤ N → ∀ (φ : FRC.Godel.Fm), ¬FRC.Godel.size (FRC.Godel.exBlock N φ) ≤ N) ∧ (∀ (p N N₂ : Nat) (diag θ : FRC.Godel.Fm), (∀ (i : Nat), i < N₂ → ∃ env v, FRC.Godel.holds p (FRC.Godel.upd env i v) θ ≠ FRC.Godel.holds p env θ) → N₂ < FRC.Godel.size (FRC.Godel.exBlock N (diag.conj θ))) ∧ ∀ (p : Nat) (φ : FRC.Godel.Fm) (N : Nat), (∀ (i : Nat), i < N → ∃ env v, FRC.Godel.holds p (FRC.Godel.upd env i v) φ ≠ FRC.Godel.holds p env φ) → N ≤ FRC.Godel.size φ :=572  And.intro @FRC.Godel.template_size (And.intro @FRC.Godel.no_template (And.intro @FRC.Godel.split_scale (@FRC.Godel.mention_cost)))573/-- 25:F3 (p25025) — Quotation exceeds mention: a formula's arity is below its length. No sentence $\lambda$ contains a subformula whose truth depends on all coordinates of a tuple of arity at least $\lvert \lambda\rvert$. Under any coding that spends at least $\lvert \lambda\rvert$ coordinates on $\lambda$, per-symbol coding included, no sentence's truth is sensitive to every coordinate of its own code. -/574theorem p25025 : (∀ (φ : FRC.Godel.Fm) (j N : Nat), (∀ (i : Nat), i < N → FRC.Godel.occ (i + j) φ = true) → N < FRC.Godel.size φ) ∧ (∀ (p : Nat) (φ : FRC.Godel.Fm) (j N : Nat), (∀ (i : Nat), i < N → ∃ env v, FRC.Godel.holds p (FRC.Godel.upd env (i + j) v) φ ≠ FRC.Godel.holds p env φ) → N < FRC.Godel.size φ) ∧ ∀ (p : Nat) {ψ lam : FRC.Godel.Fm}, FRC.Godel.Subformula ψ lam → ∀ (j N : Nat), FRC.Godel.size lam ≤ N → ¬∀ (i : Nat), i < N → ∃ env v, FRC.Godel.holds p (FRC.Godel.upd env (i + j) v) ψ ≠ FRC.Godel.holds p env ψ :=575  And.intro @FRC.Godel.arity_lt_size (And.intro @FRC.Godel.mention_cost_lt (@FRC.Godel.no_self_reading))576/-- 25:F4 (p25048) — Density: $m$ has $d$ base-$a$ digits. An injective coding of length-$n$ strings by $k$-tuples, $k\ge1$, needs $m^{k}\ge a^{n}$, so $n<dk$. In F2's $\delta(u)=\exists v\,(\mathrm{Diag}(u,v)\wedge\theta(v))$ let $v$ have $k$ coordinates and $u$ have $k_{1}$. Each coordinate of $v$ is named three times, each of $u$ once. So $\lvert\delta\rvert\ge2c(k)+c(k+k_{1})$, and $\lambda=\delta(\ulcorner\delta\urcorner)$ has $\lvert\lambda\rvert\ge3c(k)+k_{1}$, $c(j)$ the total length of the $j$ shortest names. -/577theorem p25048 : (∀ {a n m k : Nat} (c : Nat → Nat), (∀ (i : Nat), i < a ^ n → c i < m ^ k) → (∀ (i j : Nat), i < a ^ n → j < a ^ n → c i = c j → i = j) → a ^ n ≤ m ^ k) ∧ ∀ {a n m k d : Nat}, (0 : Nat) < a → m < a ^ d → a ^ n ≤ m ^ (k + (1 : Nat)) → n < d * (k + (1 : Nat)) :=578  @FRC.Ledger.p25048579/-- 25:G4 (p25031) — Prefix simulation: $Q_{1}z_{1}\cdots Q_{d}z_{d}\,\psi(\bar z)$ holds in $\M$ exactly when $\forall y_{1}\exists x_{1}\cdots\forall y_{d}\exists x_{d}\,[\bigwedge_{i:Q_{i}=\forall}x_{i}=y_{i}\wedge\psi(\bar x)]$ does: one uniform prefix simulates every coded quantifier pattern. -/580theorem p25031 : (∀ (m : Nat), (0 : Nat) < m → ∀ (ψ : List Nat → Bool) (pat : List Bool) (acc : List Nat) (c : Bool), FRC.Godel.paired m ψ pat acc c = (c && FRC.Godel.direct m ψ pat acc)) ∧ ∀ (m : Nat), (0 : Nat) < m → ∀ (ψ : List Nat → Bool) (pat : List Bool), FRC.Godel.paired m ψ pat [] true = FRC.Godel.direct m ψ pat [] :=581  And.intro @FRC.Godel.prefix_simulation (@FRC.Godel.prefix_simulation_closed)582-- end ledger predicates583584end FRC.Godel585