Theme/Diagonal.lean — FrcCore

1import FrcCore.Theme.Reach23/-!4# FrcCore.Theme.Diagonal — the diagonal under finitude (the logic theme; 25-godel's migration, 20 October 2026)56The syntax of `M_p` (`0`, `1`, `+`, `×`, equations, negation, conjunction, the quantifier over the structure) and what7the diagonal construction costs in it, with no axioms:89* mention cost: a formula's truth depends only on the variables that occur in it, so a formula reading all `N`10  coordinates of a tuple has at least `N` symbols, and more than `N` (25:F1, 25:F3);11* the template: the diagonal formula `∃ v (Diag ∧ θ)` is longer than the scale of its bound tuple and than the scale its12  matrix reads, so it has no instance per symbol at any scale and the scales cannot be split (25:F2); no sentence has a13  subformula that reads a tuple as long as the sentence (25:F3, 25:G6);14* the threshold: the `k` shortest names over `a` letters cost `c(k)` symbols with `kJ + 2 ≤ c(k) + 2a^J` for every `J`;15  a dense instance with `k` coordinates in `v` and `k₁` in `u` needs `2c(k) + c(k + k₁) < d k₁` and `3c(k) + k₁ < d k`,16  which force `k < 6a^{⌊d/3⌋+1}` (so `k` has at most `⌊d/3⌋ + 4` base-`a` digits), `k < 6a^{⌊d/4⌋+1}` at one scale,17  nothing at `d ≤ 4`, and the threshold `t = d·k*` below `a^{d−1} ≤ m` in every structure (25:F6);18* the decoders: `Int_J(x)` of linear length defines `{0, …, 2^J − 1}` in `M_p` when `2^J ≤ p` (25:F7);19* the prefix simulation: one uniform pairing prefix decides what every coded quantifier pattern decides (25:G4);20* the window's digits: an element coding `1,024` base-32 symbols needs more base-32 digits than the chart's bound of21  `Ω` has, which is `82` (00:Z9).2223The paper module `FrcCore/Godel.lean` keeps every old name as an alias.24-/2526namespace FRC.Diagonal2728open FRC.Logic FRC.Reach2930/-! ### 25:F1, 25:F3 — mention cost: truth depends only on variables that occur -/3132/-- Terms with variables (de Bruijn indices) over the signature of `M_p`. -/33inductive VTm where34  | var : Nat → VTm35  | zero : VTm36  | one : VTm37  | add : VTm → VTm → VTm38  | mul : VTm → VTm → VTm3940/-- First-order formulas: equations, negation, conjunction, and the quantifier over the whole structure41(the bound variable is variable `0` of the body, the others shift up). -/42inductive Fm where43  | eq : VTm → VTm → Fm44  | neg : Fm → Fm45  | conj : Fm → Fm → Fm46  | all : Fm → Fm4748/-- The value of a term in `M_p` under an assignment. -/49def tval (p : Nat) (env : Nat → Nat) : VTm → Nat50  | .var i => env i51  | .zero => 052  | .one => 1 % p53  | .add s t => (tval p env s + tval p env t) % p54  | .mul s t => (tval p env s * tval p env t) % p5556/-- Truth in `M_p` under an assignment: the quantifier ranges over the `p` elements. -/57def holds (p : Nat) (env : Nat → Nat) : Fm → Bool58  | .eq s t => decide (tval p env s = tval p env t)59  | .neg φ => !(holds p env φ)60  | .conj φ ψ => holds p env φ && holds p env ψ61  | .all φ => allBelow (fun x => holds p (cons x env) φ) p6263/-- Variable `i` occurs in the term. -/64def occT (i : Nat) : VTm → Bool65  | .var j => decide (j = i)66  | .zero => false67  | .one => false68  | .add s t => occT i s || occT i t69  | .mul s t => occT i s || occT i t7071/-- Variable `i` occurs free in the formula. -/72def occ (i : Nat) : Fm → Bool73  | .eq s t => occT i s || occT i t74  | .neg φ => occ i φ75  | .conj φ ψ => occ i φ || occ i ψ76  | .all φ => occ (i + 1) φ7778/-- The length of a term, in symbols. -/79def tsize : VTm → Nat80  | .var _ => 181  | .zero => 182  | .one => 183  | .add s t => tsize s + tsize t + 184  | .mul s t => tsize s + tsize t + 18586/-- The length of a formula, in symbols. -/87def size : Fm → Nat88  | .eq s t => tsize s + tsize t + 189  | .neg φ => size φ + 190  | .conj φ ψ => size φ + size ψ + 191  | .all φ => size φ + 19293theorem tval_congr (p : Nat) {env env' : Nat → Nat} :94    ∀ t : VTm, (∀ i, occT i t = true → env i = env' i) → tval p env t = tval p env' t95  | .var j, h => h j (decide_eq_true rfl)96  | .zero, _ => rfl97  | .one, _ => rfl98  | .add s t, h => by99    show (tval p env s + tval p env t) % p = (tval p env' s + tval p env' t) % p100    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))]101  | .mul s t, h => by102    show (tval p env s * tval p env t) % p = (tval p env' s * tval p env' t) % p103    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))]104105/-- 25:F1 (Lemma mention, the coincidence form) — two assignments that agree on the variables occurring free in106a formula give it the same truth value in `M_p`. -/107theorem holds_congr (p : Nat) : ∀ (φ : Fm) {env env' : Nat → Nat},108    (∀ i, occ i φ = true → env i = env' i) → holds p env φ = holds p env' φ109  | .eq s t, env, env', h => by110    show decide (tval p env s = tval p env t) = decide (tval p env' s = tval p env' t)111    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))]112  | .neg φ, env, env', h => by113    show (!(holds p env φ)) = (!(holds p env' φ))114    rw [holds_congr p φ h]115  | .conj φ ψ, env, env', h => by116    show (holds p env φ && holds p env ψ) = (holds p env' φ && holds p env' ψ)117    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))]118  | .all φ, env, env', h => by119    show allBelow (fun x => holds p (cons x env) φ) p = allBelow (fun x => holds p (cons x env') φ) p120    exact allBelow_congr (fun x _ => holds_congr p φ (fun i hi =>121      match i, hi with122      | 0, _ => rfl123      | j + 1, hj => h j hj))124125/-- The assignment changed at one coordinate. -/126def upd (env : Nat → Nat) (i v : Nat) : Nat → Nat := fun j => if j = i then v else env j127128/-- 25:F1 (Lemma mention) — if the truth of a formula in `M_p` depends on coordinate `i` (reassigning it changes129the truth value), then variable `i` occurs in the formula. -/130theorem mention (p : Nat) (φ : Fm) (env : Nat → Nat) (i v : Nat)131    (hdep : holds p (upd env i v) φ ≠ holds p env φ) : occ i φ = true :=132  match h : occ i φ with133  | true => rfl134  | false => absurd (holds_congr p φ (fun j hj =>135      match Nat.decEq j i with136      | isTrue e => Bool.noConfusion ((e ▸ hj : occ i φ = true).symm.trans h)137      | isFalse e => (ite_eq_right e : (if j = i then v else env j) = env j))) hdep138139/-! #### counting the coordinates a formula can read -/140141theorem tcount_le : ∀ (t : VTm) (N : Nat), count (fun i => occT i t) N ≤ tsize t142  | .var j, N => (count_single j N).1143  | .zero, N => by show count (fun _ => false) N ≤ 1; rw [count_false N]; exact Nat.zero_le 1144  | .one, N => by show count (fun _ => false) N ≤ 1; rw [count_false N]; exact Nat.zero_le 1145  | .add s t, N =>146    Nat.le_trans (count_or_le (fun i => occT i s) (fun i => occT i t) N)147      (Nat.le_succ_of_le (Nat.add_le_add (tcount_le s N) (tcount_le t N)))148  | .mul s t, N =>149    Nat.le_trans (count_or_le (fun i => occT i s) (fun i => occT i t) N)150      (Nat.le_succ_of_le (Nat.add_le_add (tcount_le s N) (tcount_le t N)))151152theorem fcount_le : ∀ (φ : Fm) (N : Nat), count (fun i => occ i φ) N ≤ size φ153  | .eq s t, N =>154    Nat.le_trans (count_or_le (fun i => occT i s) (fun i => occT i t) N)155      (Nat.le_succ_of_le (Nat.add_le_add (tcount_le s N) (tcount_le t N)))156  | .neg φ, N => Nat.le_succ_of_le (fcount_le φ N)157  | .conj φ ψ, N =>158    Nat.le_trans (count_or_le (fun i => occ i φ) (fun i => occ i ψ) N)159      (Nat.le_succ_of_le (Nat.add_le_add (fcount_le φ N) (fcount_le ψ N)))160  | .all φ, N =>161    Nat.le_succ_of_le (Nat.le_trans (count_shift (fun i => occ i φ) N) (fcount_le φ (N + 1)))162163/-- 25:F1 (Lemma mention, the arity) — a formula in which the `N` variables `0, …, N − 1` occur has length at164least `N`. -/165theorem arity_le_size (φ : Fm) (N : Nat) (h : ∀ i, i < N → occ i φ = true) : N ≤ size φ :=166  (count_full h) ▸ fcount_le φ N167168/-- 25:F1, 25:F2, 00:Z9 (Lemma mention, the cost) — a formula whose truth in `M_p` depends on all `N` coordinates of a169tuple (the variables `0, …, N − 1`) has length at least `N`. -/170theorem mention_cost (p : Nat) (φ : Fm) (N : Nat)171    (h : ∀ i, i < N → ∃ env v, holds p (upd env i v) φ ≠ holds p env φ) : N ≤ size φ :=172  arity_le_size φ N (fun i hi => match h i hi with173    | ⟨env, v, hdep⟩ => mention p φ env i v hdep)174175theorem fcount_lt : ∀ (φ : Fm) (N : Nat), count (fun i => occ i φ) N < size φ176  | .eq s t, N =>177    Nat.lt_succ_of_le (Nat.le_trans (count_or_le (fun i => occT i s) (fun i => occT i t) N)178      (Nat.add_le_add (tcount_le s N) (tcount_le t N)))179  | .neg φ, N => Nat.lt_succ_of_lt (fcount_lt φ N)180  | .conj φ ψ, N =>181    Nat.lt_succ_of_le (Nat.le_trans (count_or_le (fun i => occ i φ) (fun i => occ i ψ) N)182      (Nat.add_le_add (Nat.le_of_lt (fcount_lt φ N)) (Nat.le_of_lt (fcount_lt ψ N))))183  | .all φ, N =>184    Nat.lt_succ_of_lt (Nat.lt_of_le_of_lt (count_shift (fun i => occ i φ) N) (fcount_lt φ (N + 1)))185186/-- 25:F3, 25:G6 (Corollary quotation, the arity) — a formula in which the `N` variables `j, …, j + N − 1` occur has more187than `N` symbols: a formula's arity is below its length. -/188theorem arity_lt_size (φ : Fm) (j N : Nat) (h : ∀ i, i < N → occ (i + j) φ = true) : N < size φ :=189  have h1 : count (fun i => occ (i + j) φ) N = N := count_full h190  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))191192/-- 25:F3, 25:G6 (Corollary quotation, the cost) — a formula whose truth in `M_p` depends on all `N` coordinates of a193tuple, the variables `j, …, j + N − 1`, has more than `N` symbols. -/194theorem mention_cost_lt (p : Nat) (φ : Fm) (j N : Nat)195    (h : ∀ i, i < N → ∃ env v, holds p (upd env (i + j) v) φ ≠ holds p env φ) : N < size φ :=196  arity_lt_size φ j N (fun i hi => match h i hi with197    | ⟨env, v, hdep⟩ => mention p φ env (i + j) v hdep)198199/-- `Subformula ψ φ`: `ψ` is a subformula of `φ`. -/200inductive Subformula (ψ : Fm) : Fm → Prop where201  | refl : Subformula ψ ψ202  | neg {φ : Fm} : Subformula ψ φ → Subformula ψ (.neg φ)203  | conjL {φ χ : Fm} : Subformula ψ φ → Subformula ψ (.conj φ χ)204  | conjR {φ χ : Fm} : Subformula ψ χ → Subformula ψ (.conj φ χ)205  | all {φ : Fm} : Subformula ψ φ → Subformula ψ (.all φ)206207theorem sub_size {ψ : Fm} : ∀ {φ : Fm}, Subformula ψ φ → size ψ ≤ size φ208  | _, .refl => Nat.le_refl _209  | _, .neg h => Nat.le_succ_of_le (sub_size h)210  | .conj φ χ, .conjL h => Nat.le_succ_of_le (Nat.le_trans (sub_size h) (Nat.le_add_right (size φ) (size χ)))211  | .conj φ χ, .conjR h => Nat.le_succ_of_le (Nat.le_trans (sub_size h) (Nat.le_add_left (size χ) (size φ)))212  | _, .all h => Nat.le_succ_of_le (sub_size h)213214/-- 25:F3, 25:G6, 25:G7, 00:Z9 (Corollary quotation) — no sentence `lam` contains a subformula whose truth depends on all coordinates215of a tuple of arity `N ≥ |lam|`, wherever the tuple's variables `j, …, j + N − 1` sit in the subformula's frame:216the subformula would have more than `N` symbols, and it is no longer than `lam`. -/217theorem no_self_reading (p : Nat) {ψ lam : Fm} (hsub : Subformula ψ lam) (j N : Nat) (hN : size lam ≤ N) :218    ¬ ∀ i, i < N → ∃ env v, holds p (upd env (i + j) v) ψ ≠ holds p env ψ := fun h =>219  Nat.lt_irrefl N (Nat.lt_of_lt_of_le (mention_cost_lt p ψ j N h) (Nat.le_trans (sub_size hsub) hN))220221/-! ### 25:F2 — the diagonal template does not fit at any scale -/222223/-- `∃ x, φ`, written with the language's one quantifier: `¬ ∀ x, ¬ φ`. -/224def ex (φ : Fm) : Fm := .neg (.all (.neg φ))225226/-- A block of `n` existential quantifiers in front of a formula. -/227def exBlock : Nat → Fm → Fm228  | 0, φ => φ229  | n + 1, φ => ex (exBlock n φ)230231/-- 25:F1 (Lemma mention, the quantifier block) — a block binding an `n`-tuple contributes `3n` symbols in this232syntax, at least `n`. -/233theorem size_exBlock : ∀ (n : Nat) (φ : Fm), size (exBlock n φ) = size φ + 3 * n234  | 0, _ => rfl235  | n + 1, φ => by236    show size (exBlock n φ) + 1 + 1 + 1 = size φ + 3 * (n + 1)237    rw [size_exBlock n φ, Nat.mul_succ]; rfl238239/-- 25:F2, 25:G7, 00:Z9 (Theorem nocompress, the accounting) — the diagonal formula `δ = ∃ v (Diag_N ∧ θ)`, with a block of `N`240quantifiers and a diagonal relation whose truth depends on all `2N` coordinates, has length at least241`2N + |θ| + 3N`: `2N` for the relation (mention cost), then `θ`, and three symbols for each quantifier of the242block (the paper counts one, which gives its `3N + |θ|`). -/243theorem template_size (p N : Nat) (diag θ : Fm)244    (hdep : ∀ i, i < 2 * N → ∃ env v, holds p (upd env i v) diag ≠ holds p env diag) :245    2 * N + size θ + 3 * N ≤ size (exBlock N (.conj diag θ)) := by246  have h2 : 2 * N ≤ size diag := mention_cost p diag (2 * N) hdep247  rw [size_exBlock]248  show 2 * N + size θ + 3 * N ≤ size diag + size θ + 1 + 3 * N249  exact Nat.add_le_add_right (Nat.le_trans (Nat.add_le_add_right h2 (size θ)) (Nat.le_succ _)) (3 * N)250251/-- 25:F2, 00:Z9 (Theorem nocompress, the scale) — a formula that binds an `N`-tuple, `N ≥ 1`, is longer than `N`: the252diagonal formula `∃ v (Diag_N ∧ θ)` has no code in `M^N`.  The block alone gives this clause; no hypothesis on253`Diag_N` or `θ` enters. -/254theorem no_template (N : Nat) (hN : 1 ≤ N) (φ : Fm) : ¬ size (exBlock N φ) ≤ N := fun hle => by255  rw [size_exBlock] at hle256  have h3 : 3 * N ≤ N := Nat.le_trans (Nat.le_add_left (3 * N) (size φ)) hle257  have h4 : N + 1 ≤ 3 * N := by258    have : N + N ≤ 3 * N := by rw [← Nat.two_mul]; exact Nat.mul_le_mul_right N (by decide)259    exact Nat.le_trans (Nat.add_le_add_left hN N) this260  exact Nat.not_succ_le_self N (Nat.le_trans h4 h3)261262/-- 25:F2, 00:Z9 (Theorem nocompress, splitting the scales) — if `θ` reads all `N₂` coordinates of its argument (the263non-degeneracy clause, at the scale `N₂` of the code of the fixed point), the diagonal formula is longer than264`N₂`, whatever the scale `N` of its own block: here the mention cost is what excludes the instance. -/265theorem split_scale (p N N₂ : Nat) (diag θ : Fm)266    (hθ : ∀ i, i < N₂ → ∃ env v, holds p (upd env i v) θ ≠ holds p env θ) :267    N₂ < size (exBlock N (.conj diag θ)) := by268  have h : N₂ ≤ size θ := mention_cost p θ N₂ hθ269  rw [size_exBlock]270  show N₂ < size diag + size θ + 1 + 3 * N271  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)))272273/-! ### 25:F4 — density does not rescue the template -/274275/-! ### 25:G4 — the prefix simulation -/276277/-- The coded prefix evaluated directly over a structure of `m` elements: `true` codes `∀`, `false` codes `∃`;278the matrix `ψ` reads the chosen values (the last chosen first). -/279def direct (m : Nat) (ψ : List Nat → Bool) : List Bool → List Nat → Bool280  | [], acc => ψ acc281  | true :: pat, acc => allBelow (fun x => direct m ψ pat (x :: acc)) m282  | false :: pat, acc => anyBelow (fun x => direct m ψ pat (x :: acc)) m283284/-- The uniform prefix `∀ y₁ ∃ x₁ … ∀ y_d ∃ x_d` with the clause `x_i = y_i` conjoined at the coded universal285positions and the matrix read on the `x`s; `c` carries the clauses collected so far. -/286def paired (m : Nat) (ψ : List Nat → Bool) : List Bool → List Nat → Bool → Bool287  | [], acc, c => c && ψ acc288  | q :: pat, acc, c =>289    allBelow (fun y => anyBelow (fun x => paired m ψ pat (x :: acc) (c && (!q || decide (x = y)))) m) m290291/-- 25:G4 (Lemma prefix) — the prefix simulation: over a structure of `m ≥ 1` elements the uniform pairing292prefix with the copy clauses decides exactly what the coded prefix `Q₁ … Q_d` decides, for every pattern and293every matrix. -/294theorem prefix_simulation (m : Nat) (hm : 0 < m) (ψ : List Nat → Bool) :295    ∀ (pat : List Bool) (acc : List Nat) (c : Bool), paired m ψ pat acc c = (c && direct m ψ pat acc)296  | [], _, _ => rfl297  | true :: pat, acc, c => by298    show allBelow (fun y => anyBelow (fun x => paired m ψ pat (x :: acc) (c && (!true || decide (x = y)))) m) m299        = (c && allBelow (fun x => direct m ψ pat (x :: acc)) m)300    rw [← allBelow_and_const c (fun x => direct m ψ pat (x :: acc)) m hm]301    refine allBelow_congr (fun y hy => ?_)302    have h1 : anyBelow (fun x => paired m ψ pat (x :: acc) (c && (!true || decide (x = y)))) m303        = anyBelow (fun x => (c && decide (x = y)) && direct m ψ pat (x :: acc)) m :=304      anyBelow_congr (fun x _ => prefix_simulation m hm ψ pat (x :: acc) (c && decide (x = y)))305    rw [h1, anyBelow_pick c (fun x => direct m ψ pat (x :: acc)) y m, ite_eq_left hy]306  | false :: pat, acc, c => by307    show allBelow (fun y => anyBelow (fun x => paired m ψ pat (x :: acc) (c && (!false || decide (x = y)))) m) m308        = (c && anyBelow (fun x => direct m ψ pat (x :: acc)) m)309    have h1 : ∀ y, anyBelow (fun x => paired m ψ pat (x :: acc) (c && (!false || decide (x = y)))) m310        = (c && anyBelow (fun x => direct m ψ pat (x :: acc)) m) := fun y => by311      rw [← anyBelow_and_const c (fun x => direct m ψ pat (x :: acc)) m]312      refine anyBelow_congr (fun x _ => ?_)313      have h2 : paired m ψ pat (x :: acc) (c && (!false || decide (x = y))) = ((c && true) && direct m ψ pat (x :: acc)) :=314        prefix_simulation m hm ψ pat (x :: acc) (c && true)315      rw [and_true' c] at h2316      exact h2317    rw [allBelow_congr (fun y _ => h1 y)]318    exact allBelow_const _ m hm319320/-- 25:G4 (Lemma prefix, the statement) — with no clause collected, the pairing prefix equals the coded prefix. -/321theorem prefix_simulation_closed (m : Nat) (hm : 0 < m) (ψ : List Nat → Bool) (pat : List Bool) :322    paired m ψ pat [] true = direct m ψ pat [] :=323  prefix_simulation m hm ψ pat [] true324325/-! ### 25:F7 — the decoders: `Int_J(x)` defines `{0, …, 2^J − 1}` -/326327/-- `φ ∨ ψ`, with the language's connectives: `¬(¬φ ∧ ¬ψ)`. -/328def orF (φ ψ : Fm) : Fm := .neg (.conj (.neg φ) (.neg ψ))329330theorem holds_conj_iff (p : Nat) (env : Nat → Nat) (φ ψ : Fm) :331    holds p env (.conj φ ψ) = true ↔ holds p env φ = true ∧ holds p env ψ = true :=332  ⟨fun h => ⟨band_l h, band_r h⟩, fun ⟨h1, h2⟩ => by show (holds p env φ && holds p env ψ) = true; rw [h1, h2]; rfl⟩333334theorem holds_orF_iff (p : Nat) (env : Nat → Nat) (φ ψ : Fm) :335    holds p env (orF φ ψ) = true ↔ holds p env φ = true ∨ holds p env ψ = true := by336  show (!(!(holds p env φ) && !(holds p env ψ))) = true ↔ _337  match holds p env φ, holds p env ψ with338  | true, _ => exact ⟨fun _ => .inl rfl, fun _ => rfl⟩339  | false, true => exact ⟨fun _ => .inr rfl, fun _ => rfl⟩340  | false, false => exact ⟨fun h => Bool.noConfusion h, fun h => match h with | .inl e => Bool.noConfusion e | .inr e => Bool.noConfusion e⟩341342theorem not_allBelow_not (f : Nat → Bool) : ∀ n, (!(allBelow (fun y => !(f y)) n)) = anyBelow f n343  | 0 => rfl344  | n + 1 => by345    show (!((!(f n)) && allBelow (fun y => !(f y)) n)) = (f n || anyBelow f n)346    rw [← not_allBelow_not f n]347    cases f n <;> cases allBelow (fun y => !(f y)) n <;> rfl348349theorem holds_ex_iff (p : Nat) (env : Nat → Nat) (φ : Fm) :350    holds p env (ex φ) = true ↔ ∃ y, y < p ∧ holds p (cons y env) φ = true := by351  show (!(allBelow (fun y => !(holds p (cons y env) φ)) p)) = true ↔ _352  rw [not_allBelow_not]353  exact anyBelow_true_iff _ p354355theorem holds_eq_iff (p : Nat) (env : Nat → Nat) (s t : VTm) :356    holds p env (.eq s t) = true ↔ tval p env s = tval p env t :=357  ⟨of_decide_eq_true, decide_eq_true⟩358359/-- `seg_J(x, w)`: `x ∈ {0, w, 2w, …, (2^J − 1) w}` in `M_p`, written with two reused bound variables per level:360`seg_0(x, w) := x = 0`; `seg_{J+1}(x, w) := ∃ y ((x = y ∨ x = y + w) ∧ ∃ w' (w' = w + w ∧ seg_J(y, w')))`. The arguments361are variable indices; under each quantifier the outer variables shift up by one. -/362def seg : Nat → Nat → Nat → Fm363  | 0, x, _ => .eq (.var x) .zero364  | J + 1, x, w =>365    ex (.conj (orF (.eq (.var (x + 1)) (.var 0)) (.eq (.var (x + 1)) (.add (.var 0) (.var (w + 1)))))366      (ex (.conj (.eq (.var 0) (.add (.var (w + 2)) (.var (w + 2)))) (seg J 1 0))))367368/-- `Int_J(x) := ∃ w (w = 1 ∧ seg_J(x, w))`. -/369def IntJ (J x : Nat) : Fm := ex (.conj (.eq (.var 0) .one) (seg J (x + 1) 0))370371/-- The values `seg_J(·, w)` admits, in the arithmetic of `M_p`: the multiples `c·w mod p` for `c < 2^J`, built level by372level. -/373def InSeg (p : Nat) : Nat → Nat → Nat → Prop374  | 0, _, x => x = 0375  | J + 1, w, x => ∃ y, y < p ∧ InSeg p J ((w + w) % p) y ∧ (x = y ∨ x = (y + w) % p)376377/-- 25:F7 (Lemma decoders, the semantics of `seg`) — `seg_J(x, w)` holds exactly when `x` is among the values the levels378admit. -/379theorem holds_seg_iff (p : Nat) : ∀ (J : Nat) (env : Nat → Nat) (x w : Nat),380    holds p env (seg J x w) = true ↔ InSeg p J (env w) (env x)381  | 0, env, x, w => by382    show decide (env x = 0) = true ↔ env x = 0383    exact ⟨of_decide_eq_true, decide_eq_true⟩384  | J + 1, env, x, w => by385    show holds p env (ex (.conj (orF (.eq (.var (x + 1)) (.var 0)) (.eq (.var (x + 1)) (.add (.var 0) (.var (w + 1)))))386      (ex (.conj (.eq (.var 0) (.add (.var (w + 2)) (.var (w + 2)))) (seg J 1 0))))) = true387      ↔ ∃ y, y < p ∧ InSeg p J ((env w + env w) % p) y ∧ (env x = y ∨ env x = (y + env w) % p)388    refine (holds_ex_iff p env _).trans ⟨?_, ?_⟩389    · intro ⟨y, hy, h⟩390      have h' := (holds_conj_iff _ _ _ _).1 h391      have hor := (holds_orF_iff _ _ _ _).1 h'.1392      have hin := (holds_ex_iff _ _ _).1 h'.2393      match hin with394      | ⟨w', hw', h2⟩ =>395        have h2' := (holds_conj_iff _ _ _ _).1 h2396        have ew' : w' = (env w + env w) % p := (holds_eq_iff _ _ _ _).1 h2'.1397        have hseg := (holds_seg_iff p J (cons w' (cons y env)) 1 0).1 h2'.2398        -- cons w' (cons y env) reads 0 ↦ w', 1 ↦ y399        have hseg' : InSeg p J ((env w + env w) % p) y := by400          have e : InSeg p J (cons w' (cons y env) 0) (cons w' (cons y env) 1) = InSeg p J w' y := rfl401          rw [e, ew'] at hseg; exact hseg402        refine ⟨y, hy, hseg', ?_⟩403        match hor with404        | .inl e => exact .inl ((holds_eq_iff _ _ _ _).1 e)405        | .inr e => exact .inr ((holds_eq_iff _ _ _ _).1 e)406    · intro ⟨y, hy, hseg, hor⟩407      refine ⟨y, hy, (holds_conj_iff _ _ _ _).2 ⟨(holds_orF_iff _ _ _ _).2 ?_, (holds_ex_iff _ _ _).2408        ⟨(env w + env w) % p, FRC.Nat.mod_lt' _ (Nat.lt_of_le_of_lt (Nat.zero_le _) hy),409          (holds_conj_iff _ _ _ _).2 ⟨(holds_eq_iff _ _ _ _).2 rfl, (holds_seg_iff p J _ 1 0).2 hseg⟩⟩⟩⟩410      match hor with411      | .inl e => exact .inl ((holds_eq_iff _ _ _ _).2 e)412      | .inr e => exact .inr ((holds_eq_iff _ _ _ _).2 e)413414/-- Every natural is `2c' + r` with `r < 2`, by induction (no division). -/415theorem half_decomp : ∀ c : Nat, ∃ c' r, r < 2 ∧ c = 2 * c' + r416  | 0 => ⟨0, 0, Nat.zero_lt_two, rfl⟩417  | c + 1 =>418    match half_decomp c with419    | ⟨c', 0, _, e⟩ => ⟨c', 1, Nat.lt_succ_self 1, by rw [e]⟩420    | ⟨c', 1, _, e⟩ => ⟨c' + 1, 0, Nat.zero_lt_two, by rw [e, Nat.mul_succ]⟩421    | ⟨_, r + 2, hr, _⟩ => absurd hr (Nat.not_lt_of_ge (Nat.le_add_left 2 r))422423theorem lt_of_two_mul_lt {a b : Nat} (h : 2 * a < 2 * b) : a < b :=424  Nat.lt_of_not_ge (fun hge => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le h (Nat.mul_le_mul_left 2 hge)))425426/-- 25:F7 (Lemma decoders, the arithmetic of the levels) — the values `seg_J(·, w)` admits are exactly the multiples427`c·w mod p` with `c < 2^J`. -/428theorem inSeg_iff (p : Nat) (hp : 0 < p) : ∀ (J w x : Nat), InSeg p J w x ↔ ∃ c, c < 2 ^ J ∧ x = (c * w) % p429  | 0, w, x => by430    show x = 0 ↔ ∃ c, c < 2 ^ 0 ∧ x = (c * w) % p431    exact ⟨fun e => ⟨0, Nat.lt_succ_self 0, by rw [e, Nat.zero_mul]; rfl⟩,432      fun ⟨c, hc, e⟩ => by433        have e0 : c = 0 := Nat.le_zero.1 (Nat.le_of_lt_succ hc)434        rw [e, e0, Nat.zero_mul]; rfl⟩435  | J + 1, w, x => by436    show (∃ y, y < p ∧ InSeg p J ((w + w) % p) y ∧ (x = y ∨ x = (y + w) % p)) ↔ ∃ c, c < 2 ^ (J + 1) ∧ x = (c * w) % p437    have key : ∀ c', (c' * ((w + w) % p)) % p = (2 * c' * w) % p := fun c' => by438      rw [FRC.Nat.mul_mod_mod _ _ _ hp, ← Nat.two_mul, FRC.Nat.mul_left_comm, ← FRC.Nat.mul_assoc]439    constructor440    · intro ⟨y, _, hy, hor⟩441      match (inSeg_iff p hp J _ y).1 hy with442      | ⟨c', hc', ey⟩ =>443        rw [key c'] at ey444        have hc'2 : 2 * c' < 2 * 2 ^ J := Nat.mul_lt_mul_of_pos_left hc' Nat.zero_lt_two445        match hor with446        | .inl e => exact ⟨2 * c', by rw [Nat.pow_succ, Nat.mul_comm (2 ^ J) 2]; exact hc'2, e.trans ey⟩447        | .inr e =>448          have h21 : 2 * c' + 1 < 2 * 2 ^ J := by449            have : 2 * (c' + 1) ≤ 2 * 2 ^ J := Nat.mul_le_mul_left 2 (Nat.succ_le_of_lt hc')450            rw [Nat.mul_succ] at this451            exact Nat.lt_of_lt_of_le (Nat.lt_succ_self _) this452          exact ⟨2 * c' + 1, by rw [Nat.pow_succ, Nat.mul_comm (2 ^ J) 2]; exact h21,453            by rw [e, ey, FRC.Nat.mod_add_mod _ _ _ hp, FRC.Nat.add_mul, Nat.one_mul]⟩454    · intro ⟨c, hc, ex⟩455      match half_decomp c with456      | ⟨c', r, hr, ec⟩ =>457        have hc' : c' < 2 ^ J := by458          have : 2 * c' < 2 * 2 ^ J := by459            rw [Nat.pow_succ, Nat.mul_comm (2 ^ J) 2] at hc460            exact Nat.lt_of_le_of_lt (Nat.le_add_right _ r) (ec ▸ hc)461          exact lt_of_two_mul_lt this462        refine ⟨(c' * ((w + w) % p)) % p, FRC.Nat.mod_lt' _ hp, (inSeg_iff p hp J _ _).2 ⟨c', hc', rfl⟩, ?_⟩463        rw [key c', ex, ec]464        match r, hr with465        | 0, _ => exact .inl (by rw [Nat.add_zero])466        | 1, _ => exact .inr (by rw [FRC.Nat.mod_add_mod _ _ _ hp, FRC.Nat.add_mul, Nat.one_mul])467        | r + 2, hr => exact absurd hr (Nat.not_lt_of_ge (Nat.le_add_left 2 r))468469/-- 25:F7 (Lemma decoders) — over `M_p` with `2^J ≤ p`, `Int_J(x)` holds exactly when `x < 2^J`: the formula defines470`{0, …, 2^J − 1}` by writing the binary expansion along `J` doublings of the unit. -/471theorem intJ_defines (p : Nat) (hp : 2 ≤ p) (J : Nat) (hJ : 2 ^ J ≤ p) (env : Nat → Nat) (x : Nat) (hx : env x < p) :472    holds p env (IntJ J x) = true ↔ env x < 2 ^ J := by473  have hp0 : 0 < p := Nat.lt_of_lt_of_le Nat.zero_lt_two hp474  show holds p env (ex (.conj (.eq (.var 0) .one) (seg J (x + 1) 0))) = true ↔ _475  refine (holds_ex_iff p env _).trans ⟨?_, ?_⟩476  · intro ⟨w, _, h⟩477    have h' := (holds_conj_iff _ _ _ _).1 h478    have ew : w = 1 % p := (holds_eq_iff _ _ _ _).1 h'.1479    rw [FRC.Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le Nat.one_lt_two hp)] at ew480    have hseg := (holds_seg_iff p J (cons w env) (x + 1) 0).1 h'.2481    have e : InSeg p J (cons w env 0) (cons w env (x + 1)) = InSeg p J w (env x) := rfl482    rw [e, ew] at hseg483    match (inSeg_iff p hp0 J 1 (env x)).1 hseg with484    | ⟨c, hc, ec⟩ =>485      rw [Nat.mul_one, FRC.Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le hc hJ)] at ec486      rw [ec]; exact hc487  · intro hlt488    refine ⟨1, Nat.lt_of_lt_of_le Nat.one_lt_two hp, (holds_conj_iff _ _ _ _).2489      ⟨(holds_eq_iff _ _ _ _).2 (FRC.Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le Nat.one_lt_two hp)).symm, ?_⟩⟩490    refine (holds_seg_iff p J (cons 1 env) (x + 1) 0).2 ?_491    show InSeg p J 1 (env x)492    exact (inSeg_iff p hp0 J 1 (env x)).2 ⟨env x, hlt, by rw [Nat.mul_one, FRC.Nat.mod_eq_of_lt hx]⟩493494/-- 25:F7 (Lemma decoders, the length) — `seg_J` has `25J + 3` symbols in this syntax (a variable is one symbol here; the495row's `50J + 29` counts the alphabet of 25:F8, where the names are spelt out). -/496theorem size_seg : ∀ (J x w : Nat), size (seg J x w) = 25 * J + 3497  | 0, _, _ => rfl498  | J + 1, x, w => by499    have e : size (seg (J + 1) x w) = 12 + (5 + size (seg J 1 0) + 1 + 1 + 1 + 1) + 1 + 1 + 1 + 1 := rfl500    rw [e, Nat.add_comm 12, Nat.add_comm 5, size_seg J 1 0, Nat.mul_succ]501502/-- 25:F7 (Lemma decoders, the length) — `Int_J` has `25J + 10` symbols: linear in `J`. -/503theorem size_IntJ (J x : Nat) : size (IntJ J x) = 25 * J + 10 := by504  have e : size (IntJ J x) = 3 + size (seg J (x + 1) 0) + 1 + 1 + 1 + 1 := rfl505  rw [e, Nat.add_comm 3, size_seg]506507/-! ### 00:Z9 — the window's digits against the totality -/508509/-- 00:Z9 (the window, in digit counts) — the chart's bound of `Ω` (`00:A7`, `Ω < 1.33 × 10^123`) has `82` base-32 digits510(`32^81 ≤ 1.32 × 10^123` and `1.33 × 10^123 < 32^82`), fewer than the `1,024` base-32 symbols an element of the511dense-coded instance of 25:F8 holds: that instance exists in no shell of the totality. No number above `Ω`'s digit bound512is named. -/513theorem window_beyond_totality : 32 ^ 81 ≤ 132 * 10 ^ 121 ∧ 133 * 10 ^ 121 < 32 ^ 82 ∧ 82 < 1024 := by decide514515end FRC.Diagonal516