Theme/Threshold.lean — FrcCore

1import FrcCore.Theme.Diagonal23/-!4# FrcCore.Theme.Threshold — the threshold of the dense coding (the logic theme; 25-godel's migration, 20 October 2026)56What the names of the diagonal template cost, and where the count closes (25:F6, 00:Z9), with no axioms. The `k`7shortest distinct names over `a` letters cost `c(k)` symbols (`nameCost`), and `kJ + 2 ≤ c(k) + 2a^J` for every `J`8(`nameCost_lower`): a name is one symbol at least, and at most `2a^j − 2` names have `j` letters or fewer. A dense instance9with `k` coordinates in `v` and `k₁` in `u` needs `2c(k) + c(k + k₁) < d·k₁` and `3c(k) + k₁ < d·k` (`admits`, 25:F4),10which force `k < 6a^{⌊d/3⌋+1}` (`admits_bound`; `k` has at most `⌊d/3⌋ + 4` base-`a` digits, `admits_digits`),11`k < 6a^{⌊d/4⌋+1}` at one scale (`one_scale_bound`), and nothing at `d ≤ 4` (`no_instance_small_d`). The largest admitted12`k` is `k*` (`kstar`, a bounded search that misses nothing, `kstar_max`), the threshold is `t = d·k*`, no instance codes13`λ` at length `n ≥ t` (`no_instance_at_threshold`, with 25:F4's digit bound), and `t < a^{d−1} ≤ m` in every structure14(`threshold_lt`, `threshold_digits`): for `d ≥ 13` and for `a ≥ 6` by `6d·a^{⌊d/3⌋+1} ≤ a^{d−1}`, the pairs with `a ≤ 5`15and `5 ≤ d ≤ 12` by the kernel's computation of `k*`. `⌊d/3⌋` and `⌊d/4⌋` are `third` and `quarter`, by recursion.16-/1718namespace FRC.Diagonal1920open FRC.Logic FRC.Reach2122/-! ### 25:F6 — the threshold: the names the template must spend -/2324/-- `⌊d/3⌋`, by the core's recursion (no division). -/25def third : Nat → Nat26  | 0 => 027  | 1 => 028  | 2 => 029  | n + 3 => third n + 13031/-- `⌊d/4⌋`, by the core's recursion. -/32def quarter : Nat → Nat33  | 0 => 034  | 1 => 035  | 2 => 036  | 3 => 037  | n + 4 => quarter n + 13839theorem third_spec : ∀ d, 3 * third d ≤ d ∧ d < 3 * third d + 340  | 0 => by decide41  | 1 => by decide42  | 2 => by decide43  | n + 3 => by44    have ih := third_spec n45    show 3 * (third n + 1) ≤ n + 3 ∧ n + 3 < 3 * (third n + 1) + 346    rw [Nat.mul_succ]47    exact ⟨Nat.add_le_add_right ih.1 3, Nat.add_lt_add_right ih.2 3⟩4849theorem quarter_spec : ∀ d, 4 * quarter d ≤ d ∧ d < 4 * quarter d + 450  | 0 => by decide51  | 1 => by decide52  | 2 => by decide53  | 3 => by decide54  | n + 4 => by55    have ih := quarter_spec n56    show 4 * (quarter n + 1) ≤ n + 4 ∧ n + 4 < 4 * (quarter n + 1) + 457    rw [Nat.mul_succ]58    exact ⟨Nat.add_le_add_right ih.1 4, Nat.add_lt_add_right ih.2 4⟩5960/-- The number of names of a length between `L` and `j` over `a` letters: `a^L + … + a^j` (`0` when `j < L`). -/61def namesBetween (a L : Nat) : Nat → Nat62  | 0 => 063  | j + 1 => namesBetween a L j + (if L ≤ j + 1 then a ^ (j + 1) else 0)6465theorem namesBetween_zero_of_lt (a L : Nat) : ∀ j, j < L → namesBetween a L j = 066  | 0, _ => rfl67  | j + 1, h => by68    show namesBetween a L j + (if L ≤ j + 1 then a ^ (j + 1) else 0) = 069    rw [namesBetween_zero_of_lt a L j (Nat.lt_of_succ_lt h), ite_eq_right (Nat.not_le_of_gt h)]7071theorem namesBetween_split (a L : Nat) (hL : 1 ≤ L) : ∀ j, L ≤ j → namesBetween a L j = a ^ L + namesBetween a (L + 1) j72  | 0, h => absurd (Nat.le_trans hL h) (Nat.not_le_of_gt Nat.zero_lt_one)73  | j + 1, h => by74    show namesBetween a L j + (if L ≤ j + 1 then a ^ (j + 1) else 0)75        = a ^ L + (namesBetween a (L + 1) j + (if L + 1 ≤ j + 1 then a ^ (j + 1) else 0))76    rw [ite_eq_left h]77    match Nat.lt_or_ge j L with78    | .inl hlt =>79      have e : L = j + 1 := Nat.le_antisymm h (Nat.succ_le_of_lt hlt)80      rw [namesBetween_zero_of_lt a L j hlt, namesBetween_zero_of_lt a (L + 1) j (Nat.lt_succ_of_lt hlt),81        ite_eq_right (fun h' : L + 1 ≤ j + 1 => Nat.lt_irrefl j (Nat.lt_of_lt_of_le hlt (Nat.le_of_succ_le_succ h'))), e]82      exact (Nat.zero_add _).trans (Nat.add_zero _).symm83    | .inr hge =>84      rw [namesBetween_split a L hL j hge, ite_eq_left (Nat.succ_le_succ hge), Nat.add_assoc]8586theorem pow_le_namesBetween (a L : Nat) (hL : 1 ≤ L) (j : Nat) (h : L ≤ j) : a ^ L ≤ namesBetween a L j := by87  rw [namesBetween_split a L hL j h]; exact Nat.le_add_right _ _8889/-- The cost of the `k` shortest names of length at least `L`: `a^L` of them cost `L` each, the rest are longer. -/90def costFrom (a : Nat) : Nat → Nat → Nat → Nat91  | 0, _, _ => 092  | fuel + 1, L, k => if k ≤ a ^ L then k * L else a ^ L * L + costFrom a fuel (L + 1) (k - a ^ L)9394/-- The total length of the `k` shortest distinct names over `a` letters: `a` of one letter, `a²` of two, …95(25:F4's `c(k)`). -/96def nameCost (a k : Nat) : Nat := costFrom a k 1 k9798theorem lt_of_mul_lt_mul_left' {a b c : Nat} (h : c * a < c * b) : a < b :=99  Nat.lt_of_not_ge (fun hge => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le h (Nat.mul_le_mul_left c hge)))100101theorem sub_add_eq' (k x : Nat) : ∀ y, k - (x + y) = k - x - y102  | 0 => rfl103  | y + 1 => by104    show k - (x + y + 1) = k - x - (y + 1)105    rw [Nat.sub_succ, Nat.sub_succ, sub_add_eq' k x y]106107theorem le_sub_add' (k x : Nat) : k ≤ k - x + x :=108  match Nat.lt_or_ge k x with109  | .inl h => by rw [FRC.Nat.sub_eq_zero_of_le (Nat.le_of_lt h), Nat.zero_add]; exact Nat.le_of_lt h110  | .inr h => by rw [FRC.Nat.sub_add_cancel h]; exact Nat.le_refl k111112theorem sumBelow_le_mul (g : Nat → Nat) (c : Nat) (h : ∀ j, g j ≤ c) : ∀ J, sumBelow g J ≤ J * c := fun J =>113  Nat.le_trans (sumBelow_le_sumBelow (fun j _ => h j)) (Nat.le_of_eq (sumBelow_const c J))114115theorem sumBelow_ite_le (c L : Nat) : ∀ J, sumBelow (fun j => if j < L then c else 0) J ≤ L * c116  | 0 => Nat.zero_le _117  | J + 1 => by118    show sumBelow (fun j => if j < L then c else 0) J + (if J < L then c else 0) ≤ L * c119    match Nat.lt_or_ge J L with120    | .inl hlt =>121      rw [ite_eq_left hlt]122      have h1 : sumBelow (fun j => if j < L then c else 0) J ≤ J * c :=123        sumBelow_le_mul _ c (fun j => by split <;> first | exact Nat.le_refl c | exact Nat.zero_le c) J124      have h2 : J * c + c ≤ L * c := by rw [← Nat.succ_mul]; exact Nat.mul_le_mul_right c (Nat.succ_le_of_lt hlt)125      exact Nat.le_trans (Nat.add_le_add_right h1 c) h2126    | .inr hge =>127      rw [ite_eq_right (Nat.not_lt_of_ge hge), Nat.add_zero]; exact sumBelow_ite_le c L J128129/-- The lower bound behind 25:F6 (i): the `k` shortest names of length at least `L` cost at least130`Σ_{j<J} (k − N_L(j))`, `N_L(j)` the number of such names of length at most `j` — summed over the levels `j`, each name131contributes one to every level below its length. -/132theorem costFrom_lower (a : Nat) (ha : 0 < a) :133    ∀ fuel L k J, 1 ≤ L → k ≤ fuel → sumBelow (fun j => k - namesBetween a L j) J ≤ costFrom a fuel L k134  | 0, L, k, J, _, hk => by135    have e : k = 0 := Nat.le_zero.1 hk136    subst e137    have : sumBelow (fun j => 0 - namesBetween a L j) J = sumBelow (fun _ => 0) J :=138      sumBelow_congr (fun j _ => Nat.zero_sub _)139    rw [this, sumBelow_const, Nat.mul_zero]; exact Nat.le_refl 0140  | fuel + 1, L, k, J, hL, hk => by141    show sumBelow (fun j => k - namesBetween a L j) J142        ≤ (if k ≤ a ^ L then k * L else a ^ L * L + costFrom a fuel (L + 1) (k - a ^ L))143    match Nat.lt_or_ge (a ^ L) k with144    | .inr hle =>145      rw [ite_eq_left hle]146      -- each level below L contributes k, each level from L on contributes nothing147      have hpt : ∀ j, k - namesBetween a L j ≤ (if j < L then k else 0) := fun j =>148        match Nat.lt_or_ge j L with149        | .inl hj => by rw [ite_eq_left hj]; exact Nat.sub_le k _150        | .inr hj => by151          rw [ite_eq_right (Nat.not_lt_of_ge hj)]152          exact Nat.le_of_eq (FRC.Nat.sub_eq_zero_of_le (Nat.le_trans hle (pow_le_namesBetween a L hL j hj)))153      exact Nat.le_trans (sumBelow_le_sumBelow (fun j _ => hpt j))154        (Nat.le_trans (sumBelow_ite_le k L J) (Nat.le_of_eq (Nat.mul_comm L k)))155    | .inl hlt =>156      rw [ite_eq_right (Nat.not_le_of_gt hlt)]157      have hk' : k - a ^ L ≤ fuel :=158        Nat.le_of_lt_succ (Nat.lt_of_lt_of_le (Nat.sub_lt (Nat.lt_of_le_of_lt (Nat.zero_le _) hlt) (Nat.pow_pos ha)) hk)159      have ih := costFrom_lower a ha fuel (L + 1) (k - a ^ L) J (Nat.le_succ_of_le hL) hk'160      -- pointwise: k − N_L(j) ≤ (k − a^L) − N_{L+1}(j) + (if j < L then a^L else 0)161      have hpt : ∀ j, k - namesBetween a L j162          ≤ (k - a ^ L - namesBetween a (L + 1) j) + (if j < L then a ^ L else 0) := fun j =>163        match Nat.lt_or_ge j L with164        | .inl hj => by165          rw [ite_eq_left hj, namesBetween_zero_of_lt a L j hj, namesBetween_zero_of_lt a (L + 1) j (Nat.lt_succ_of_lt hj),166            Nat.sub_zero, Nat.sub_zero, FRC.Nat.sub_add_cancel (Nat.le_of_lt hlt)]167          exact Nat.le_refl k168        | .inr hj => by169          rw [ite_eq_right (Nat.not_lt_of_ge hj), Nat.add_zero, namesBetween_split a L hL j hj, sub_add_eq']170          exact Nat.le_refl _171      have hsum := sumBelow_le_sumBelow (R := J) (fun j _ => hpt j)172      rw [sumBelow_add] at hsum173      exact Nat.le_trans hsum (Nat.le_trans (Nat.add_le_add ih (sumBelow_ite_le (a ^ L) L J))174        (Nat.le_of_eq (by rw [Nat.add_comm, Nat.mul_comm])))175176/-- `N(j) = a + … + a^j`, the names of length at most `j`, number at most `2a^j − 2` for `a ≥ 2`. -/177theorem namesBetween_one_le (a : Nat) (ha : 2 ≤ a) : ∀ j, namesBetween a 1 j + 2 ≤ 2 * a ^ j178  | 0 => show 0 + 2 ≤ 2 * 1 from Nat.le_refl 2179  | j + 1 => by180    show namesBetween a 1 j + (if 1 ≤ j + 1 then a ^ (j + 1) else 0) + 2 ≤ 2 * a ^ (j + 1)181    rw [ite_eq_left (Nat.succ_le_succ (Nat.zero_le j))]182    have ih := namesBetween_one_le a ha j183    have h2 : 2 * a ^ j ≤ a ^ (j + 1) := by rw [Nat.pow_succ, Nat.mul_comm (a ^ j) a]; exact Nat.mul_le_mul_right _ ha184    have : namesBetween a 1 j + a ^ (j + 1) + 2 = (namesBetween a 1 j + 2) + a ^ (j + 1) := by185      rw [Nat.add_right_comm]186    rw [this, Nat.two_mul]187    exact Nat.add_le_add (Nat.le_trans ih h2) (Nat.le_refl _)188189/-- `Σ_{j<J} N(j) ≤ 2a^J − 2` for `a ≥ 2`. -/190theorem sumBelow_namesBetween_le (a : Nat) (ha : 2 ≤ a) : ∀ J, sumBelow (namesBetween a 1) J + 2 ≤ 2 * a ^ J191  | 0 => show 0 + 2 ≤ 2 * 1 from Nat.le_refl 2192  | J + 1 => by193    show sumBelow (namesBetween a 1) J + namesBetween a 1 J + 2 ≤ 2 * a ^ (J + 1)194    have ih := sumBelow_namesBetween_le a ha J195    have hN := namesBetween_one_le a ha J196    have h2 : 2 * a ^ J ≤ a ^ (J + 1) := by197      rw [Nat.pow_succ, Nat.mul_comm (a ^ J) a]; exact Nat.mul_le_mul_right _ ha198    have h4 : 2 * a ^ J + 2 * a ^ J ≤ 2 * a ^ (J + 1) := by199      rw [← Nat.two_mul]; exact Nat.mul_le_mul_left 2 h2200    have : sumBelow (namesBetween a 1) J + namesBetween a 1 J + 2201        = (sumBelow (namesBetween a 1) J + 2) + namesBetween a 1 J := by rw [Nat.add_right_comm]202    rw [this]203    exact Nat.le_trans (Nat.add_le_add ih (Nat.le_trans (Nat.le_add_right _ 2) hN)) h4204205/-- 25:F6 (i), 00:Z9 — the name-cost bound: for every `J`, `kJ + 2 ≤ c(k) + 2a^J`: the `k` shortest names cannot all be206short. -/207theorem nameCost_lower (a : Nat) (ha : 2 ≤ a) (k J : Nat) : k * J + 2 ≤ nameCost a k + 2 * a ^ J := by208  have h1 : sumBelow (fun j => k - namesBetween a 1 j) J ≤ nameCost a k :=209    costFrom_lower a (Nat.lt_of_lt_of_le Nat.zero_lt_two ha) k 1 k J (Nat.le_refl 1) (Nat.le_refl k)210  have h2 : sumBelow (fun _ => k) J ≤ sumBelow (fun j => k - namesBetween a 1 j) J + sumBelow (namesBetween a 1) J := by211    rw [← sumBelow_add]; exact sumBelow_le_sumBelow (fun j _ => le_sub_add' k _)212  rw [sumBelow_const, Nat.mul_comm] at h2213  have h3 := sumBelow_namesBetween_le a ha J214  calc k * J + 2 ≤ sumBelow (fun j => k - namesBetween a 1 j) J + sumBelow (namesBetween a 1) J + 2 :=215        Nat.add_le_add_right h2 2216    _ = sumBelow (fun j => k - namesBetween a 1 j) J + (sumBelow (namesBetween a 1) J + 2) := Nat.add_assoc _ _ _217    _ ≤ nameCost a k + 2 * a ^ J := Nat.add_le_add h1 h3218219/-- Every name has at least one letter: `c(k) ≥ k`. -/220theorem le_nameCost (a : Nat) (ha : 0 < a) (k : Nat) : k ≤ nameCost a k := by221  have h := costFrom_lower a ha k 1 k 1 (Nat.le_refl 1) (Nat.le_refl k)222  show k ≤ costFrom a k 1 k223  have e : sumBelow (fun j => k - namesBetween a 1 j) 1 = k := by224    show 0 + (k - 0) = k; rw [Nat.sub_zero, Nat.zero_add]225  rw [e] at h; exact h226227/-- The least total length of the variable names in `δ(u) = ∃ v (Diag(u, v) ∧ θ(v))`: each coordinate of `v` named three228times, each of `u` once, the weight on the shortest names (25:F4). -/229def deltaNames (a k k₁ : Nat) : Nat := 2 * nameCost a k + nameCost a (k + k₁)230231/-- The least number of symbols the coordinates cost in `λ = δ(⌜δ⌝)`: each coordinate of `v` three times and a closed term232of at least one symbol in each place of `u` (25:F4). -/233def lambdaNames (a k k₁ : Nat) : Nat := 3 * nameCost a k + k₁234235/-- The name count leaves an instance open: `λ`'s symbols fit a code of `k` coordinates and `δ`'s a code of `k₁`, a tuple236of `j` coordinates over a structure of `d` digits holding fewer than `d·j` letters. -/237def admits (a d k k₁ : Nat) : Bool :=238  decide (lambdaNames a k k₁ < d * k) && decide (deltaNames a k k₁ < d * k₁)239240theorem admits_lambda {a d k k₁ : Nat} (h : admits a d k k₁ = true) : 3 * nameCost a k + k₁ < d * k :=241  of_decide_eq_true (band_l h)242243theorem admits_delta {a d k k₁ : Nat} (h : admits a d k k₁ = true) : 2 * nameCost a k + nameCost a (k + k₁) < d * k₁ :=244  of_decide_eq_true (band_r h)245246theorem mul3_add_two {x y z : Nat} (h : x + 2 ≤ y + 2 * z) : 3 * x + 6 ≤ 3 * y + 6 * z := by247  have := Nat.mul_le_mul_left 3 h248  rw [Nat.mul_add, Nat.mul_add, ← FRC.Nat.mul_assoc] at this249  exact this250251theorem mul2_add_two {x y z : Nat} (h : x + 2 ≤ y + 2 * z) : 2 * x + 4 ≤ 2 * y + 4 * z := by252  have := Nat.mul_le_mul_left 2 h253  rw [Nat.mul_add, Nat.mul_add, ← FRC.Nat.mul_assoc] at this254  exact this255256theorem add_self_mul (k J : Nat) : (k + k) * J = 2 * (k * J) := by rw [FRC.Nat.add_mul, Nat.two_mul]257258theorem two_add_two_add (x : Nat) : 2 * x + 4 + (2 * x + 2) = 4 * x + 6 := by259  rw [Nat.add_assoc, Nat.add_left_comm 4, ← Nat.add_assoc, ← Nat.two_mul, ← FRC.Nat.mul_assoc]260261theorem add_four_add_two (y z w : Nat) : y + 4 * w + (z + 2 * w) = y + z + 6 * w := by262  rw [Nat.add_assoc, Nat.add_left_comm (4 * w), ← Nat.add_assoc, ← FRC.Nat.add_mul]263264/-- 25:F6 (the bound), 00:Z9 — an admitted instance has `k < 6a^{⌊d/3⌋+1}`: from `3c(k) < dk` and the name-cost bound at265`J = ⌊d/3⌋ + 1`, where `3J ≥ d + 1`. -/266theorem admits_bound {a d k k₁ : Nat} (ha : 2 ≤ a) (h : admits a d k k₁ = true) : k < 6 * a ^ (third d + 1) := by267  have h3 : 3 * nameCost a k < d * k := Nat.lt_of_le_of_lt (Nat.le_add_right _ k₁) (admits_lambda h)268  have hJ : d + 1 ≤ 3 * (third d + 1) := by rw [Nat.mul_succ]; exact (third_spec d).2269  have h4 := mul3_add_two (nameCost_lower a ha k (third d + 1))270  have h5 : d * k + k ≤ 3 * (k * (third d + 1)) := by271    have := Nat.mul_le_mul_left k hJ272    rw [Nat.mul_succ, FRC.Nat.mul_left_comm, Nat.mul_comm k d] at this273    exact this274  have h6 : d * k + (k + 6) < d * k + 6 * a ^ (third d + 1) := by275    rw [← Nat.add_assoc]276    exact Nat.lt_of_le_of_lt (Nat.le_trans (Nat.add_le_add_right h5 6) h4) (Nat.add_lt_add_right h3 _)277  exact Nat.lt_of_le_of_lt (Nat.le_add_right k 6) (Nat.lt_of_add_lt_add_left h6)278279/-- 25:F6 (the digit form), 00:Z9 — an admitted `k` has at most `⌊d/3⌋ + 4` base-`a` digits: `6a^J < a^{J+3}`. -/280theorem admits_digits {a d k k₁ : Nat} (ha : 2 ≤ a) (h : admits a d k k₁ = true) : k < a ^ (third d + 4) := by281  have h1 := admits_bound ha h282  have h2 : 6 * a ^ (third d + 1) < 8 * a ^ (third d + 1) :=283    FRC.Nat.mul_lt_mul_of_lt_of_pos (by decide) (Nat.pow_pos (Nat.lt_of_lt_of_le Nat.zero_lt_two ha))284  have h3 : 8 * a ^ (third d + 1) ≤ a ^ 3 * a ^ (third d + 1) :=285    Nat.mul_le_mul_right _ (Nat.pow_le_pow_left ha 3)286  have e : a ^ 3 * a ^ (third d + 1) = a ^ (third d + 4) := by287    rw [← FRC.Nat.pow_add, Nat.add_comm 3]288  exact Nat.lt_of_lt_of_le h1 (Nat.le_trans (Nat.le_of_lt h2) (e ▸ h3))289290/-- 25:F6 (one scale) — with `k₁ = k` the count `2c(k) + c(2k) < dk` forces `k < 6a^{⌊d/4⌋+1}`. -/291theorem one_scale_bound {a d k : Nat} (ha : 2 ≤ a) (h : admits a d k k = true) : k < 6 * a ^ (quarter d + 1) := by292  have hdel : 2 * nameCost a k + nameCost a (k + k) < d * k := admits_delta h293  have hJ : d + 1 ≤ 4 * (quarter d + 1) := by rw [Nat.mul_succ]; exact (quarter_spec d).2294  have b1 := mul2_add_two (nameCost_lower a ha k (quarter d + 1))295  have b2 := nameCost_lower a ha (k + k) (quarter d + 1)296  rw [add_self_mul] at b2297  have h4 : 4 * (k * (quarter d + 1)) + 6 ≤ 2 * nameCost a k + nameCost a (k + k) + 6 * a ^ (quarter d + 1) := by298    have := Nat.add_le_add b1 b2299    rw [two_add_two_add, add_four_add_two] at this300    exact this301  have h5 : d * k + k ≤ 4 * (k * (quarter d + 1)) := by302    have := Nat.mul_le_mul_left k hJ303    rw [Nat.mul_succ, FRC.Nat.mul_left_comm, Nat.mul_comm k d] at this304    exact this305  have h6 : d * k + (k + 6) < d * k + 6 * a ^ (quarter d + 1) := by306    rw [← Nat.add_assoc]307    exact Nat.lt_of_le_of_lt (Nat.le_trans (Nat.add_le_add_right h5 6) h4) (Nat.add_lt_add_right hdel _)308  exact Nat.lt_of_le_of_lt (Nat.le_add_right k 6) (Nat.lt_of_add_lt_add_left h6)309310/-- 25:F6 (small `d`) — for `d ≤ 4` no instance is admitted: `c(j) ≥ j` gives `k₁ < k` from `λ`'s count and `k < k₁`311from `δ`'s. -/312theorem no_instance_small_d {a d k k₁ : Nat} (ha : 0 < a) (hd : d ≤ 4) : admits a d k k₁ = false := by313  match h : admits a d k k₁ with314  | false => rfl315  | true =>316    exfalso317    have hlam := admits_lambda h318    have hdel := admits_delta h319    have c1 := le_nameCost a ha k320    have c2 := le_nameCost a ha (k + k₁)321    have h1 : 3 * k + k₁ < 4 * k :=322      Nat.lt_of_le_of_lt (Nat.add_le_add_right (Nat.mul_le_mul_left 3 c1) k₁)323        (Nat.lt_of_lt_of_le hlam (Nat.mul_le_mul_right k hd))324    have h2 : 3 * k + k₁ < 4 * k₁ := by325      have : 3 * k + k₁ ≤ 2 * nameCost a k + nameCost a (k + k₁) := by326        have e : 3 * k + k₁ = 2 * k + (k + k₁) := by327          rw [Nat.succ_mul 2 k, Nat.add_assoc]328        rw [e]; exact Nat.add_le_add (Nat.mul_le_mul_left 2 c1) c2329      exact Nat.lt_of_le_of_lt this (Nat.lt_of_lt_of_le hdel (Nat.mul_le_mul_right k₁ hd))330    -- k₁ < k from h1 and k < k₁ from h2331    have hk₁ : k₁ < k := by332      rw [Nat.succ_mul 3 k] at h1333      exact Nat.lt_of_add_lt_add_left h1334    have hk : k < k₁ := by335      rw [Nat.succ_mul 3 k₁, Nat.add_comm (3 * k₁) k₁, Nat.add_comm (3 * k) k₁] at h2336      exact lt_of_mul_lt_mul_left' (Nat.lt_of_add_lt_add_left h2)337    exact Nat.lt_irrefl k (Nat.lt_trans hk hk₁)338339/-- Whether some `k₁` admits `k`: by `λ`'s count `k₁ < dk − 3c(k)`, so the search runs below that bound. -/340def admitsSome (a d k : Nat) : Bool := anyBelow (fun k₁ => admits a d k k₁) (d * k - 3 * nameCost a k)341342theorem admitsSome_of {a d k k₁ : Nat} (h : admits a d k k₁ = true) : admitsSome a d k = true := by343  have hlam := admits_lambda h344  have hlt : k₁ < d * k - 3 * nameCost a k := by345    have h3 : 3 * nameCost a k ≤ d * k := Nat.le_of_lt (Nat.lt_of_le_of_lt (Nat.le_add_right _ k₁) hlam)346    have e := FRC.Nat.sub_add_cancel h3347    rw [← e, Nat.add_comm] at hlam348    exact Nat.lt_of_add_lt_add_right hlam349  exact (anyBelow_true_iff _ _).2 ⟨k₁, hlt, h⟩350351/-- The largest `i < n` with `P i`, or `0` if there is none. -/352def largestBelow (P : Nat → Bool) : Nat → Nat353  | 0 => 0354  | n + 1 => if P n then n else largestBelow P n355356theorem le_largestBelow (P : Nat → Bool) {i : Nat} (hi : P i = true) : ∀ n, i < n → i ≤ largestBelow P n357  | 0, h => absurd h (Nat.not_lt_zero i)358  | n + 1, h => by359    show i ≤ (if P n then n else largestBelow P n)360    match hP : P n with361    | true => rw [ite_eq_left rfl]; exact Nat.le_of_lt_succ h362    | false =>363      rw [ite_eq_right (by decide : ¬ (false = true))]364      have hne : i ≠ n := fun e => Bool.noConfusion (hi.symm.trans (e ▸ hP))365      exact le_largestBelow P hi n (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ h) hne)366367theorem largestBelow_lt (P : Nat → Bool) : ∀ n, 0 < n → largestBelow P n < n368  | 0, h => absurd h (Nat.lt_irrefl 0)369  | n + 1, _ => by370    show (if P n then n else largestBelow P n) < n + 1371    match hP : P n with372    | true => rw [ite_eq_left rfl]; exact Nat.lt_succ_self n373    | false =>374      rw [ite_eq_right (by decide : ¬ (false = true))]375      match n with376      | 0 => exact Nat.zero_lt_one377      | n + 1 => exact Nat.lt_succ_of_lt (largestBelow_lt P (n + 1) (Nat.succ_pos n))378379theorem largestBelow_eq_zero (P : Nat → Bool) : ∀ n, (∀ i, i < n → P i = false) → largestBelow P n = 0380  | 0, _ => rfl381  | n + 1, h => by382    show (if P n then n else largestBelow P n) = 0383    rw [h n (Nat.lt_succ_self n), ite_eq_right (by decide : ¬ (false = true))]384    exact largestBelow_eq_zero P n (fun i hi => h i (Nat.lt_succ_of_lt hi))385386/-- `k*(M)`: the largest `k` some `k₁` admits, searched below the bound `6a^{⌊d/3⌋+1}` (25:F6). -/387def kstar (a d : Nat) : Nat := largestBelow (admitsSome a d) (6 * a ^ (third d + 1))388389/-- `t(M) = d · k*(M)`, the threshold length (25:F6). -/390def threshold (a d : Nat) : Nat := d * kstar a d391392/-- 25:F6, 00:Z9 — the search misses nothing: every admitted `k` is at most `k*`. -/393theorem kstar_max {a d k k₁ : Nat} (ha : 2 ≤ a) (h : admits a d k k₁ = true) : k ≤ kstar a d :=394  le_largestBelow (admitsSome a d) (admitsSome_of h) _ (admits_bound ha h)395396/-- 25:F6 — `k*(M) < 6a^{⌊d/3⌋+1}`, as the row states it. -/397theorem kstar_lt {a d : Nat} (ha : 1 ≤ a) : kstar a d < 6 * a ^ (third d + 1) :=398  largestBelow_lt _ _ (Nat.mul_pos (by decide) (Nat.pow_pos ha))399400/-- 25:F6, 00:Z9 (the digit form) — `k*(M)` has at most `⌊d/3⌋ + 4` base-`a` digits. -/401theorem kstar_digits {a d : Nat} (ha : 2 ≤ a) : kstar a d < a ^ (third d + 4) := by402  have h2 : 6 * a ^ (third d + 1) < 8 * a ^ (third d + 1) :=403    FRC.Nat.mul_lt_mul_of_lt_of_pos (by decide) (Nat.pow_pos (Nat.lt_of_lt_of_le Nat.zero_lt_two ha))404  have h3 : 8 * a ^ (third d + 1) ≤ a ^ 3 * a ^ (third d + 1) :=405    Nat.mul_le_mul_right _ (Nat.pow_le_pow_left ha 3)406  have e : a ^ 3 * a ^ (third d + 1) = a ^ (third d + 4) := by rw [← FRC.Nat.pow_add, Nat.add_comm 3]407  exact Nat.lt_of_lt_of_le (kstar_lt (Nat.le_of_lt ha)) (Nat.le_trans (Nat.le_of_lt h2) (e ▸ h3))408409/-- 25:F6 (ii), 00:Z9 — no instance codes `λ` at length `n ≥ t(M)`: with `k + 1` coordinates in `v` admitted and the410coding injective (`a^n ≤ m^(k+1)`, 25:F4) over a structure of `d` digits, `n < d(k + 1) ≤ d·k* = t(M)`. -/411theorem no_instance_at_threshold {a d k k₁ m n : Nat} (ha : 2 ≤ a) (h : admits a d (k + 1) k₁ = true)412    (hm : m < a ^ d) (hc : a ^ n ≤ m ^ (k + 1)) : n < threshold a d :=413  Nat.lt_of_lt_of_le (digit_bound (Nat.lt_of_lt_of_le Nat.zero_lt_two ha) hm hc)414    (Nat.mul_le_mul_left d (kstar_max ha h))415416/-- For `d ≤ 4` the threshold is `0`: nothing is admitted. -/417theorem threshold_small_d {a d : Nat} (ha : 0 < a) (hd : d ≤ 4) : threshold a d = 0 := by418  show d * largestBelow (admitsSome a d) _ = 0419  rw [largestBelow_eq_zero (admitsSome a d) _ (fun k _ => by420    show anyBelow (fun k₁ => admits a d k k₁) _ = false421    rw [anyBelow_congr (fun k₁ _ => no_instance_small_d ha hd)]; exact anyBelow_false _), Nat.mul_zero]422423theorem coef_pow_le {a : Nat} (ha : 2 ≤ a) (c e J : Nat) (hc : c ≤ 2 ^ e) : c * a ^ J ≤ a ^ (e + J) := by424  rw [FRC.Nat.pow_add]; exact Nat.mul_le_mul_right _ (Nat.le_trans hc (Nat.pow_le_pow_left ha e))425426theorem coef_pow_le6 {a : Nat} (ha : 6 ≤ a) (c e J : Nat) (hc : c ≤ 6 ^ e) : c * a ^ J ≤ a ^ (e + J) := by427  rw [FRC.Nat.pow_add]; exact Nat.mul_le_mul_right _ (Nat.le_trans hc (Nat.pow_le_pow_left ha e))428429theorem rearr4 (x y z : Nat) : 4 * x * (y * z) = x * y * (4 * z) := by430  rw [FRC.Nat.mul_assoc, FRC.Nat.mul_left_comm, FRC.Nat.mul_left_comm 4 y, ← FRC.Nat.mul_assoc]431432/-- The step `d → d + 3` of the bound `6d·a^{⌊d/3⌋+1} ≤ a^{d−1}`: the left side gains at most the factor `4a`, the right433side `a³`. -/434theorem six_d_pow_step {a : Nat} (ha : 2 ≤ a) (d : Nat) (hd : 1 ≤ d)435    (h : 6 * d * a ^ (third d + 1) ≤ a ^ (d - 1)) : 6 * (d + 3) * a ^ (third (d + 3) + 1) ≤ a ^ (d + 2) := by436  have e3 : third (d + 3) + 1 = third d + 1 + 1 := rfl437  rw [e3]438  have h1 : 6 * (d + 3) ≤ 4 * (6 * d) := by439    have e1 : 6 * (d + 3) = 6 * d + 18 := by rw [Nat.mul_add]440    have e2 : 4 * (6 * d) = 6 * d + 18 * d := by rw [← FRC.Nat.mul_assoc, ← FRC.Nat.add_mul]441    rw [e1, e2]442    exact Nat.add_le_add_left (Nat.le_mul_of_pos_right 18 hd) _443  have h4 : 4 ≤ a ^ 2 := Nat.pow_le_pow_left ha 2444  have hpow : a ^ (third d + 1 + 1) = a ^ (third d + 1) * a := rfl445  have hd2 : a ^ (d + 2) = a ^ (d - 1) * (a ^ 2 * a) := by446    have e : d - 1 + 3 = d + 2 := congrArg (· + 2) (FRC.Nat.sub_add_cancel hd)447    rw [← e, FRC.Nat.pow_add]; rfl448  rw [hpow, hd2]449  calc 6 * (d + 3) * (a ^ (third d + 1) * a)450      ≤ 4 * (6 * d) * (a ^ (third d + 1) * a) := Nat.mul_le_mul_right _ h1451    _ = 6 * d * a ^ (third d + 1) * (4 * a) := rearr4 _ _ _452    _ ≤ a ^ (d - 1) * (a ^ 2 * a) := Nat.mul_le_mul h (Nat.mul_le_mul_right a h4)453454/-- `6d·a^{⌊d/3⌋+1} ≤ a^{d−1}` for every `d ≥ 13` and `a ≥ 2`: the cases `13`, `14`, `15` and the step. -/455theorem six_d_pow_le_large {a : Nat} (ha : 2 ≤ a) :456    ∀ n, 6 * (13 + n) * a ^ (third (13 + n) + 1) ≤ a ^ (12 + n) := by457  have base0 : 6 * (13 + 0) * a ^ (third (13 + 0) + 1) ≤ a ^ (12 + 0) := coef_pow_le ha 78 7 5 (by decide)458  have base1 : 6 * (13 + 1) * a ^ (third (13 + 1) + 1) ≤ a ^ (12 + 1) := coef_pow_le ha 84 8 5 (by decide)459  have base2 : 6 * (13 + 2) * a ^ (third (13 + 2) + 1) ≤ a ^ (12 + 2) := coef_pow_le ha 90 8 6 (by decide)460  have step : ∀ n, 6 * (13 + n) * a ^ (third (13 + n) + 1) ≤ a ^ (12 + n)461      → 6 * (13 + (n + 3)) * a ^ (third (13 + (n + 3)) + 1) ≤ a ^ (12 + (n + 3)) := fun n h => by462    have e1 : 13 + n - 1 = 12 + n := by463      rw [Nat.add_comm 13 n, Nat.add_comm 12 n]; exact FRC.Nat.add_sub_cancel (n + 12) 1464    have h' : 6 * (13 + n) * a ^ (third (13 + n) + 1) ≤ a ^ (13 + n - 1) := by rw [e1]; exact h465    have := six_d_pow_step ha (13 + n) (Nat.le_add_right_of_le (by decide)) h'466    have e2 : 13 + (n + 3) = 13 + n + 3 := (Nat.add_assoc 13 n 3).symm467    have e3 : 12 + (n + 3) = 13 + n + 2 := by468      rw [Nat.add_comm n 3, ← Nat.add_assoc, Nat.add_assoc 13 n 2, Nat.add_comm n 2, ← Nat.add_assoc]469    rw [e2, e3]; exact this470  have all : ∀ n, (6 * (13 + n) * a ^ (third (13 + n) + 1) ≤ a ^ (12 + n)) ∧471      (6 * (13 + (n + 1)) * a ^ (third (13 + (n + 1)) + 1) ≤ a ^ (12 + (n + 1))) ∧472      (6 * (13 + (n + 2)) * a ^ (third (13 + (n + 2)) + 1) ≤ a ^ (12 + (n + 2))) := fun n => by473    induction n with474    | zero => exact ⟨base0, base1, base2⟩475    | succ n ih => exact ⟨ih.2.1, ih.2.2, step n ih.1⟩476  exact fun n => (all n).1477478/-- `6d·a^{⌊d/3⌋+1} ≤ a^{d−1}` for `5 ≤ d ≤ 12` and `a ≥ 6`, each `d` by one bound `6d ≤ 6^{d−1−J}`. -/479theorem six_d_pow_le_mid {a : Nat} (ha : 6 ≤ a) (d : Nat) (h5 : 5 ≤ d) (h12 : d ≤ 12) :480    6 * d * a ^ (third d + 1) ≤ a ^ (d - 1) :=481  match d, h5, h12 with482  | 5, _, _ => coef_pow_le6 ha 30 2 2 (by decide)483  | 6, _, _ => coef_pow_le6 ha 36 2 3 (by decide)484  | 7, _, _ => coef_pow_le6 ha 42 3 3 (by decide)485  | 8, _, _ => coef_pow_le6 ha 48 4 3 (by decide)486  | 9, _, _ => coef_pow_le6 ha 54 4 4 (by decide)487  | 10, _, _ => coef_pow_le6 ha 60 5 4 (by decide)488  | 11, _, _ => coef_pow_le6 ha 66 6 4 (by decide)489  | 12, _, _ => coef_pow_le6 ha 72 6 5 (by decide)490  | 0, h, _ => absurd h (by decide)491  | 1, h, _ => absurd h (by decide)492  | 2, h, _ => absurd h (by decide)493  | 3, h, _ => absurd h (by decide)494  | 4, h, _ => absurd h (by decide)495  | n + 13, _, h => absurd h (Nat.not_le_of_gt (Nat.lt_of_lt_of_le (by decide) (Nat.le_add_left 13 n)))496497/-- The pairs `(a, d)` with `a ≤ 5` and `5 ≤ d ≤ 12`: either the bound `6d·a^{⌊d/3⌋+1} ≤ a^{d−1}` holds or the kernel498computes `k*` and finds `t < a^{d−1}` — the fifteen pairs of the row's check D5, decided here. -/499theorem threshold_small_pairs : ∀ a, a < 6 → ∀ d, d < 13 → 2 ≤ a → 5 ≤ d →500    (6 * d * a ^ (third d + 1) ≤ a ^ (d - 1) ∨ threshold a d < a ^ (d - 1)) := by501  decide +kernel502503/-- 25:F6 (iii), 25:G7, 00:Z9 — `t(M) < m` in every structure: `m` has `d` base-`a` digits (`a^{d−1} ≤ m`), and the threshold504`d·k*` has fewer: `k* < 6a^{⌊d/3⌋+1}` and `6d·a^{⌊d/3⌋+1} ≤ a^{d−1}` from `d = 13` on and for `a ≥ 6`, the small pairs505computed, nothing admitted at `d ≤ 4`. -/506theorem threshold_lt {a d m : Nat} (ha : 2 ≤ a) (hm : a ^ (d - 1) ≤ m) : threshold a d < m := by507  have ha1 : 0 < a := Nat.lt_of_lt_of_le Nat.zero_lt_two ha508  have hpos : 0 < m := Nat.lt_of_lt_of_le (Nat.pow_pos ha1) hm509  have viaG : 0 < d → 6 * d * a ^ (third d + 1) ≤ a ^ (d - 1) → threshold a d < m := fun hd hG => by510    show d * kstar a d < m511    have h1 : d * kstar a d < d * (6 * a ^ (third d + 1)) := Nat.mul_lt_mul_of_pos_left (kstar_lt ha1) hd512    have e : d * (6 * a ^ (third d + 1)) = 6 * d * a ^ (third d + 1) := by513      rw [FRC.Nat.mul_left_comm, ← FRC.Nat.mul_assoc]514    exact Nat.lt_of_lt_of_le h1 (Nat.le_trans (e ▸ hG) hm)515  match Nat.lt_or_ge d 5 with516  | .inl hd4 => rw [threshold_small_d ha1 (Nat.le_of_lt_succ hd4)]; exact hpos517  | .inr hd5 =>518    have hd : 0 < d := Nat.lt_of_lt_of_le (by decide) hd5519    match Nat.lt_or_ge d 13 with520    | .inr hd13 =>521      have hG := six_d_pow_le_large ha (d - 13)522      have e1 : 13 + (d - 13) = d := FRC.Nat.add_sub_of_le hd13523      have e2 : 12 + (d - 13) = d - 1 := by524        have h := congrArg (· - 1) e1525        have e : 13 + (d - 13) - 1 = 12 + (d - 13) := by526          rw [show 13 + (d - 13) = 12 + (d - 13) + 1 from (Nat.add_right_comm 12 (d - 13) 1).symm]527          exact FRC.Nat.add_sub_cancel _ 1528        rw [← e]; exact h529      rw [e1, e2] at hG530      exact viaG hd hG531    | .inl hd13 =>532      match Nat.lt_or_ge a 6 with533      | .inr ha6 => exact viaG hd (six_d_pow_le_mid ha6 d hd5 (Nat.le_of_lt_succ hd13))534      | .inl ha6 =>535        match threshold_small_pairs a ha6 d hd13 ha hd5 with536        | .inl hG => exact viaG hd hG537        | .inr hlt => exact Nat.lt_of_lt_of_le hlt hm538539/-- 25:F6 (iii), 00:Z9, the digit form — the threshold has fewer base-`a` digits than `m`: `t(M) < a^{d−1}`. -/540theorem threshold_digits {a d : Nat} (ha : 2 ≤ a) : threshold a d < a ^ (d - 1) :=541  threshold_lt ha (Nat.le_refl _)542543end FRC.Diagonal544