Theme/Ladder.lean — FrcCore

1import FrcCore.Frame2import FrcCore.Series34/-!5# FrcCore.Theme.Ladder — the horizon theme: the ladder of the four roles, the ascent and the descent (26-pnp, 16 October 2026)67The computational face of the horizon clause (master Z2–Z4, B6), on a frame `(τ; 0, 1, g)` of a prime shell with the8drive `g` of order `n = p − 1`. The index cycle `C_n` is carried to the units by the ascent `m ↦ g^m`; the descent reads9the index back. On every shell, with no hypothesis beyond the frame:1011* the power map acts on the index as multiplication by `k` — `(g^m)^k = g^{km mod n}` — and its iterates as12  multiplication by `k^r` (`power_index`, `phase_index`); the ascent is one multiplication per counted step13  (`ascent_step`); a tower exponent is read modulo `n`, so iterated exponentiation opens no fifth role14  (`tower_reduces`, the drive's `pow_mod`);15* multiplication by a unit permutes the units (`mul_perm`), the clause behind the Gauss-sum telescoping;16* every index `m` has a recentring chart, a translation of the cycle that carries it to one step from the origin17  (`recentre`, `recentre_inj`);18* the power map `x ↦ x^k` is a bijection of the units when `k` is invertible modulo `n`, inverted by `x ↦ x^a` with19  `ak ≡ 1` (`power_bijective_of_unit`); when `d` divides `k` and `n`, its image is the cycle of `g^d`, of exactly20  `n/d` elements (`power_image`); the gcd enters as a Bezout witness, never by the prelude's `Nat.gcd` (propext);21* square-and-multiply computes `b^e` with at most `2·bits e` multiplications (`sqmul_spec`, `sqmul_count`,22  `bits_le_of_lt_pow`);23* the baby-step–giant-step search, with `m² ≥ n` baby steps `1, g, …, g^{m−1}` (one multiplication each,24  `baby_step`) and at most `m` giant steps (one multiplication each, `giant_count`), recovers an index `y` with25  `g^y = g^x` from `g^x` (`bsgs_spec`).2627The bit length and the halving are the file's own structural recursions (`half`, `par`, `bits`), since the prelude's28`Nat.log2` and `Nat.div` lemmas carry `propext`. No axioms.29-/3031namespace FRC.Ladder3233open FRC.Shell FRC.Shell.Frame3435variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}3637/-! ## The index dynamics of the power map (26:G2, G3) -/3839/-- 26:G2, 26:G3 — the power map on the index: `(g^m)^k = g^{km mod n}`, multiplication by `k` on the index cycle. -/40theorem power_index (F : Frame p κ g) (m k : Nat) : (g ^ m) ^ k = g ^ ((k * m) % (p - 1)) := by41  rw [← pow_mul, Nat.mul_comm m k, F.pow_mod]4243/-- `r` iterates of a map. -/44def iter {α : Type} (f : α → α) : Nat → α → α45  | 0, x => x46  | r + 1, x => iter f r (f x)4748/-- 26:G3 — the iterated power map on the index: `P_k^r(g^m) = g^{k^r m mod n}`. -/49theorem phase_index (F : Frame p κ g) (k : Nat) : ∀ (r m : Nat),50    iter (fun x : Shell p => x ^ k) r (g ^ m) = g ^ ((k ^ r * m) % (p - 1))51  | 0, m => by52    show g ^ m = g ^ ((1 * m) % (p - 1))53    rw [Nat.one_mul, ← F.pow_mod]54  | r + 1, m => by55    show iter (fun x : Shell p => x ^ k) r ((g ^ m) ^ k) = g ^ ((k ^ (r + 1) * m) % (p - 1))56    rw [power_index F, phase_index F k r, FRC.Nat.mul_mod_mod _ _ _ F.n_pos, Nat.pow_succ,57      FRC.Nat.mul_assoc, Nat.mul_comm k m, ← FRC.Nat.mul_assoc]5859/-- 26:G3, 26:G4 — the ascent is counting along the orbit: `g^{j+1} = g^j · g`, one multiplication per step. -/60theorem ascent_step (j : Nat) : g ^ (j + 1) = g ^ j * g := pow_succ g j6162/-- 26:G2 — a tower exponent is read modulo `n`: `g^{(g^j)} = g^{(g^j) mod n}`; tetration is exponentiation of a63reduced index, and the two cyclic structures host every iterate. -/64theorem tower_reduces (F : Frame p κ g) (j : Nat) : g ^ (g ^ j).val = g ^ ((g ^ j).val % (p - 1)) :=65  F.pow_mod _6667/-! ## Multiplication by a unit permutes the units (26:B5) -/6869/-- 26:B5 — multiplication by a unit `c` is injective on the shell and reaches every residue. -/70theorem mul_perm (F : Frame p κ g) {c : Shell p} (hc : c ≠ 0) :71    (∀ {x y : Shell p}, c * x = c * y → x = y) ∧ ∀ y : Shell p, ∃ x, c * x = y := by72  refine ⟨fun h => F.mul_left_cancel hc h, fun y => ?_⟩73  obtain ⟨u, hu⟩ := F.exists_inv hc74  exact ⟨u * y, by rw [← mul_assoc, hu, one_mul]⟩7576/-! ## The recentring chart (26:E8) -/7778/-- The translation of the index cycle that carries the index `m` to `1`. -/79def recentre (n m j : Nat) : Nat := (j + (n - m) + 1) % n8081/-- 26:E8 — the recentred witness sits one step from the origin: `g^{recentre m} = g = g^0 · g`. -/82theorem recentre_witness (F : Frame p κ g) {m : Nat} (hm : m < p - 1) :83    g ^ recentre (p - 1) m m = g ∧ g = g ^ 0 * g := by84  refine ⟨?_, by rw [pow_zero, one_mul]⟩85  unfold recentre86  rw [← F.pow_mod, FRC.Nat.add_sub_of_le (Nat.le_of_lt hm), pow_succ, F.pow_n, one_mul]8788/-- 26:E8 — the recentring is a chart: a bijection of the index cycle (injective on the `n` indices). -/89theorem recentre_inj (F : Frame p κ g) (m : Nat) {i j : Nat} (hi : i < p - 1) (hj : j < p - 1)90    (h : recentre (p - 1) m i = recentre (p - 1) m j) : i = j := by91  unfold recentre at h92  rw [Nat.add_assoc, Nat.add_assoc] at h93  have e : g ^ (p - 1 - m + 1) * g ^ i = g ^ (p - 1 - m + 1) * g ^ j := by94    rw [mul_comm, mul_comm _ (g ^ j), ← pow_add, ← pow_add, F.pow_mod (i + _), F.pow_mod (j + _), h]95  exact F.pow_inj hi hj (F.mul_left_cancel (F.pow_ne_zero _) e)9697/-- 26:E8 — the recentring reaches every index `j < n` (from `i = (j + m + n − 1) % n`): with `recentre_inj`, a98bijection of the index cycle. -/99theorem recentre_surj (F : Frame p κ g) {m : Nat} (hm : m < p - 1) {j : Nat} (hj : j < p - 1) :100    ∃ i, i < p - 1 ∧ recentre (p - 1) m i = j := by101  have hn := F.n_pos102  refine ⟨(j + m + (p - 1 - 1)) % (p - 1), Nat.mod_lt _ hn, ?_⟩103  unfold recentre104  rw [Nat.add_assoc, FRC.Nat.mod_add_mod _ _ _ hn, ← Nat.add_assoc]105  have e : j + m + (p - 1 - 1) + (p - 1 - m) + 1 = (p - 1) * 2 + j := by106    have h1 : m + (p - 1 - m) = p - 1 := FRC.Nat.add_sub_of_le (Nat.le_of_lt hm)107    have h2 : (p - 1 - 1) + 1 = p - 1 := FRC.Nat.sub_add_cancel hn108    rw [Nat.add_assoc (j + m + (p - 1 - 1)), Nat.add_assoc (j + m), Nat.add_assoc j,109      Nat.add_left_comm (p - 1 - 1), ← Nat.add_assoc m, h1, h2, ← Nat.mul_two, Nat.add_comm]110  rw [e, FRC.Nat.add_mul_mod_self_left _ _ _ hn, FRC.Nat.mod_eq_of_lt hj]111112/-! ## The power map: bijective or compressive (26:G5) -/113114/-- 26:G5 — when `ak ≡ 1 (mod n)` the power map `x ↦ x^k` is a bijection of the units, inverted by `x ↦ x^a`. -/115theorem power_bijective_of_unit (F : Frame p κ g) {a k : Nat} (hak : (a * k) % (p - 1) = 1) (m : Nat) :116    ((g ^ m) ^ k) ^ a = g ^ m ∧ ((g ^ m) ^ a) ^ k = g ^ m := by117  have key : ∀ u v : Nat, (u * v) % (p - 1) = 1 → ((g ^ m) ^ u) ^ v = g ^ m := fun u v huv => by118    rw [← pow_mul, ← pow_mul, F.pow_mod, ← FRC.Nat.mul_mod_mod _ _ _ F.n_pos, huv, Nat.mul_one, ← F.pow_mod]119  exact ⟨key k a (by rw [Nat.mul_comm]; exact hak), key a k hak⟩120121/-- 26:G5 — when `d ∣ k`, `n = d·e` and `ak = bn + d` (the gcd as a Bezout witness), the image of the power map122`x ↦ x^k` on the units is the cycle of `g^d`: every value is a power of `g^d`, every power of `g^d` is a value, and123the powers `(g^d)^i`, `i < e`, are distinct — the image has exactly `e = n/d` elements. -/124theorem power_image (F : Frame p κ g) {d e c a b k : Nat} (hn : p - 1 = d * e) (hk : k = d * c)125    (hbez : a * k = b * (p - 1) + d) :126    (∀ m : Nat, (g ^ m) ^ k = (g ^ d) ^ (m * c)) ∧127    (∀ i : Nat, ((g ^ a) ^ i) ^ k = (g ^ d) ^ i) ∧128    (∀ i j : Nat, i < e → j < e → (g ^ d) ^ i = (g ^ d) ^ j → i = j) := by129  have hd : 0 < d := by130    match d, hn with131    | 0, hn =>132      have h0 : 0 < 0 * e := hn ▸ F.n_pos133      rw [Nat.zero_mul] at h0134      exact absurd h0 (Nat.lt_irrefl 0)135    | d + 1, _ => exact Nat.zero_lt_succ d136  refine ⟨fun m => ?_, fun i => ?_, fun i j hi hj h => ?_⟩137  · rw [← pow_mul, ← pow_mul, hk, Nat.mul_comm d c, ← FRC.Nat.mul_assoc, Nat.mul_comm (m * c) d]138  · rw [← pow_mul, ← pow_mul, ← pow_mul, FRC.Nat.mul_left_comm, hbez, Nat.left_distrib, pow_add,139      ← FRC.Nat.mul_assoc, Nat.mul_comm (i * b), pow_mul, F.pow_n, one_pow, one_mul, Nat.mul_comm i d]140  · rw [← pow_mul, ← pow_mul] at h141    have hi' : d * i < p - 1 := by rw [hn]; exact Nat.mul_lt_mul_of_pos_left hi hd142    have hj' : d * j < p - 1 := by rw [hn]; exact Nat.mul_lt_mul_of_pos_left hj hd143    exact Nat.eq_of_mul_eq_mul_left hd (F.pow_inj hi' hj' h)144145146/-- 26:G5 — the compressive image has at most `e = n/d` elements: every value of `x ↦ x^k` is `(g^d)^i` with `i < e`147(with `power_image`'s distinctness of those powers, exactly `e`). -/148theorem power_image_index (F : Frame p κ g) {d e c k : Nat} (hn : p - 1 = d * e) (hk : k = d * c) (m : Nat) :149    ∃ i, i < e ∧ (g ^ m) ^ k = (g ^ d) ^ i := by150  have he : 0 < e := by151    match e, hn with152    | 0, hn => exact absurd (hn ▸ F.n_pos) (by rw [Nat.mul_zero]; exact Nat.lt_irrefl 0)153    | e + 1, _ => exact Nat.zero_lt_succ e154  have hde : (g ^ d) ^ e = 1 := by rw [← pow_mul, ← hn, F.pow_n]155  have h1 : (g ^ m) ^ k = (g ^ d) ^ (m * c) := by156    rw [← pow_mul, ← pow_mul, hk, Nat.mul_comm d c, ← FRC.Nat.mul_assoc, Nat.mul_comm (m * c) d]157  refine ⟨(m * c) % e, Nat.mod_lt _ he, ?_⟩158  rw [h1]159  match FRC.Nat.mod_spec e he (m * c) with160  | ⟨q, hq⟩ =>161    calc (g ^ d) ^ (m * c) = (g ^ d) ^ (e * q + (m * c) % e) := by rw [← hq]162      _ = ((g ^ d) ^ e) ^ q * (g ^ d) ^ ((m * c) % e) := by rw [pow_add, pow_mul]163      _ = (g ^ d) ^ ((m * c) % e) := by rw [hde, one_pow, one_mul]164165/-- 26:G5 — the only-if: when `d = gcd(k, n) > 1` the image has fewer than `n` elements (`e < d·e = n`), so the power map166is no bijection of the units. -/167theorem compressive_of_gcd (F : Frame p κ g) {d e : Nat} (hn : p - 1 = d * e) (hd : 1 < d) : e < p - 1 := by168  have he : 0 < e := by169    match e, hn with170    | 0, hn => exact absurd (hn ▸ F.n_pos) (by rw [Nat.mul_zero]; exact Nat.lt_irrefl 0)171    | e + 1, _ => exact Nat.zero_lt_succ e172  rw [hn]173  calc e = 1 * e := (Nat.one_mul e).symm174    _ < d * e := Nat.mul_lt_mul_of_pos_right hd he175176/-! ## The bit length (the file's own recursion) -/177178/-- The half of a natural number, by structural recursion. -/179def half : Nat → Nat180  | 0 => 0181  | 1 => 0182  | n + 2 => half n + 1183184/-- The parity bit of a natural number. -/185def par : Nat → Nat186  | 0 => 0187  | 1 => 1188  | n + 2 => par n189190theorem half_par : ∀ n : Nat, n = 2 * half n + par n191  | 0 => rfl192  | 1 => rfl193  | n + 2 => by194    show n + 2 = 2 * (half n + 1) + par n195    rw [Nat.mul_succ, Nat.add_right_comm, ← half_par n]196197theorem par_lt_two : ∀ n : Nat, par n < 2198  | 0 => Nat.zero_lt_succ 1199  | 1 => Nat.lt_succ_self 1200  | n + 2 => par_lt_two n201202theorem half_lt : ∀ {n : Nat}, 0 < n → half n < n203  | 0, h => absurd h (Nat.lt_irrefl 0)204  | 1, _ => Nat.zero_lt_succ 0205  | n + 2, _ => by206    show half n + 1 < n + 2207    exact Nat.succ_le_succ (Nat.succ_le_succ (half_le n))208where209  half_le : ∀ n : Nat, half n ≤ n210    | 0 => Nat.le_refl 0211    | 1 => Nat.zero_le 1212    | n + 2 => Nat.succ_le_succ (Nat.le_trans (half_le n) (Nat.le_succ n))213214/-- `a·b < a·c` gives `b < c` (the prelude's lemma carries `propext`). -/215theorem lt_of_mul_lt_mul_left' {a b c : Nat} (h : a * b < a * c) : b < c :=216  match Nat.lt_or_ge b c with217  | .inl hlt => hlt218  | .inr hge => absurd h (Nat.not_lt_of_le (Nat.mul_le_mul_left a hge))219220/-- The bit length by fuel: `bitsAux fuel e` is the length of `e` written in binary when `e ≤ fuel`. -/221def bitsAux : Nat → Nat → Nat222  | 0, _ => 0223  | fuel + 1, e => if e = 0 then 0 else bitsAux fuel (half e) + 1224225/-- The bit length of `e` (`0` for `e = 0`). -/226def bits (e : Nat) : Nat := bitsAux e e227228theorem bitsAux_eq : ∀ (f₁ f₂ e : Nat), e ≤ f₁ → e ≤ f₂ → bitsAux f₁ e = bitsAux f₂ e229  | 0, f₂, e, h₁, _ => by230    have he : e = 0 := Nat.le_zero.1 h₁231    subst he232    match f₂ with233    | 0 => rfl234    | f₂ + 1 => rfl235  | f₁ + 1, 0, e, _, h₂ => by236    have he : e = 0 := Nat.le_zero.1 h₂237    subst he; rfl238  | f₁ + 1, f₂ + 1, e, h₁, h₂ => by239    show (if e = 0 then 0 else bitsAux f₁ (half e) + 1) = (if e = 0 then 0 else bitsAux f₂ (half e) + 1)240    match Nat.decEq e 0 with241    | isTrue he => rw [ite_eq_left he, ite_eq_left he]242    | isFalse he =>243      rw [ite_eq_right he, ite_eq_right he]244      have hl := half_lt (Nat.pos_of_ne_zero he)245      rw [bitsAux_eq f₁ f₂ (half e) (Nat.le_of_lt_succ (Nat.lt_of_lt_of_le hl h₁))246        (Nat.le_of_lt_succ (Nat.lt_of_lt_of_le hl h₂))]247248/-- 26:F2 — a number below `2^l` has at most `l` bits. -/249theorem bitsAux_le_of_lt_pow : ∀ (l fuel e : Nat), e ≤ fuel → e < 2 ^ l → bitsAux fuel e ≤ l250  | l, 0, e, _, _ => Nat.zero_le l251  | 0, fuel + 1, e, _, he => by252    match e, he with253    | 0, _ => exact Nat.le_refl 0254    | e + 1, he => exact absurd he (Nat.not_lt_of_le (Nat.succ_le_succ (Nat.zero_le e)))255  | l + 1, fuel + 1, e, hf, he => by256    show (if e = 0 then 0 else bitsAux fuel (half e) + 1) ≤ l + 1257    match Nat.decEq e 0 with258    | isTrue h0 => rw [ite_eq_left h0]; exact Nat.zero_le _259    | isFalse h0 =>260      rw [ite_eq_right h0]261      apply Nat.succ_le_succ262      have hl := half_lt (Nat.pos_of_ne_zero h0)263      apply bitsAux_le_of_lt_pow l fuel (half e) (Nat.le_of_lt_succ (Nat.lt_of_lt_of_le hl hf))264      -- `2 · half e ≤ e < 2^(l+1) = 2 · 2^l`265      have h2 : 2 * half e < 2 * 2 ^ l := by266        have e2 : 2 * 2 ^ l = 2 ^ (l + 1) := by rw [Nat.pow_succ, Nat.mul_comm]267        rw [e2]268        refine Nat.lt_of_le_of_lt ?_ he269        conv => rhs; rw [half_par e]270        exact Nat.le_add_right _ _271      exact lt_of_mul_lt_mul_left' h2272273theorem bits_le_of_lt_pow {l e : Nat} (he : e < 2 ^ l) : bits e ≤ l :=274  bitsAux_le_of_lt_pow l e e (Nat.le_refl e) he275276/-- 26:E10 — `e < 2^(bits e)`: the upper half of the bit-length bracket. -/277theorem lt_pow_bits : ∀ (fuel e : Nat), e ≤ fuel → e < 2 ^ bitsAux fuel e278  | 0, e, h => by279    have he : e = 0 := Nat.le_zero.1 h280    subst he; exact Nat.zero_lt_one281  | fuel + 1, e, h => by282    show e < 2 ^ (if e = 0 then 0 else bitsAux fuel (half e) + 1)283    match Nat.decEq e 0 with284    | isTrue h0 => rw [ite_eq_left h0, h0]; exact Nat.zero_lt_one285    | isFalse h0 =>286      rw [ite_eq_right h0]287      have hl := half_lt (Nat.pos_of_ne_zero h0)288      have ih := lt_pow_bits fuel (half e) (Nat.le_of_lt_succ (Nat.lt_of_lt_of_le hl h))289      have hp := par_lt_two e290      calc e = 2 * half e + par e := half_par e291        _ < 2 * half e + 2 := Nat.add_lt_add_left hp _292        _ = 2 * (half e + 1) := by rw [Nat.mul_succ]293        _ ≤ 2 * 2 ^ bitsAux fuel (half e) := Nat.mul_le_mul_left 2 ih294        _ = 2 ^ (bitsAux fuel (half e) + 1) := by rw [Nat.pow_succ, Nat.mul_comm]295296/-- 26:E10 — `2^(bits e − 1) ≤ e` for `e > 0`: the lower half of the bit-length bracket. -/297theorem pow_bits_pred_le : ∀ (fuel e : Nat), e ≤ fuel → 0 < e → 2 ^ (bitsAux fuel e - 1) ≤ e298  | 0, e, h, he => absurd (Nat.lt_of_lt_of_le he h) (Nat.lt_irrefl 0)299  | fuel + 1, e, h, he => by300    show 2 ^ ((if e = 0 then 0 else bitsAux fuel (half e) + 1) - 1) ≤ e301    have h0 : e ≠ 0 := Nat.ne_of_gt he302    rw [ite_eq_right h0, Nat.add_sub_cancel]303    match Nat.decEq (half e) 0 with304    | isTrue hh =>305      have hb : bitsAux fuel 0 = 0 := by cases fuel <;> rfl306      rw [hh, hb]; exact he307    | isFalse hh =>308      have hl := half_lt he309      have ih := pow_bits_pred_le fuel (half e) (Nat.le_of_lt_succ (Nat.lt_of_lt_of_le hl h)) (Nat.pos_of_ne_zero hh)310      have hb1 : 1 ≤ bitsAux fuel (half e) := by311        match fuel, (Nat.le_of_lt_succ (Nat.lt_of_lt_of_le hl h) : half e ≤ fuel) with312        | 0, hf => exact absurd (Nat.le_zero.1 hf) hh313        | f + 1, _ =>314          show 1 ≤ (if half e = 0 then 0 else bitsAux f (half (half e)) + 1)315          rw [ite_eq_right hh]; exact Nat.succ_le_succ (Nat.zero_le _)316      have key : ∀ b : Nat, 1 ≤ b → 2 ^ b = 2 * 2 ^ (b - 1) := fun b hb => by317        match b, hb with318        | b' + 1, _ => rw [Nat.add_sub_cancel, Nat.pow_succ, Nat.mul_comm]319      calc 2 ^ bitsAux fuel (half e) = 2 * 2 ^ (bitsAux fuel (half e) - 1) := key _ hb1320        _ ≤ 2 * half e := Nat.mul_le_mul_left 2 ih321        _ ≤ 2 * half e + par e := Nat.le_add_right _ _322        _ = e := (half_par e).symm323324/-- 26:E10 — the bit-length bracket: `2^(ℓ−1) ≤ e < 2^ℓ` for `ℓ = bits e`, `e > 0`. -/325theorem bits_bracket {e : Nat} (he : 0 < e) : 2 ^ (bits e - 1) ≤ e ∧ e < 2 ^ bits e :=326  ⟨pow_bits_pred_le e e (Nat.le_refl e) he, lt_pow_bits e e (Nat.le_refl e)⟩327328/-- The sum of the distances `1, …, n` along the orbit. -/329def distSum : Nat → Nat330  | 0 => 0331  | n + 1 => distSum n + (n + 1)332333/-- 26:E10 — the distances `1, …, n` have mean `(n + 1)/2` (`P/2` on the cycle of `n = P − 1` units):334`2 · Σ_{k<n} (k + 1) = n (n + 1)`. -/335theorem two_mul_distSum : ∀ n : Nat, 2 * distSum n = n * (n + 1)336  | 0 => rfl337  | n + 1 => by338    show 2 * (distSum n + (n + 1)) = (n + 1) * (n + 1 + 1)339    rw [Nat.mul_add, two_mul_distSum n, ← Nat.add_mul, Nat.mul_comm]340341/-- 26:E10 — the maximum of the distances `1, …, n` is `n`: every `k + 1` with `k < n` is at most `n`. -/342theorem dist_le (n : Nat) : ∀ k, k < n → k + 1 ≤ n := fun _ hk => hk343344/-! ## The ascent: square-and-multiply with its count (26:F2, G4) -/345346/-- Square-and-multiply, right to left, by fuel: the pair (accumulator, multiplications). -/347def sqmulAux (b r : Shell p) (ops : Nat) : Nat → Nat → Shell p × Nat348  | 0, _ => (r, ops)349  | fuel + 1, e =>350    if e = 0 then (r, ops)351    else352      sqmulAux (b * b) (if par e = 1 then r * b else r) ((if par e = 1 then ops + 1 else ops) + 1) fuel (half e)353354/-- Square-and-multiply: `b^e` and the number of modular multiplications used. -/355def sqmul (b : Shell p) (e : Nat) : Shell p × Nat := sqmulAux b 1 0 e e356357theorem sqmulAux_spec : ∀ (fuel e : Nat) (b r : Shell p) (ops : Nat), e ≤ fuel →358    (sqmulAux b r ops fuel e).1 = r * b ^ e359  | 0, e, b, r, ops, h => by360    have he : e = 0 := Nat.le_zero.1 h361    subst he; show r = r * 1; rw [mul_one]362  | fuel + 1, e, b, r, ops, h => by363    show (if e = 0 then (r, ops) else sqmulAux (b * b) (if par e = 1 then r * b else r)364      ((if par e = 1 then ops + 1 else ops) + 1) fuel (half e)).1 = r * b ^ e365    match Nat.decEq e 0 with366    | isTrue h0 => rw [ite_eq_left h0, h0, pow_zero, mul_one]367    | isFalse h0 =>368      rw [ite_eq_right h0]369      have hl := half_lt (Nat.pos_of_ne_zero h0)370      rw [sqmulAux_spec fuel (half e) (b * b) _ _ (Nat.le_of_lt_succ (Nat.lt_of_lt_of_le hl h))]371      have hb : (b * b) ^ half e = b ^ (2 * half e) := by rw [mul_pow, Nat.mul_comm, pow_mul, pow_succ, pow_one]372      rw [hb]373      match (par_lt_two e), Nat.decEq (par e) 1 with374      | _, isTrue h1 =>375        rw [ite_eq_left h1]376        calc r * b * b ^ (2 * half e) = r * b ^ (2 * half e + 1) := by377              rw [pow_succ, mul_assoc, mul_comm b]378          _ = r * b ^ e := by rw [← h1]; conv => rhs; rw [half_par e]379      | hlt, isFalse h1 =>380        rw [ite_eq_right h1]381        have h0' : par e = 0 := by382          match (par e), hlt, h1 with383          | 0, _, _ => rfl384          | 1, _, h1 => exact absurd rfl h1385          | n + 2, hlt, _ => exact absurd hlt (Nat.not_lt_of_le (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le n))))386        have : e = 2 * half e := by conv => lhs; rw [half_par e, h0', Nat.add_zero]387        rw [← this]388389/-- 26:F2 — square-and-multiply computes `b^e`. -/390theorem sqmul_spec (b : Shell p) (e : Nat) : (sqmul b e).1 = b ^ e := by391  unfold sqmul; rw [sqmulAux_spec e e b 1 0 (Nat.le_refl e), one_mul]392393theorem sqmulAux_count : ∀ (fuel e : Nat) (b r : Shell p) (ops : Nat), e ≤ fuel →394    (sqmulAux b r ops fuel e).2 ≤ ops + 2 * bitsAux fuel e395  | 0, e, b, r, ops, _ => Nat.le_add_right _ _396  | fuel + 1, e, b, r, ops, h => by397    show (if e = 0 then (r, ops) else sqmulAux (b * b) (if par e = 1 then r * b else r)398      ((if par e = 1 then ops + 1 else ops) + 1) fuel (half e)).2399      ≤ ops + 2 * (if e = 0 then 0 else bitsAux fuel (half e) + 1)400    match Nat.decEq e 0 with401    | isTrue h0 => rw [ite_eq_left h0, ite_eq_left h0]; exact Nat.le_add_right _ _402    | isFalse h0 =>403      rw [ite_eq_right h0, ite_eq_right h0]404      have hl := half_lt (Nat.pos_of_ne_zero h0)405      have ih := sqmulAux_count fuel (half e) (b * b) (if par e = 1 then r * b else r)406        ((if par e = 1 then ops + 1 else ops) + 1) (Nat.le_of_lt_succ (Nat.lt_of_lt_of_le hl h))407      have hops : (if par e = 1 then ops + 1 else ops) + 1 ≤ ops + 2 := by408        match Nat.decEq (par e) 1 with409        | isTrue h1 => rw [ite_eq_left h1]; exact Nat.le_refl _410        | isFalse h1 => rw [ite_eq_right h1]; exact Nat.le_succ _411      calc _ ≤ (if par e = 1 then ops + 1 else ops) + 1 + 2 * bitsAux fuel (half e) := ih412        _ ≤ ops + 2 + 2 * bitsAux fuel (half e) := Nat.add_le_add_right hops _413        _ = ops + 2 * (bitsAux fuel (half e) + 1) := by414          rw [Nat.mul_succ, Nat.add_assoc, Nat.add_comm 2]415416/-- 26:F2, 26:G4 — square-and-multiply uses at most `2·bits e` multiplications; for `e < 2^l`, at most `2l`. -/417theorem sqmul_count (b : Shell p) (e : Nat) : (sqmul b e).2 ≤ 2 * bits e := by418  have h := sqmulAux_count e e b 1 0 (Nat.le_refl e)419  rw [Nat.zero_add] at h420  exact h421422/-- 26:F2, 26:G4 — for an exponent below `2^l`, square-and-multiply uses at most `2l` multiplications: `O(ℓ)` on a shell423of `ℓ` bits. -/424theorem sqmul_count_of_lt_pow (b : Shell p) {e l : Nat} (he : e < 2 ^ l) : (sqmul b e).2 ≤ 2 * l :=425  Nat.le_trans (sqmul_count b e) (Nat.mul_le_mul_left 2 (bits_le_of_lt_pow he))426427/-! ## The descent: baby-step–giant-step with its count (26:F3, G4) -/428429/-- The least `m < n` with `P m`, by search. -/430def findLT (P : Nat → Prop) [DecidablePred P] : Nat → Option Nat431  | 0 => none432  | n + 1 =>433    match findLT P n with434    | some m => some m435    | none => if P n then some n else none436437theorem findLT_some {P : Nat → Prop} [DecidablePred P] : ∀ {n m : Nat}, findLT P n = some m → m < n ∧ P m438  | 0, m, h => by cases h439  | n + 1, m, h => by440    unfold findLT at h441    match hf : findLT P n with442    | some m' =>443      rw [hf] at h444      have hm : m' = m := Option.some.inj h445      have := findLT_some hf446      exact ⟨Nat.lt_succ_of_lt (hm ▸ this.1), hm ▸ this.2⟩447    | none =>448      rw [hf] at h449      have h' : (if P n then some n else none) = some m := h450      match (inferInstance : Decidable (P n)) with451      | isTrue hp =>452        rw [ite_eq_left hp] at h'453        have hm : n = m := Option.some.inj h'454        exact ⟨hm ▸ Nat.lt_succ_self n, hm ▸ hp⟩455      | isFalse hp =>456        rw [ite_eq_right hp] at h'457        cases h'458459theorem findLT_of_exists {P : Nat → Prop} [DecidablePred P] : ∀ {n : Nat}, (∃ m, m < n ∧ P m) →460    ∃ m, findLT P n = some m461  | 0, ⟨m, hm, _⟩ => absurd hm (Nat.not_lt_zero m)462  | n + 1, ⟨m, hm, hp⟩ =>463    match hf : findLT P n with464    | some m' => ⟨m', by unfold findLT; rw [hf]⟩465    | none =>466      match Nat.lt_or_ge m n with467      | .inl hlt =>468        match findLT_of_exists ⟨m, hlt, hp⟩ with469        | ⟨m'', h''⟩ => by rw [hf] at h''; cases h''470      | .inr hge =>471        have hmn : m = n := Nat.le_antisymm (Nat.le_of_lt_succ hm) hge472        ⟨n, by473          unfold findLT; rw [hf]474          show (if P n then some n else none) = some n475          rw [ite_eq_left (hmn ▸ hp)]⟩476477/-- The giant steps: from `γ`, multiply by `u` until the value is in the baby table; `(some (i, j), ops)` with `i`478the number of giant steps taken, `j` the baby index hit and `ops` the multiplications used. -/479def giantAux (u : Shell p) (m : Nat) (baby : Nat → Shell p) : Nat → Nat → Shell p → Nat → Option (Nat × Nat) × Nat480  | 0, _, _, ops => (none, ops)481  | fuel + 1, i, γ, ops =>482    match findLT (fun j => γ = baby j) m with483    | some j => (some (i, j), ops)484    | none => giantAux u m baby fuel (i + 1) (γ * u) (ops + 1)485486/-- Baby-step–giant-step on the frame: `m` baby steps `g^j`, giant steps by `g^{n−m}` from the target `h`. -/487def bsgs (g h : Shell p) (n m : Nat) : Option (Nat × Nat) × Nat :=488  giantAux (g ^ (n - m)) m (fun j => g ^ j) m 0 h 0489490/-- 26:F3 — the baby steps are one multiplication each: `g^{j+1} = g^j · g`. -/491theorem baby_step (j : Nat) : g ^ (j + 1) = g ^ j * g := pow_succ g j492493theorem giantAux_count (u : Shell p) (m : Nat) (baby : Nat → Shell p) :494    ∀ (fuel i : Nat) (γ : Shell p) (ops : Nat), (giantAux u m baby fuel i γ ops).2 ≤ ops + fuel495  | 0, _, _, ops => Nat.le_refl _496  | fuel + 1, i, γ, ops => by497    unfold giantAux498    match findLT (fun j => γ = baby j) m with499    | some j => exact Nat.le_add_right _ _500    | none =>501      calc _ ≤ ops + 1 + fuel := giantAux_count u m baby fuel (i + 1) (γ * u) (ops + 1)502        _ = ops + (fuel + 1) := by rw [Nat.add_assoc, Nat.add_comm 1]503504theorem giantAux_spec (u : Shell p) (m : Nat) (baby : Nat → Shell p) :505    ∀ (fuel i : Nat) (γ : Shell p) (ops i' j : Nat),506      (giantAux u m baby fuel i γ ops).1 = some (i', j) → j < m ∧ i ≤ i' ∧ γ * u ^ (i' - i) = baby j507  | 0, _, _, _, _, _, h => by cases h508  | fuel + 1, i, γ, ops, i', j, h => by509    unfold giantAux at h510    match hf : findLT (fun j => γ = baby j) m with511    | some j' =>512      rw [hf] at h513      have hj := findLT_some hf514      have e := Prod.mk.inj (Option.some.inj h)515      rw [← e.1, ← e.2, Nat.sub_self, pow_zero, mul_one]516      exact ⟨hj.1, Nat.le_refl _, hj.2⟩517    | none =>518      rw [hf] at h519      obtain ⟨hj, hi, hγ⟩ := giantAux_spec u m baby fuel (i + 1) (γ * u) (ops + 1) i' j h520      refine ⟨hj, Nat.le_of_succ_le hi, ?_⟩521      have : i' - i = (i' - (i + 1)) + 1 := by522        conv => lhs; rw [← FRC.Nat.add_sub_of_le hi, Nat.add_assoc, Nat.add_comm 1, FRC.Nat.add_sub_cancel_left]523      rw [this, pow_succ, ← mul_assoc, mul_comm (γ * u ^ (i' - (i + 1))) u, ← mul_assoc, mul_comm u γ]524      exact hγ525526theorem giantAux_of_exists (u : Shell p) (m : Nat) (baby : Nat → Shell p) :527    ∀ (fuel i : Nat) (γ : Shell p) (ops : Nat),528      (∃ t, t < fuel ∧ ∃ j, j < m ∧ γ * u ^ t = baby j) → ∃ r, (giantAux u m baby fuel i γ ops).1 = some r529  | 0, _, _, _, ⟨t, ht, _⟩ => absurd ht (Nat.not_lt_zero t)530  | fuel + 1, i, γ, ops, ⟨t, ht, j, hj, hγ⟩ =>531    match hf : findLT (fun j => γ = baby j) m with532    | some j' => ⟨(i, j'), by unfold giantAux; rw [hf]⟩533    | none =>534      match t, ht, hγ with535      | 0, _, hγ =>536        have hγ' : γ = baby j := by rw [pow_zero, mul_one] at hγ; exact hγ537        match findLT_of_exists (P := fun j => γ = baby j) ⟨j, hj, hγ'⟩ with538        | ⟨j'', h''⟩ => by rw [hf] at h''; cases h''539      | t + 1, ht, hγ =>540        match giantAux_of_exists u m baby fuel (i + 1) (γ * u) (ops + 1)541            ⟨t, Nat.lt_of_succ_lt_succ ht, j, hj, by rw [mul_assoc, mul_comm u, ← pow_succ]; exact hγ⟩ with542        | ⟨r, hr⟩ => ⟨r, by unfold giantAux; rw [hf]; exact hr⟩543544/-- The descent's verdict on a target, decidable by the kernel: the pair returned reconstructs the target. -/545def descendsB (g h : Shell p) (n m : Nat) : Bool :=546  match (bsgs g h n m).1 with547  | some (i, j) => decide (j < m) && decide (g ^ (j + m * i) = h)548  | none => false549550/-- 26:F3 — the kernel's verdict unpacked: when `descendsB` holds, the search returns `(i, j)` with `j < m` and551`g^{j + m i} = h`. -/552theorem descendsB_spec {g h : Shell p} {n m : Nat} (hd : descendsB g h n m = true) :553    ∃ i j, (bsgs g h n m).1 = some (i, j) ∧ j < m ∧ g ^ (j + m * i) = h := by554  unfold descendsB at hd555  match hb : (bsgs g h n m).1 with556  | some (i, j) =>557    rw [hb] at hd558    have hd' : (decide (j < m) && decide (g ^ (j + m * i) = h)) = true := hd559    have h1 : decide (j < m) = true := by560      match hc : decide (j < m) with561      | true => rfl562      | false => rw [hc] at hd'; cases hd'563    rw [h1] at hd'564    have h2 : decide (g ^ (j + m * i) = h) = true := by565      match hc : decide (g ^ (j + m * i) = h) with566      | true => rfl567      | false => rw [hc] at hd'; cases hd'568    exact ⟨i, j, rfl, of_decide_eq_true h1, of_decide_eq_true h2⟩569  | none => rw [hb] at hd; cases hd570571/-- 26:F3, 26:G4 — the descent: for `m ≤ n ≤ m²`, baby-step–giant-step from `h = g^x` (`x < n`) returns `(i, j)` with572`g^{j + m i} = h`, so the index is recovered modulo `n`, after at most `m` giant-step multiplications. -/573theorem bsgs_spec (F : Frame p κ g) {m : Nat} (hm : m ≤ p - 1) (hmm : p - 1 ≤ m * m) {x : Nat} (hx : x < p - 1) :574    (∃ i j, (bsgs g (g ^ x) (p - 1) m).1 = some (i, j) ∧ j < m ∧ g ^ (j + m * i) = g ^ x) ∧575    (bsgs g (g ^ x) (p - 1) m).2 ≤ m := by576  have hm0 : 0 < m := by577    match m, hmm with578    | 0, hmm => exact absurd (Nat.lt_of_lt_of_le F.n_pos hmm) (Nat.lt_irrefl 0)579    | m + 1, _ => exact Nat.zero_lt_succ m580  have hu : g ^ (p - 1 - m) * g ^ m = 1 := by rw [← pow_add, FRC.Nat.sub_add_cancel hm, F.pow_n]581  have hcount : (bsgs g (g ^ x) (p - 1) m).2 ≤ m := by582    have hc := giantAux_count (g ^ (p - 1 - m)) m (fun j => g ^ j) m 0 (g ^ x) 0583    rw [Nat.zero_add] at hc584    exact hc585  refine ⟨?_, hcount⟩586  -- the hit exists at the giant step `q`, `x = m q + r`587  obtain ⟨q, hq⟩ := FRC.Nat.mod_spec m hm0 x588  have hr : x % m < m := Nat.mod_lt x hm0589  have hqm : q < m := by590    have h1 : m * q < m * m := Nat.lt_of_le_of_lt (by rw [hq]; exact Nat.le_add_right _ _) (Nat.lt_of_lt_of_le hx hmm)591    exact lt_of_mul_lt_mul_left' h1592  have hhit : g ^ x * (g ^ (p - 1 - m)) ^ q = g ^ (x % m) := by593    have e1 : x + (p - 1 - m) * q = x % m + (p - 1) * q := by594      conv => lhs; rw [hq]595      rw [Nat.add_right_comm, Nat.add_comm, ← FRC.Nat.add_mul, Nat.add_comm m, FRC.Nat.sub_add_cancel hm]596    rw [← pow_mul, ← pow_add, e1, pow_add, pow_mul, F.pow_n, one_pow, mul_one]597  obtain ⟨⟨i', j⟩, hr'⟩ := giantAux_of_exists (g ^ (p - 1 - m)) m (fun j => g ^ j) m 0 (g ^ x) 0598    ⟨q, hqm, x % m, hr, hhit⟩599  obtain ⟨hj, _, hγ⟩ := giantAux_spec (g ^ (p - 1 - m)) m (fun j => g ^ j) m 0 (g ^ x) 0 i' j hr'600  refine ⟨i', j, hr', hj, ?_⟩601  have hγ' : g ^ x * (g ^ (p - 1 - m)) ^ i' = g ^ j := by rw [Nat.sub_zero] at hγ; exact hγ602  calc g ^ (j + m * i') = g ^ j * (g ^ m) ^ i' := by rw [pow_add, pow_mul]603    _ = g ^ x * (g ^ (p - 1 - m)) ^ i' * (g ^ m) ^ i' := by rw [hγ']604    _ = g ^ x * (g ^ (p - 1 - m) * g ^ m) ^ i' := by rw [mul_assoc, ← mul_pow]605    _ = g ^ x := by rw [hu, one_pow, mul_one]606607/-- 26:F3 — the descent's total: the `m` baby steps and the giant multiplications together are at most `2m`. -/608theorem bsgs_total (F : Frame p κ g) {m : Nat} (hm : m ≤ p - 1) (hmm : p - 1 ≤ m * m) {x : Nat} (hx : x < p - 1) :609    m + (bsgs g (g ^ x) (p - 1) m).2 ≤ 2 * m := by610  have h := (bsgs_spec F hm hmm hx).2611  rw [Nat.two_mul]612  exact Nat.add_le_add_left h m613614/-! ## The reference shape `𝔽₁₃` and `𝔽₁₀₁`, decided by the kernel (26:B3, E8, F2, F3, G2, G3, G5) -/615616/-- 26:B3, the reference shape — the twelve eigenvalues `2^ν` of the scale shift on `𝔽₁₃` are distinct. -/617theorem eigenvalues13 : ∀ i, i < 12 → ∀ j, j < 12 → (2 : Shell 13) ^ i = 2 ^ j → i = j :=618  @of_decide_eq_true _ (@decForallLT (fun i => ∀ j, j < 12 → (2 : Shell 13) ^ i = 2 ^ j → i = j)619    (fun i => decForallLT (fun j => (2 : Shell 13) ^ i = 2 ^ j → i = j) 12) 12) (by decide +kernel)620621/-- 26:G3, the reference shape — the phase formula on `𝔽₁₃`: two iterates of `x ↦ x³` carry `2^m` to `2^{9m mod 12}`,622and three iterates of `x ↦ x²` to `2^{8m mod 12}`. -/623theorem phase13 : ∀ m, m < 12 → iter (fun x : Shell 13 => x ^ 3) 2 (2 ^ m) = 2 ^ ((9 * m) % 12) ∧624    iter (fun x : Shell 13 => x ^ 2) 3 (2 ^ m) = 2 ^ ((8 * m) % 12) :=625  @of_decide_eq_true _ (decForallLT (fun m => iter (fun x : Shell 13 => x ^ 3) 2 (2 ^ m) = 2 ^ ((9 * m) % 12) ∧626    iter (fun x : Shell 13 => x ^ 2) 3 (2 ^ m) = 2 ^ ((8 * m) % 12)) 12) (by decide +kernel)627628/-- 26:G2, the reference shape — a tower exponent is read modulo `12`: `2^{(2^j)} = 2^{(2^j) mod 12}` on `𝔽₁₃`. -/629theorem tower13 : ∀ j, j < 12 → (2 : Shell 13) ^ ((2 : Shell 13) ^ j).val = 2 ^ (((2 : Shell 13) ^ j).val % 12) :=630  @of_decide_eq_true _ (decForallLT (fun j => (2 : Shell 13) ^ ((2 : Shell 13) ^ j).val =631    2 ^ (((2 : Shell 13) ^ j).val % 12)) 12) (by decide +kernel)632633/-- 26:E8, the reference shape — every index of `𝔽₁₃` is recentred to one step from the origin. -/634theorem recentre13 : ∀ m, m < 12 → (2 : Shell 13) ^ recentre 12 m m = 2 :=635  @of_decide_eq_true _ (decForallLT (fun m => (2 : Shell 13) ^ recentre 12 m m = 2) 12) (by decide +kernel)636637/-- 26:G5, the reference shape — on `𝔽₁₃` the power map `x ↦ x⁵` is a bijection (`5 · 5 = 25 ≡ 1 (mod 12)`), and638`x ↦ x⁴` compresses the units onto the three powers of `2⁴ = 3` (`gcd(4, 12) = 4`, `1 · 4 = 0 · 12 + 4`). -/639theorem powers13 : (∀ m, m < 12 → (((2 : Shell 13) ^ m) ^ 5) ^ 5 = 2 ^ m) ∧640    (∀ m, m < 12 → ∃ i, i < 3 ∧ ((2 : Shell 13) ^ m) ^ 4 = ((2 : Shell 13) ^ 4) ^ i) ∧641    (∀ i, i < 3 → ∃ m, m < 12 ∧ ((2 : Shell 13) ^ m) ^ 4 = ((2 : Shell 13) ^ 4) ^ i) :=642  ⟨@of_decide_eq_true _ (decForallLT (fun m => (((2 : Shell 13) ^ m) ^ 5) ^ 5 = 2 ^ m) 12) (by decide +kernel),643   @of_decide_eq_true _ (@decForallLT (fun m => ∃ i, i < 3 ∧ ((2 : Shell 13) ^ m) ^ 4 = ((2 : Shell 13) ^ 4) ^ i)644     (fun m => decExistsLT (fun i => ((2 : Shell 13) ^ m) ^ 4 = ((2 : Shell 13) ^ 4) ^ i) 3) 12) (by decide +kernel),645   @of_decide_eq_true _ (@decForallLT (fun i => ∃ m, m < 12 ∧ ((2 : Shell 13) ^ m) ^ 4 = ((2 : Shell 13) ^ 4) ^ i)646     (fun i => decExistsLT (fun m => ((2 : Shell 13) ^ m) ^ 4 = ((2 : Shell 13) ^ 4) ^ i) 12) 3) (by decide +kernel)⟩647648/-- 26:F2, the reference shape — square-and-multiply on `𝔽₁₃` computes every `2^e`, `e < 64`, within `2·bits e`649multiplications; `2^{11}` in seven. -/650theorem sqmul13 : (∀ e, e < 64 → (sqmul (2 : Shell 13) e).1 = 2 ^ e ∧ (sqmul (2 : Shell 13) e).2 ≤ 2 * bits e) ∧651    (sqmul (2 : Shell 13) 11).2 = 7 :=652  ⟨@of_decide_eq_true _ (decForallLT (fun e => (sqmul (2 : Shell 13) e).1 = 2 ^ e ∧653      (sqmul (2 : Shell 13) e).2 ≤ 2 * bits e) 64) (by decide +kernel), by decide⟩654655/-- 26:F3, the reference shape and `𝔽₁₀₁` — baby-step–giant-step recovers every index: on `𝔽₁₃` with `m = 4`656(`16 ≥ 12`), on `𝔽₁₀₁` with `m = 10` (`100 ≥ 100`), the pair returned reconstructs the target. -/657theorem descent13_101 : (∀ x, x < 12 → descendsB (2 : Shell 13) (2 ^ x) 12 4 = true) ∧658    (∀ x, x < 100 → descendsB (2 : Shell 101) (2 ^ x) 100 10 = true) :=659  ⟨@of_decide_eq_true _ (decForallLT (fun x => descendsB (2 : Shell 13) (2 ^ x) 12 4 = true) 12) (by decide +kernel),660   @of_decide_eq_true _ (decForallLT (fun x => descendsB (2 : Shell 101) (2 ^ x) 100 10 = true) 100) (by decide +kernel)⟩661662end FRC.Ladder663