Theme/Reach.lean — FrcCore

1import FrcCore.Theme.Logic23/-!4# FrcCore.Theme.Reach — the part and the reach bound (the logic theme; 25-godel's migration, 20 October 2026)56What a bounded part of a finite structure can hold, certify and derive, in the core's grammar and with no axioms:78* the term calculus of the wrap lemma (`Tm`, `val`, `Agree`): a term evaluated by table lookups takes the same value in9  every table that agrees on the entries the evaluation consults, so a certificate keeps its warrant in the small world10  built on its cited entries (25:D4, 25:J2); a term with `ℓ` leaves performs `ℓ − 1` lookups;11* abundance: every closed term over `1` and `+` with `ℓ` leaves has the value `ℓ mod p` in `M_p`, so any two terms with12  the same leaf count give a true equation, and the truths outrun every budget (25:E1, 25:G1);13* the reach bound: fewer than `a^(B+1)` records of length at most `B`, a fraction below `1/N` of a cohort of `2^L` truths14  once `L ≥ a^(B+1) N` (25:E2);15* aliasing: a reading of `m` elements by `R < m` states has a fibre of at least `⌈m/R⌉ ≥ 2` elements, and every element16  outside a maximal faithfully read range shares its reading with one inside (25:D3);17* the length horizon: a certificate contains its end sentence, so nothing longer than the budget is certified (25:G1);18* the evaluation ceiling: the one-rule system that asserts a sentence on exhaustive evaluation is sound and complete, its19  derivation of `φ` is `φ` itself, and the step check costs `m^q` atomic evaluations under `q` quantifiers (25:G2);20* the bare evaluation calculus: a derivation of a global clause from its `m` instances has at least `m + 1` lines, beyond21  every budget `H < m`, while the universal rule is sound (25:E4);22* the trichotomy's middle cell on its finite parts: the sentences "at least `n` elements" with a free unary predicate have23  models of `N` elements with the predicate inhabited and with it empty for every `n ≤ N`, and no structure of `N`24  elements satisfies "at least `N + 1` elements" (25:H5).2526The paper module `FrcCore/Godel.lean` keeps every old name as an alias.27-/2829namespace FRC.Reach3031open FRC.Logic3233/-! ### 25:D4, 25:E1 — closed terms, their values, and the entries an evaluation consults -/3435/-- Closed terms over one constant and one binary operation: the full binary trees. -/36inductive Tm where37  | one : Tm38  | op : Tm → Tm → Tm3940/-- The value of a term in the structure with the constant read as `u` and the operation's table `f`. -/41def val (u : Nat) (f : Nat → Nat → Nat) : Tm → Nat42  | .one => u43  | .op s t => f (val u f s) (val u f t)4445/-- `g` agrees with `f` on every table entry the evaluation of the term in `(u, f)` consults. -/46def Agree (u : Nat) (f g : Nat → Nat → Nat) : Tm → Prop47  | .one => True48  | .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)4950/-- The number of leaves of a term. -/51def leaves : Tm → Nat52  | .one => 153  | .op s t => leaves s + leaves t5455/-- The number of table lookups the evaluation of a term performs: one per operation. -/56def lookups : Tm → Nat57  | .one => 058  | .op s t => lookups s + lookups t + 15960/-- 25:D4, 25:J2 (Lemma wrap (2), the trace argument) — a structure that agrees with `M` on the entries the evaluation61consults gives the term the same value: the verification succeeds there step for step. -/62theorem trace_transport (u : Nat) (f g : Nat → Nat → Nat) : ∀ t : Tm, Agree u f g t → val u g t = val u f t63  | .one, _ => rfl64  | .op s t, ⟨hs, ht, e⟩ => by65    show g (val u g s) (val u g t) = f (val u f s) (val u f t)66    rw [trace_transport u f g s hs, trace_transport u f g t ht]; exact e6768/-- 25:D4, 25:J2 (Lemma wrap (2), the end sentence) — an equation verified by evaluation in `M` is true in every other69table that agrees with `M` on the cited entries: the certificate keeps its warrant in the small world. -/70theorem wrap_equation (u : Nat) (f g : Nat → Nat → Nat) (s t : Tm) (hs : Agree u f g s) (ht : Agree u f g t)71    (h : val u f s = val u f t) : val u g s = val u g t := by72  rw [trace_transport u f g s hs, trace_transport u f g t ht]; exact h7374/-- 25:D4 (Lemma wrap (2), the size of the trace) — the evaluation of a term with `ℓ` leaves performs `ℓ − 1`75lookups. -/76theorem lookups_succ : ∀ t : Tm, lookups t + 1 = leaves t77  | .one => rfl78  | .op s t => by79    show lookups s + lookups t + 1 + 1 = leaves s + leaves t80    rw [← lookups_succ s, ← lookups_succ t]81    exact (FRC.Nat.add_add_add_comm (lookups s) 1 (lookups t) 1).symm8283/-- 25:E1 (Lemma abundance, the value) — in `M_p` the closed term over `1` and `+` with `ℓ` leaves has the84value `ℓ mod p`, whatever its shape. -/85theorem value_leaves (p : Nat) (hp : 0 < p) :86    ∀ t : Tm, val (1 % p) (fun x y => (x + y) % p) t = leaves t % p87  | .one => rfl88  | .op s t => by89    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) % p90    rw [value_leaves p hp s, value_leaves p hp t]91    exact (FRC.Nat.add_mod (leaves s) (leaves t) p hp).symm9293/-- 25:E1 (Lemma abundance, the cohort) — any two terms with the same number of leaves give a true equation94of `M_p`. -/95theorem equal_leaves_equal_value (p : Nat) (hp : 0 < p) (s t : Tm) (h : leaves s = leaves t) :96    val (1 % p) (fun x y => (x + y) % p) s = val (1 % p) (fun x y => (x + y) % p) t := by97  rw [value_leaves p hp s, value_leaves p hp t, h]9899/-- The left comb with `n + 1` leaves: `((1 + 1) + 1) + …`. -/100def combL : Nat → Tm101  | 0 => .one102  | n + 1 => .op (combL n) .one103104/-- The right comb with `n + 1` leaves: `1 + (1 + (1 + …))`. -/105def combR : Nat → Tm106  | 0 => .one107  | n + 1 => .op .one (combR n)108109theorem leaves_combL : ∀ n, leaves (combL n) = n + 1110  | 0 => rfl111  | n + 1 => by show leaves (combL n) + 1 = n + 1 + 1; rw [leaves_combL n]112113theorem leaves_combR : ∀ n, leaves (combR n) = n + 1114  | 0 => rfl115  | n + 1 => by show 1 + leaves (combR n) = n + 1 + 1; rw [leaves_combR n, Nat.add_comm]116117/-- 25:G1, 25:E1 (Proposition lengthhorizon, "beyond every budget there are truths") — for every budget `B` the two combs118with `B + 1` leaves give a true equation of `M_p` whose sides have more than `B` leaves each, so more than `B`119symbols: a truth no certificate of length `B` contains. -/120theorem truths_beyond_budget (p : Nat) (hp : 0 < p) (B : Nat) :121    ∃ s t : Tm, leaves s = leaves t ∧ B < leaves s ∧122      val (1 % p) (fun x y => (x + y) % p) s = val (1 % p) (fun x y => (x + y) % p) t :=123  ⟨combL B, combR B, by rw [leaves_combL, leaves_combR], by rw [leaves_combL]; exact Nat.lt_succ_self B,124    equal_leaves_equal_value p hp _ _ (by rw [leaves_combL, leaves_combR])⟩125126/-! ### 25:E2 — the reach bound -/127128/-- 25:E2, 25:G7 (Proposition reach, the vanishing fraction in finite form) — against a cohort of `2^L` truths the129records of length at most `B` certify a fraction below `1/N` once `L ≥ a^(B+1)·N`: their number times `N` is130below `2^L`. -/131theorem reach_vanishes (a : Nat) (ha : 2 ≤ a) (B N L : Nat) (h : a ^ (B + 1) * N ≤ L) :132    FRC.Logic.records a B * N < 2 ^ L :=133  Nat.lt_of_le_of_lt134    (Nat.le_trans (Nat.mul_le_mul_right N (Nat.le_of_lt (FRC.Logic.records_lt a ha B))) h)135    Nat.lt_two_pow_self136137/-! ### sums over an initial segment, for the fibre and derivation counts -/138139/-- `g 0 + … + g (R − 1)`. -/140def sumBelow (g : Nat → Nat) : Nat → Nat141  | 0 => 0142  | R + 1 => sumBelow g R + g R143144theorem sumBelow_congr {g h : Nat → Nat} : ∀ {R : Nat}, (∀ r, r < R → g r = h r) → sumBelow g R = sumBelow h R145  | 0, _ => rfl146  | R + 1, e => by147    show sumBelow g R + g R = sumBelow h R + h R148    rw [sumBelow_congr (fun r hr => e r (Nat.lt_succ_of_lt hr)), e R (Nat.lt_succ_self R)]149150theorem sumBelow_add (g h : Nat → Nat) : ∀ R, sumBelow (fun r => g r + h r) R = sumBelow g R + sumBelow h R151  | 0 => rfl152  | R + 1 => by153    show sumBelow (fun r => g r + h r) R + (g R + h R) = sumBelow g R + g R + (sumBelow h R + h R)154    rw [sumBelow_add g h R]; exact FRC.Nat.add_add_add_comm _ _ _ _155156theorem sumBelow_const (c : Nat) : ∀ R, sumBelow (fun _ => c) R = R * c157  | 0 => (Nat.zero_mul c).symm158  | R + 1 => by show sumBelow (fun _ => c) R + c = (R + 1) * c; rw [sumBelow_const c R, Nat.succ_mul]159160theorem sumBelow_le_sumBelow {g h : Nat → Nat} : ∀ {R : Nat}, (∀ r, r < R → g r ≤ h r) → sumBelow g R ≤ sumBelow h R161  | 0, _ => Nat.le_refl 0162  | R + 1, e => Nat.add_le_add (sumBelow_le_sumBelow (fun r hr => e r (Nat.lt_succ_of_lt hr))) (e R (Nat.lt_succ_self R))163164/-- The indicator `[x = r]` summed over `r < R` is `1` when `x < R` and `0` otherwise. -/165theorem sumBelow_indicator (x : Nat) : ∀ R, sumBelow (fun r => cond (decide (x = r)) 1 0) R = if x < R then 1 else 0166  | 0 => rfl167  | R + 1 => by168    show sumBelow (fun r => cond (decide (x = r)) 1 0) R + cond (decide (x = R)) 1 0 = if x < R + 1 then 1 else 0169    rw [sumBelow_indicator x R]170    match Nat.lt_or_ge x R with171    | .inl hlt =>172      have hne : x ≠ R := Nat.ne_of_lt hlt173      rw [ite_eq_left hlt, ite_eq_left (Nat.lt_succ_of_lt hlt), decide_eq_false hne]; rfl174    | .inr hge =>175      rw [ite_eq_right (Nat.not_lt_of_ge hge)]176      match Nat.eq_or_lt_of_le hge with177      | .inl heq => rw [decide_eq_true heq.symm, ite_eq_left (heq ▸ Nat.lt_succ_self R)]; rfl178      | .inr hgt =>179        have hne : x ≠ R := fun e => Nat.lt_irrefl R (e ▸ hgt)180        rw [decide_eq_false hne, ite_eq_right (Nat.not_lt_of_ge (Nat.succ_le_of_lt hgt))]; rfl181182/-- If the sum of `g` over `r < R` exceeds `R · c`, some `g r` exceeds `c` (constructively, by the case split on `g R`). -/183theorem exists_gt_of_sumBelow_gt (g : Nat → Nat) (c : Nat) : ∀ R, R * c < sumBelow g R → ∃ r, r < R ∧ c < g r184  | 0, h => by rw [Nat.zero_mul] at h; exact absurd h (Nat.lt_irrefl 0)185  | R + 1, h => by186    match Nat.lt_or_ge c (g R) with187    | .inl hgt => exact ⟨R, Nat.lt_succ_self R, hgt⟩188    | .inr hle =>189      have h' : R * c < sumBelow g R := by190        have e : (R + 1) * c = R * c + c := Nat.succ_mul R c191        have : R * c + c < sumBelow g R + g R := e ▸ h192        exact Nat.lt_of_add_lt_add_right (Nat.lt_of_lt_of_le this (Nat.add_le_add_left hle _))193      match exists_gt_of_sumBelow_gt g c R h' with194      | ⟨r, hr, hc⟩ => exact ⟨r, Nat.lt_succ_of_lt hr, hc⟩195196/-! ### 25:D3 — aliasing: the fibres of a reading -/197198/-- The number of elements below `m` that the reading `ρ` sends to `r`. -/199def fibre (ρ : Nat → Nat) (r m : Nat) : Nat := count (fun i => decide (ρ i = r)) m200201/-- The fibres of a reading into `[0, R)` partition `[0, m)`: their sizes sum to `m`. -/202theorem sumBelow_fibre (ρ : Nat → Nat) (R : Nat) : ∀ m, (∀ i, i < m → ρ i < R) → sumBelow (fun r => fibre ρ r m) R = m203  | 0, _ => sumBelow_const 0 R ▸ (Nat.mul_zero R).symm ▸ rfl204  | m + 1, h => by205    have e : ∀ r, fibre ρ r (m + 1) = fibre ρ r m + cond (decide (ρ m = r)) 1 0 := fun r => rfl206    rw [sumBelow_congr (fun r _ => e r), sumBelow_add, sumBelow_fibre ρ R m (fun i hi => h i (Nat.lt_succ_of_lt hi)),207      sumBelow_indicator, ite_eq_left (h m (Nat.lt_succ_self m))]208209/-- 25:D3 (Lemma wrap (1), the fibre) — a reading of `m` elements by `R` states has a fibre of more than `c` elements210for every `c` with `R · c < m`: the largest such `c + 1` is `⌈m/R⌉`, stated without division. -/211theorem alias_fibre (ρ : Nat → Nat) (m R : Nat) (hρ : ∀ i, i < m → ρ i < R) (c : Nat) (hc : R * c < m) :212    ∃ r, r < R ∧ c + 1 ≤ fibre ρ r m := by213  have hsum : sumBelow (fun r => fibre ρ r m) R = m := sumBelow_fibre ρ R m hρ214  have hlt : R * c < sumBelow (fun r => fibre ρ r m) R := by rw [hsum]; exact hc215  match exists_gt_of_sumBelow_gt _ _ R hlt with216  | ⟨r, hr, hgt⟩ => exact ⟨r, hr, Nat.succ_le_of_lt hgt⟩217218/-- 25:D3 (Lemma wrap (1), at least two) — with fewer states than elements some reading stands for at least two219elements (the pigeonhole of 25:D1, counted). -/220theorem alias_two (ρ : Nat → Nat) (m R : Nat) (hρ : ∀ i, i < m → ρ i < R) (h : R < m) :221    ∃ r, r < R ∧ 2 ≤ fibre ρ r m :=222  alias_fibre ρ m R hρ 1 (by rw [Nat.mul_one]; exact h)223224/-- `S` is read faithfully: `ρ` is injective on the elements of `S` below `m`. -/225def Faithful (ρ : Nat → Nat) (S : Nat → Bool) (m : Nat) : Prop :=226  ∀ i j, i < m → j < m → S i = true → S j = true → ρ i = ρ j → i = j227228/-- The range `S` with one more element `x`. -/229def adjoin (S : Nat → Bool) (x : Nat) : Nat → Bool := fun y => S y || decide (y = x)230231theorem anyBelow_true_iff (f : Nat → Bool) : ∀ n, anyBelow f n = true ↔ ∃ x, x < n ∧ f x = true232  | 0 => ⟨fun h => Bool.noConfusion h, fun ⟨_, hx, _⟩ => absurd hx (Nat.not_lt_zero _)⟩233  | n + 1 => by234    show (f n || anyBelow f n) = true ↔ _235    have ih := anyBelow_true_iff f n236    match hf : f n with237    | true => exact ⟨fun _ => ⟨n, Nat.lt_succ_self n, hf⟩, fun _ => rfl⟩238    | false => exact ⟨fun h => match ih.1 h with | ⟨x, hx, e⟩ => ⟨x, Nat.lt_succ_of_lt hx, e⟩,239        fun ⟨x, hx, e⟩ => match Nat.lt_or_ge x n with240          | .inl hlt => ih.2 ⟨x, hlt, e⟩241          | .inr hge => Bool.noConfusion ((Nat.le_antisymm (Nat.le_of_lt_succ hx) hge ▸ e).symm.trans hf)⟩242243/-- 25:D3 (Lemma wrap (1), the alias) — if `S` is a maximal faithfully read range (adjoining any element outside it244breaks injectivity), every element `x < m` outside `S` is read as an alias of an element inside it. -/245theorem alias_outside (ρ : Nat → Nat) (S : Nat → Bool) (m : Nat) (hS : Faithful ρ S m)246    (hmax : ∀ x, x < m → S x = false → ¬ Faithful ρ (adjoin S x) m) (x : Nat) (hx : x < m) (hxS : S x = false) :247    ∃ s, s < m ∧ S s = true ∧ ρ s = ρ x := by248  match h : anyBelow (fun s => S s && decide (ρ s = ρ x)) m with249  | true =>250    match (anyBelow_true_iff _ m).1 h with251    | ⟨s, hs, e⟩ => exact ⟨s, hs, band_l e, of_decide_eq_true (band_r e)⟩252  | false =>253    exfalso254    apply hmax x hx hxS255    intro i j hi hj hSi hSj hij256    have hno : ∀ s, s < m → S s = true → ρ s ≠ ρ x := fun s hs hSs e =>257      Bool.noConfusion (((anyBelow_true_iff _ m).2 ⟨s, hs, by rw [hSs, decide_eq_true e]; rfl⟩).symm.trans h)258    -- each of i, j is in S or equals x259    have ci : S i = true ∨ i = x := match hi' : S i with260      | true => .inl rfl261      | false => .inr (of_decide_eq_true (by262          have : (S i || decide (i = x)) = true := hSi263          rw [hi'] at this; exact this))264    have cj : S j = true ∨ j = x := match hj' : S j with265      | true => .inl rfl266      | false => .inr (of_decide_eq_true (by267          have : (S j || decide (j = x)) = true := hSj268          rw [hj'] at this; exact this))269    match ci, cj with270    | .inl si, .inl sj => exact hS i j hi hj si sj hij271    | .inl si, .inr ej => exact absurd (ej ▸ hij) (hno i hi si)272    | .inr ei, .inl sj => exact absurd (ei ▸ hij.symm) (hno j hj sj)273    | .inr ei, .inr ej => exact ei.trans ej.symm274275/-! ### 25:G1, 25:G2 — certificates, the length horizon, the one-rule system -/276277/-- The length of a formula over a relational signature, in symbols. -/278def fsize : FForm → Nat279  | .rel _ xs => xs.length + 1280  | .eq _ _ => 3281  | .neg φ => fsize φ + 1282  | .conj φ ψ => fsize φ + fsize ψ + 1283  | .all φ => fsize φ + 1284285/-- The length of a record: the lengths of its lines. -/286def csize : List FForm → Nat287  | [] => 0288  | φ :: l => fsize φ + csize l289290theorem fsize_le_csize_of_mem {φ : FForm} : ∀ {l : List FForm}, φ ∈ l → fsize φ ≤ csize l291  | _ :: l, .head _ => Nat.le_add_right (fsize φ) (csize l)292  | ψ :: l, .tail _ h => Nat.le_trans (fsize_le_csize_of_mem h) (Nat.le_add_left (csize l) (fsize ψ))293294/-- 25:G1, 25:G7 (Proposition lengthhorizon) — a certificate contains its designated end sentence, so a record of length at295most `B` certifies no sentence longer than `B`: nothing longer than the budget is certifiable in any system. -/296theorem length_horizon (l : List FForm) (φ : FForm) (hmem : φ ∈ l) (B : Nat) (hB : csize l ≤ B) : fsize φ ≤ B :=297  Nat.le_trans (fsize_le_csize_of_mem hmem) hB298299/-- 25:G1 (Proposition lengthhorizon, contrapositive) — a sentence longer than `H` has no derivation of length at most300`H` in any system whose derivations contain their conclusion. -/301theorem no_short_derivation (l : List FForm) (φ : FForm) (hmem : φ ∈ l) (H : Nat) (hφ : H < fsize φ) :302    ¬ csize l ≤ H := fun h => Nat.lt_irrefl H (Nat.lt_of_lt_of_le hφ (length_horizon l φ hmem H h))303304/-- The one-rule system `D_tt`: a sentence is derived, in one line, exactly when exhaustive evaluation makes it true. -/305def DttDerives (M : FinStr) (env : Nat → Nat) (φ : FForm) : Prop := fval M env φ = true306307/-- 25:G2 (Proposition dtruth, soundness and completeness) — `D_tt` derives exactly the true sentences. -/308theorem dtt_sound_complete (M : FinStr) (env : Nat → Nat) (φ : FForm) : DttDerives M env φ ↔ Sat M env φ :=309  fin_theory_decidable M φ env310311/-- 25:G2 (Proposition dtruth, the ceiling) — the derivation of `φ` in `D_tt` is the line `φ`, of length `|φ|`: a truth312has a derivation of length at most `H` exactly when it is no longer than `H`. -/313theorem dtt_ceiling (M : FinStr) (env : Nat → Nat) (φ : FForm) (H : Nat) :314    (Sat M env φ ∧ csize [φ] ≤ H) ↔ (DttDerives M env φ ∧ fsize φ ≤ H) :=315  ⟨fun ⟨hs, hl⟩ => ⟨(fin_theory_decidable M φ env).2 hs, by simpa [csize] using hl⟩,316   fun ⟨hd, hl⟩ => ⟨(fin_theory_decidable M φ env).1 hd, by simpa [csize] using hl⟩⟩317318/-- The atomic evaluations the exhaustive evaluator performs: each quantifier multiplies by the `m` elements. -/319def cost (M : FinStr) : FForm → Nat320  | .rel _ _ => 1321  | .eq _ _ => 1322  | .neg φ => cost M φ323  | .conj φ ψ => cost M φ + cost M ψ324  | .all φ => M.m * cost M φ325326/-- A prefix of `q` universal quantifiers. -/327def allBlock : Nat → FForm → FForm328  | 0, φ => φ329  | q + 1, φ => .all (allBlock q φ)330331/-- 25:G2 (Proposition dtruth, the step check) — under `q` quantifiers the step check of `D_tt` performs `m^q` times the332matrix's atomic evaluations. -/333theorem cost_allBlock (M : FinStr) : ∀ (q : Nat) (φ : FForm), cost M (allBlock q φ) = M.m ^ q * cost M φ334  | 0, φ => (Nat.one_mul _).symm335  | q + 1, φ => by336    show M.m * cost M (allBlock q φ) = M.m ^ (q + 1) * cost M φ337    rw [cost_allBlock M q φ, Nat.pow_succ, Nat.mul_comm (M.m ^ q) M.m, Nat.mul_assoc]338339/-! ### 25:E4 — the bare evaluation calculus and the global clause -/340341/-- A line of the bare calculus: an instance `φ(c)` checked by evaluation, or the universal rule. -/342inductive Line where343  | inst : Nat → Line344  | univ : Line345346/-- Whether the instance `φ(c)` occurs among the lines. -/347def hasInst : List Line → Nat → Bool348  | [], _ => false349  | .inst d :: l, c => decide (d = c) || hasInst l c350  | .univ :: l, c => hasInst l c351352/-- The number of lines that are the instance `φ(c)`. -/353def countInst : List Line → Nat → Nat354  | [], _ => 0355  | .inst d :: l, c => countInst l c + cond (decide (d = c)) 1 0356  | .univ :: l, c => countInst l c357358/-- The universal rule applies when every one of the `m` instances is among the premises. -/359def RuleApplies (m : Nat) (l : List Line) : Prop := ∀ c, c < m → hasInst l c = true360361theorem one_le_countInst : ∀ (l : List Line) (c : Nat), hasInst l c = true → 1 ≤ countInst l c362  | .inst d :: l, c, h => by363    show 1 ≤ countInst l c + cond (decide (d = c)) 1 0364    match hd : decide (d = c) with365    | true => exact Nat.le_add_left 1 _366    | false =>367      have h' : hasInst l c = true := by368        have : (decide (d = c) || hasInst l c) = true := h369        rw [hd] at this; exact this370      exact Nat.le_trans (one_le_countInst l c h') (Nat.le_add_right _ _)371  | .univ :: l, c, h => one_le_countInst l c h372373theorem sumBelow_countInst_le (m : Nat) : ∀ l : List Line, sumBelow (fun c => countInst l c) m ≤ l.length374  | [] => by375    have e : sumBelow (countInst []) m = sumBelow (fun _ => 0) m := sumBelow_congr (fun _ _ => rfl)376    rw [e, sumBelow_const, Nat.mul_zero]; exact Nat.le_refl 0377  | .inst d :: l => by378    show sumBelow (fun c => countInst l c + cond (decide (d = c)) 1 0) m ≤ l.length + 1379    rw [sumBelow_add, sumBelow_indicator]380    exact Nat.add_le_add (sumBelow_countInst_le m l) (by split <;> decide)381  | .univ :: l => Nat.le_trans (sumBelow_countInst_le m l) (Nat.le_succ _)382383/-- 25:E4 (Remark globalclause, the length) — a derivation whose universal rule applies lists all `m` instances, so it has384at least `m` lines before the rule and `m + 1` with it. -/385theorem global_clause_length (m : Nat) (l : List Line) (h : RuleApplies m l) : m ≤ l.length :=386  have h1 : sumBelow (fun _ => 1) m ≤ sumBelow (fun c => countInst l c) m :=387    sumBelow_le_sumBelow (fun c hc => one_le_countInst l c (h c hc))388  Nat.le_trans (by rw [sumBelow_const, Nat.mul_one] at h1; exact h1) (sumBelow_countInst_le m l)389390/-- 25:E4 (Remark globalclause, the budget) — every derivation of a global clause in the bare calculus, the rule line391included (`l.length + 1` lines), has more than `m` lines, so none fits a budget `H < m`. -/392theorem global_clause_defeats_budget (m : Nat) (l : List Line) (h : RuleApplies m l) (H : Nat) (hH : H < m) :393    ¬ l.length + 1 ≤ H := fun hle =>394  have : m + 1 ≤ H := Nat.le_trans (Nat.add_le_add_right (global_clause_length m l h) 1) hle395  Nat.lt_irrefl H (Nat.lt_of_lt_of_le hH (Nat.le_of_succ_le this))396397/-- 25:E4 (Remark globalclause, soundness) — the universal rule is sound: when the `m` instances of `φ` evaluate true in398the structure, the global clause `∀ x φ(x)` holds there. -/399theorem bare_rule_sound (M : FinStr) (env : Nat → Nat) (φ : FForm)400    (h : ∀ c, c < M.m → fval M (cons c env) φ = true) : Sat M env (.all φ) :=401  fun x hx => (fin_theory_decidable M φ (cons x env)).1 (h x hx)402403/-! ### 25:H5 — the trichotomy's middle cell on its finite parts -/404405/-- `x₀ ≠ x_k ∧ … ∧ x_{i−1} ≠ x_k`: the variable `k` differs from the first `i` variables. -/406def diffs : Nat → Nat → FForm407  | 0, _ => .eq 0 0408  | i + 1, k => .conj (diffs i k) (.neg (.eq i k))409410/-- The first `n` variables are pairwise distinct. -/411def distinct : Nat → FForm412  | 0 => .eq 0 0413  | k + 1 => .conj (distinct k) (diffs k k)414415/-- `∃ x φ`, with the language's one quantifier. -/416def exF (φ : FForm) : FForm := .neg (.all (.neg φ))417418/-- A block of `n` existential quantifiers. -/419def exBlockF : Nat → FForm → FForm420  | 0, φ => φ421  | n + 1, φ => exF (exBlockF n φ)422423/-- The sentence "at least `n` elements": `n` distinct elements exist. -/424def atLeast (n : Nat) : FForm := exBlockF n (distinct n)425426/-- The sentence "the predicate `P` (relation symbol `0`) is inhabited". -/427def someP : FForm := exF (.rel 0 [0])428429theorem sat_diffs (M : FinStr) (env : Nat → Nat) : ∀ (i k : Nat), Sat M env (diffs i k) ↔ ∀ j, j < i → env j ≠ env k430  | 0, _ => ⟨fun _ j hj => absurd hj (Nat.not_lt_zero j), fun _ => rfl⟩431  | i + 1, k =>432    have ih := sat_diffs M env i k433    ⟨fun h j hj =>434      have h' : Sat M env (diffs i k) ∧ ¬ env i = env k := h435      match Nat.lt_or_ge j i with436      | .inl hlt => ih.1 h'.1 j hlt437      | .inr hge => by438        have e : j = i := Nat.le_antisymm (Nat.le_of_lt_succ hj) hge439        subst e; exact h'.2,440     fun h => show Sat M env (diffs i k) ∧ ¬ env i = env k from441      ⟨ih.2 (fun j hj => h j (Nat.lt_succ_of_lt hj)), h i (Nat.lt_succ_self i)⟩⟩442443theorem sat_distinct (M : FinStr) (env : Nat → Nat) :444    ∀ n, Sat M env (distinct n) ↔ ∀ j k, j < k → k < n → env j ≠ env k445  | 0 => ⟨fun _ _ k _ hk => absurd hk (Nat.not_lt_zero k), fun _ => rfl⟩446  | k + 1 =>447    have ih := sat_distinct M env k448    have id := sat_diffs M env k k449    ⟨fun h j k' hj hk' =>450      have h' : Sat M env (distinct k) ∧ Sat M env (diffs k k) := h451      match Nat.lt_or_ge k' k with452      | .inl hlt => ih.1 h'.1 j k' hj hlt453      | .inr hge => by454        have e : k' = k := Nat.le_antisymm (Nat.le_of_lt_succ hk') hge455        subst e; exact id.1 h'.2 j hj,456     fun h => show Sat M env (distinct k) ∧ Sat M env (diffs k k) from457      ⟨ih.2 (fun j k' hj hk' => h j k' hj (Nat.lt_succ_of_lt hk')), id.2 (fun j hj => h j k hj (Nat.lt_succ_self k))⟩⟩458459/-- A witness below `m` gives the existential sentence. -/460theorem sat_exF_of (M : FinStr) (env : Nat → Nat) (φ : FForm) (x : Nat) (hx : x < M.m) (h : Sat M (cons x env) φ) :461    Sat M env (exF φ) := fun hall => hall x hx h462463/-- Choosing the elements `k, k − 1, …` from the outside in: after `k` more quantifiers the first `n` variables read464`0, …, n − 1` in reverse order. -/465theorem sat_exBlock_distinct (M : FinStr) (n : Nat) (hn : n ≤ M.m) :466    ∀ (k : Nat) (env : Nat → Nat), k ≤ n → (∀ i, i < n - k → env i = i + k) → Sat M env (exBlockF k (distinct n))467  | 0, env, _, h => (sat_distinct M env n).2 (fun j k hj hk e => by468      rw [h j (by rw [Nat.sub_zero]; exact Nat.lt_trans hj hk), h k (by rw [Nat.sub_zero]; exact hk)] at e469      exact Nat.ne_of_lt hj (Nat.add_right_cancel e))470  | k + 1, env, hk, h =>471    sat_exF_of M env _ k (Nat.lt_of_lt_of_le (Nat.lt_of_lt_of_le (Nat.lt_succ_self k) hk) hn)472      (sat_exBlock_distinct M n hn k (cons k env) (Nat.le_of_succ_le hk) (fun i hi => by473        match i with474        | 0 => show k = 0 + k; exact (Nat.zero_add k).symm475        | i + 1 =>476          show env i = i + 1 + k477          have : i < n - (k + 1) := by478            have h1 : i + 1 < n - k := hi479            have h2 : n - k = n - (k + 1) + 1 := by480              rw [Nat.sub_succ]; exact (Nat.succ_pred_eq_of_pos (Nat.lt_of_le_of_lt (Nat.zero_le _) h1)).symm481            rw [h2] at h1; exact Nat.lt_of_succ_lt_succ h1482          rw [h i this, Nat.add_assoc, Nat.add_comm 1 k]))483484/-- 25:H5 (Corollary trichotomy, cell (ii) on its finite parts) — a structure of `N` elements satisfies "at least `n`485elements" for every `n ≤ N`. -/486theorem atLeast_of_le (M : FinStr) (env : Nat → Nat) (n : Nat) (hn : n ≤ M.m) : Sat M env (atLeast n) :=487  sat_exBlock_distinct M n hn n env (Nat.le_refl n) (fun i hi => absurd hi (by rw [Nat.sub_self]; exact Nat.not_lt_zero i))488489/-- No structure of `m < n` elements has `n` distinct elements: the chosen values collide (25:D1's pigeonhole). -/490theorem not_exBlock_distinct (M : FinStr) (n : Nat) (hn : M.m < n) :491    ∀ (k : Nat) (env : Nat → Nat), (∀ i, i < n - k → env i < M.m) → ¬ Sat M env (exBlockF k (distinct n))492  | 0, env, h, hs =>493    part_collides hn env (fun i hi => h i (by rw [Nat.sub_zero]; exact hi))494      (fun i j hi hj e => match Nat.lt_or_ge i j with495        | .inl hlt => absurd e ((sat_distinct M env n).1 hs i j hlt hj)496        | .inr hge => match Nat.eq_or_lt_of_le hge with497          | .inl heq => heq.symm498          | .inr hgt => absurd e.symm ((sat_distinct M env n).1 hs j i hgt hi))499  | k + 1, env, h, hs =>500    hs (fun x hx => not_exBlock_distinct M n hn k (cons x env) (fun i hi => by501      match i with502      | 0 => exact hx503      | i + 1 =>504        show env i < M.m505        apply h i506        have h1 : i + 1 < n - k := hi507        have h2 : n - k = n - (k + 1) + 1 := by508          rw [Nat.sub_succ]; exact (Nat.succ_pred_eq_of_pos (Nat.lt_of_le_of_lt (Nat.zero_le _) h1)).symm509        rw [h2] at h1; exact Nat.lt_of_succ_lt_succ h1))510511/-- 25:H5 (Corollary trichotomy, cell (ii) on its finite parts) — no structure of `N` elements satisfies "at least512`N + 1` elements": the finite parts of the theory bound the models they admit. -/513theorem not_atLeast_succ (M : FinStr) (env : Nat → Nat) : ¬ Sat M env (atLeast (M.m + 1)) :=514  not_exBlock_distinct M (M.m + 1) (Nat.lt_succ_self M.m) (M.m + 1) env515    (fun i hi => absurd hi (by rw [Nat.sub_self]; exact Nat.not_lt_zero i))516517/-- The structure of `N` elements with the predicate everywhere true. -/518def withP (N : Nat) : FinStr := ⟨N, fun _ _ => true⟩519520/-- The structure of `N` elements with the predicate everywhere false. -/521def withoutP (N : Nat) : FinStr := ⟨N, fun _ _ => false⟩522523/-- 25:H5 (Corollary trichotomy, cell (ii) on its finite parts) — for every `N ≥ 1` the first `N` sentences "at least524`n` elements" have a model of `N` elements with `∃ x P(x)` true and one with it false, so they decide neither it nor its525negation; and `∀ x ¬P(x)` settles it. -/526theorem middle_cell_undecided (N : Nat) (hN : 0 < N) (env : Nat → Nat) :527    (∀ n, n ≤ N → Sat (withP N) env (atLeast n)) ∧ Sat (withP N) env someP ∧528    (∀ n, n ≤ N → Sat (withoutP N) env (atLeast n)) ∧ ¬ Sat (withoutP N) env someP :=529  ⟨fun n hn => atLeast_of_le (withP N) env n hn,530   sat_exF_of (withP N) env _ 0 hN rfl,531   fun n hn => atLeast_of_le (withoutP N) env n hn,532   fun hs => hs (fun _ _ h => Bool.noConfusion h)⟩533534end FRC.Reach535