Theme/Horizon.lean — FrcCore

1import FrcCore.Transform2import FrcCore.Theme.Extension3import FrcCore.Theme.Foundation45/-!6# FrcCore.Theme.Horizon — the horizon theme: the shell theorem (ledger migration, task LM26)78The master's block Z, the limits of the bounded observer, where its rows are exact on every shell. The shell theorem9(00:Z10, 20:E12) in the `𝔽_p` reading, on a frame `(τ; 0, 1, g)` of capacity `κ` (`p = 4κ + 1`, `n = p − 1`):1011* the finite zeta `Z(k) = Σ_{x≠0} x^k` vanishes on every nonterminal mode `0 < k < n` and is `−1` on the full12  cycle (`zero_slot`, 20:B4);13* every vector on the cycle expands in the power modes `x ↦ x^k`, `k < n`: the constant mode and the nonterminal14  ones (`mode_expansion`);15* the scale-shift `x ↦ g^r x` has the modes as eigenvectors, `(g^r x)^k = (g^r)^k x^k`, with an `n`-th root of unity16  as eigenvalue (`shift_power_character`, `eigenphase`), and fixes `n·[n ∣ r]` points (`shift_trace`);17* every readout `z(θ) = 2⁻¹ + θη` lies on the self-dual line `Tr z = 1`, `2⁻¹ = 2κ + 1` (`readout_on_line`), and a18  nontrivial slot's index is neither `0` nor `−1` (`readout_slot_index`).1920No hypothesis on the vector and none on the shell beyond the frame: no off-line mode, `Ω`-blind. `half_inverse`,21`zero_slot`, `shift_power_character`, `shift_trace`, `readout`, `readout_on_line` and `readout_slot_index` moved here22from `FrcCore/Rh.lean` (20-rh), which keeps each under its old name.2324Since task LM36 the theme also holds the rest of 20-rh's shell arithmetic, moved from `Rh.lean` under the same names25(the extension's `Ext.*` without the prefix): slot complementarity (20:B5); the Subject constants (20:B10); the26Ramanujan sum (20:B7); the half-turn `ρ`, the Klein four-group, the critical line, the fixed loci and the energy on the27line in the quadratic extension, and the quarter-turn off the circle (20:B6, B8, B9); frame coincidence below the28horizon (20:B2); and the values on `𝔽₁₃`, `𝔽₅₃` and the laboratory pair `(13, 233)` (20:B1). The theme imports the29transform and the extension, not the orbits, so that its key file stays within the budget of gate G10. No axioms.30-/3132namespace FRC.Horizon3334open FRC.Shell FRC.Shell.Frame35open FRC.Extension (Ext)3637variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}3839/-- Double sums commute: `Σ_{i<n} Σ_{j<m} f i j = Σ_{j<m} Σ_{i<n} f i j`. -/40theorem sum_comm (f : Nat → Nat → Shell p) (m : Nat) : ∀ n,41    sumRange (fun i => sumRange (fun j => f i j) m) n = sumRange (fun j => sumRange (fun i => f i j) n) m42  | 0 => (sum_zero m (fun _ _ => rfl)).symm43  | n + 1 => by44    rw [sumRange_succ, sum_comm f m n, ← sum_add]45    rfl4647/-! ## The half-turn (20:B8) -/4849/-- 20:B8 — `2⁻¹ = 2κ + 1 = −π` on every shell: `2·(2κ + 1) = 1` and `2κ + 1 = −(2κ)`. -/50theorem half_inverse (F : Frame p κ g) :51    (2 : Shell p) * ofNat (2 * κ + 1) = 1 ∧ (ofNat (2 * κ + 1) : Shell p) = -(ofNat (2 * κ)) := by52  have e : 2 * (2 * κ + 1) = 1 + p := by53    rw [F.cap]54    calc 2 * (2 * κ + 1) = 2 * (2 * κ) + 2 * 1 := Nat.mul_add 2 (2 * κ) 155      _ = 4 * κ + 2 := by rw [← FRC.Nat.mul_assoc]56      _ = 1 + (4 * κ + 1) := by rw [Nat.add_comm 1, Nat.add_assoc]57  constructor58  · show ofNat 2 * ofNat (2 * κ + 1) = 159    rw [ofNat_mul, e, ofNat_add_self]60    rfl61  · have e2 : 2 * κ + (2 * κ + 1) = p := by62      rw [← Nat.add_assoc, F.four_kappa]; exact FRC.Nat.sub_add_cancel Pos.pos63    have h : (ofNat (2 * κ) : Shell p) + ofNat (2 * κ + 1) = 0 := by64      rw [ofNat_add, e2]; exact ofNat_self65    exact (neg_eq_of_add_eq_zero h).symm6667/-! ## The modes: the finite zeta and the expansion (20:B4, 20:E12 (i)) -/6869/-- 20:B4, Z10 — the finite zeta on every shell: over the nonzero residues `x = l + 1`, `l < p − 1`,70`Σ x^k = 0` for every nonterminal exponent `0 < k < p − 1`, and `Σ x^{p−1} = −1` on the full cycle. -/71theorem zero_slot (F : Frame p κ g) :72    (∀ k, 0 < k → k < p - 1 → sumRange (fun l => (ofNat (l + 1) : Shell p) ^ k) (p - 1) = 0) ∧73    sumRange (fun l => (ofNat (l + 1) : Shell p) ^ (p - 1)) (p - 1) = -1 := by74  constructor75  · intro k hk0 hk76    rw [sum_units_eq_sum_pow F (fun x => x ^ k)]77    have e : ∀ m, m < p - 1 → (fun m => (g ^ m) ^ k) m = (fun m => (g ^ k) ^ m) m := fun m _ =>78      pow_mul_comm g m k79    rw [sum_congr (p - 1) e]80    exact (F.principal_root k hk0 hk).2.181  · rw [sum_units_eq_sum_pow F (fun x => x ^ (p - 1))]82    have e : ∀ m, m < p - 1 → (fun m => (g ^ m) ^ (p - 1)) m = (fun _ => (1 : Shell p)) m := fun m _ => by83      show (g ^ m) ^ (p - 1) = 184      rw [pow_mul_comm, F.pow_n, one_pow]85    rw [sum_congr (p - 1) e, sum_const, mul_one, F.ofNat_n]8687/-- The coefficient of the mode `k` in a vector `v` on the cycle: `c_k = −Σ_{l<n} v_l g^{(n−l)k}`. -/88def modeCoeff (g : Shell p) (v : Nat → Shell p) (k : Nat) : Shell p :=89  sumRange (fun l => v l * -(g ^ ((p - 1 - l) * k))) (p - 1)9091/-- 20:E12 (i), Z10 — every vector on the cycle expands in the power modes: at the point `x = g^j`,92`v_j = Σ_{k<p−1} c_k x^k`, the constant mode `k = 0` and the nonterminal modes `0 < k < p − 1`. -/93theorem mode_expansion (F : Frame p κ g) (v : Nat → Shell p) {j : Nat} (hj : j < p - 1) :94    v j = sumRange (fun k => modeCoeff g v k * (g ^ j) ^ k) (p - 1) := by95  have h1 : sumRange (fun k => modeCoeff g v k * (g ^ j) ^ k) (p - 1)96      = sumRange (fun k => sumRange (fun l => v l * (g ^ (k * j) * -(g ^ ((p - 1 - l) * k)))) (p - 1)) (p - 1) := by97    apply sum_congr; intro k _98    unfold modeCoeff99    rw [← sum_mul_right]100    apply sum_congr; intro l _101    rw [← pow_mul, Nat.mul_comm j k, mul_assoc, mul_comm (-(g ^ ((p - 1 - l) * k))) (g ^ (k * j))]102  rw [h1, sum_comm (fun k l => v l * (g ^ (k * j) * -(g ^ ((p - 1 - l) * k)))) (p - 1) (p - 1)]103  have h2 : ∀ l, l < p - 1 → sumRange (fun k => v l * (g ^ (k * j) * -(g ^ ((p - 1 - l) * k)))) (p - 1)104      = v l * (if j = l then 1 else 0) := fun l hl => by105    rw [sum_mul_left, F.dft_inverse hj hl]106  rw [sum_congr (p - 1) h2, sum_eq_single hj (fun l _ hne => by rw [ite_eq_right (fun e => hne e.symm), mul_zero]),107    ite_eq_left rfl, mul_one]108109/-! ## The scale-shift (20:E1, 20:E12 (iii)) -/110111/-- 20:E1, 20:E12, 26:B3 — the power characters are eigenvectors of the scale-shift `x ↦ g^r x` in the `𝔽_p` reading:112`(g^r x)^k = (g^r)^k · x^k`. -/113theorem shift_power_character (r k : Nat) (x : Shell p) : (g ^ r * x) ^ k = (g ^ r) ^ k * x ^ k :=114  mul_pow _ _ _115116/-- 20:E12 (iii), 20:Z10, 26:B3 — the eigenvalue `(g^r)^k` of the mode `k` under the scale-shift is a `(p − 1)`-th root of117unity, independent of the vector. -/118theorem eigenphase (F : Frame p κ g) (r k : Nat) : ((g ^ r) ^ k) ^ (p - 1) = 1 := by119  rw [pow_mul_comm, pow_mul_comm g r (p - 1), F.pow_n, one_pow, one_pow]120121/-- 20:E12, 20:E1, 26:B3 — clause (iii) in the `𝔽_p` reading: the fixed-point count of the scale-shift, the trace of its122permutation matrix: `x ↦ g^r x` fixes every nonzero residue when `(p − 1) ∣ r` and none otherwise,123`Tr S^r = (p − 1)·[(p − 1) ∣ r]`; the shell's trace carries no prime data. -/124theorem shift_trace (F : Frame p κ g) (r : Nat) :125    natCount (fun x => x ≠ 0 ∧ g ^ r * ofNat x = ofNat x) p = if r % (p - 1) = 0 then p - 1 else 0 := by126  have hn : p = (p - 1) + 1 := (FRC.Nat.sub_add_cancel Pos.pos).symm127  match (inferInstance : Decidable (r % (p - 1) = 0)) with128  | isTrue h =>129    rw [ite_eq_left h]130    have h1 : g ^ r = 1 := F.pow_eq_one_of_mod h131    have e : ∀ x, x < p → ((x ≠ 0 ∧ g ^ r * ofNat x = ofNat x) ↔ x ≠ 0) := fun x _ =>132      ⟨fun h => h.1, fun h => ⟨h, by rw [h1, one_mul]⟩⟩133    have hc := natCount_ne_zero (p - 1)134    rw [← hn] at hc135    rw [natCount_congr _ _ p e]136    exact hc137  | isFalse h =>138    rw [ite_eq_right h]139    apply natCount_eq_zero140    intro x hx hP141    apply h142    apply F.mod_eq_zero_of_pow_eq_one143    have hx0 : (ofNat x : Shell p) ≠ 0 := fun h0 => by144      have := val_injective h0145      rw [val_ofNat, val_zero, FRC.Nat.mod_eq_of_lt hx] at this146      exact hP.1 this147    apply F.mul_left_cancel hx0148    rw [mul_comm, hP.2, mul_one]149150/-! ## The readout on the self-dual line (20:B8, 20:E12 (ii)) -/151152variable {ν : Shell p}153154/-- 20:E12, 20:B8 — the spectral readout in the core: the mode index `θ` is read at `z(θ) = 2⁻¹ + θη`,155`2⁻¹ = 2κ + 1`, in the quadratic extension `𝔽_p(η)`, `η² = ν`. -/156def readout (ν : Shell p) (κ : Nat) (θ : Shell p) : Ext p ν := ⟨ofNat (2 * κ + 1), θ⟩157158/-- 20:E12 (ii), Z10 — every readout lies on the self-dual line `Tr z = 1`, its real part the half-turn159`2⁻¹ = 2κ + 1`, and `θ ↦ z(θ)` is injective: no off-line mode. -/160theorem readout_on_line (F : Frame p κ g) (ν θ : Shell p) :161    Ext.trace (readout ν κ θ) = 1 ∧ (readout ν κ θ).re = ofNat (2 * κ + 1) ∧162    ∀ θ' : Shell p, readout ν κ θ = readout ν κ θ' → θ = θ' := by163  refine ⟨?_, rfl, fun θ' h => Ext.im_congr h⟩164  show ofNat (2 * κ + 1) + ofNat (2 * κ + 1) = 1165  rw [← two_mul', (half_inverse F).1]166167/-- 20:E12 — the slot index of a nontrivial slot: for `1 ≤ k ≤ p − 2` the index `θ = Φ(k) = −g^k` is neither168`0` (the centre `2⁻¹`) nor `−1` (the full-cycle exponent), on every shell and with no axioms. -/169theorem readout_slot_index (F : Frame p κ g) (k : Nat) (hk1 : 1 ≤ k) (hk2 : k ≤ p - 2) :170    -(g ^ k) ≠ 0 ∧ -(g ^ k) ≠ -1 := by171  refine ⟨fun h => F.pow_ne_zero k ?_, fun h => ?_⟩172  · calc g ^ k = - -(g ^ k) := (neg_neg _).symm173      _ = -0 := by rw [h]174      _ = 0 := neg_zero175  · have h1 : g ^ k = 1 := by176      calc g ^ k = - -(g ^ k) := (neg_neg _).symm177        _ = - -1 := by rw [h]178        _ = 1 := neg_neg 1179    have hmod := F.mod_eq_zero_of_pow_eq_one h1180    have hlt : k < p - 1 :=181      Nat.lt_of_le_of_lt hk2 (Nat.pred_lt (Nat.ne_of_gt F.n_pos))182    rw [FRC.Nat.mod_eq_of_lt hlt] at hmod183    exact Nat.not_succ_le_zero 0 (by rw [hmod] at hk1; exact hk1)184185/-! ## 20-rh's shell arithmetic (task LM36): slot complementarity, the Subject constants (20:B5, 20:B10) -/186187/-- 20:B5 — slot complementarity on every shell: `Φ(k) = −g^k` is injective on the nontrivial spectral slots188`0 < k < p − 1`, its values avoid `0` and `−1`, and every residue off `{0, −1}` is `Φ(k)` for one such `k`. -/189theorem slot_complementarity (F : Frame p κ g) :190    (∀ i j, i < p - 1 → j < p - 1 → -(g ^ i) = -(g ^ j) → i = j) ∧191    (∀ k, 0 < k → k < p - 1 → -(g ^ k) ≠ 0 ∧ -(g ^ k) ≠ -1) ∧192    (∀ y : Shell p, y ≠ 0 → y ≠ -1 → ∃ k, 0 < k ∧ k < p - 1 ∧ -(g ^ k) = y) := by193  refine ⟨fun i j hi hj h => ?_, fun k hk0 hk => ⟨fun h => ?_, fun h => ?_⟩, fun y hy0 hy1 => ?_⟩194  · apply F.pow_inj hi hj195    rw [← neg_neg (g ^ i), h, neg_neg]196  · apply F.pow_ne_zero k197    rw [← neg_neg (g ^ k), h, neg_zero]198  · have h1 : g ^ k = 1 := by rw [← neg_neg (g ^ k), h, neg_neg]199    have := F.mod_eq_zero_of_pow_eq_one h1200    rw [FRC.Nat.mod_eq_of_lt hk] at this201    exact Nat.lt_irrefl 0 (this ▸ hk0)202  · have hny : -y ≠ 0 := fun h => hy0 (by rw [← neg_neg y, h, neg_zero])203    match F.eq_pow_of_ne_zero hny with204    | ⟨m, hm, e⟩ =>205      refine ⟨m, Nat.pos_of_ne_zero (fun h0 => ?_), hm, by rw [e, neg_neg]⟩206      rw [h0, pow_zero] at e207      exact hy1 (by rw [← neg_neg y, ← e])208209/-- 20:B10 — `i = g^{−κ}`, read as `g^{3κ}` on the cycle of length `4κ`, is the quarter-turn `−g^κ`. -/210theorem quarter_turn_eq_pow (F : Frame p κ g) : g ^ (3 * κ) = quarterTurn g κ := by211  unfold quarterTurn212  have e : 3 * κ = κ + 2 * κ := by213    rw [show (3 : Nat) = 1 + 2 from rfl, FRC.Nat.add_mul, Nat.one_mul]214  rw [e, pow_add, F.half_period, ← mul_neg, mul_one]215216/-- 20:B10 — the Subject constants on every shell: `2π = −1` with `π = 2κ`; `i = g^{−κ} = −g^κ` with `i² = −1`;217`g^π = −1`; and `e^{iπ} = (g^m)^{m·π} = −1` for every odd `m` — the convention "`e = g^m` on the odd218representative `m` of `i`" fixes the parity of the exponent, and the identity uses nothing else about `m`. -/219theorem subject_constants (F : Frame p κ g) :220    (ofNat (2 * halfPeriod κ) : Shell p) = -1 ∧ g ^ (3 * κ) = quarterTurn g κ ∧221    quarterTurn g κ * quarterTurn g κ = -1 ∧ g ^ (2 * κ) = -1 ∧222    ∀ m : Nat, m % 2 = 1 → (g ^ m) ^ (m * (2 * κ)) = -1 := by223  refine ⟨F.two_pi, quarter_turn_eq_pow F, F.quarter_turn_sq, F.half_period, fun m hm => ?_⟩224  have h0 : m % 2 ≠ 0 := by rw [hm]; exact fun h => Nat.noConfusion h225  rw [F.euler_identity, ite_eq_right h0]226227/-- 20:B10 [value] — on `𝔽₁₃(τ; 0, 1, 2)`: `π = 6`, `2π = −1`, `i = 2^9 = 5 = −2^3`, `i² = −1`, `e = 2^5 = 6`,228`2^π = −1`, `e^{iπ} = 6^{30} = −1`. -/229theorem constants13 :230    (2 : Shell 13) * 6 = -1 ∧ (2 : Shell 13) ^ 9 = 5 ∧ quarterTurn (2 : Shell 13) 3 = 5 ∧231    (5 : Shell 13) * 5 = -1 ∧ (2 : Shell 13) ^ 5 = 6 ∧ (2 : Shell 13) ^ 6 = -1 ∧232    (6 : Shell 13) ^ (5 * 6) = -1 := by decide233234/-! ## The Ramanujan sum (20:B7) -/235236section ramanujan237variable {q : Nat} [Pos q] {κ' : Nat} {h : Shell q}238239/-- Powers of an element of finite order reduce modulo the order. -/240theorem pow_mod_of_pow_eq_one {ω : Shell q} {m : Nat} (hm : 0 < m) (hω : ω ^ m = 1) (l : Nat) :241    ω ^ l = ω ^ (l % m) := by242  match FRC.Nat.mod_spec m hm l with243  | ⟨c, hc⟩ =>244    calc ω ^ l = ω ^ (m * c + l % m) := by rw [← hc]245      _ = (ω ^ m) ^ c * ω ^ (l % m) := by rw [pow_add, pow_mul]246      _ = ω ^ (l % m) := by rw [hω, one_pow, one_mul]247248/-- 20:B7, 26:B5 — the flat ground state: in a shell `𝔽_q` with a frame (no zero divisors) and an element `ω` of249order exactly `m`, the Ramanujan sum `Σ_{a=1}^{m−1} ω^{an}` equals `−1` for every `n ≢ 0 (mod m)`. With250`m = p` this is `c_p(n) ≡ −1`: the mode at the spectral origin carries no prime information. -/251theorem ramanujan_sum (F : Frame q κ' h) {m : Nat} (hm : 0 < m) {ω : Shell q} (hω : IsPrimitive ω m)252    (n : Nat) (hn : n % m ≠ 0) :253    sumRange (fun a => ω ^ (n * (a + 1))) (m - 1) = -1 := by254  have hx1 : ω ^ n ≠ 1 := by255    rw [pow_mod_of_pow_eq_one hm hω.1 n]256    exact hω.2 (n % m) (Nat.mod_lt n hm) (Nat.pos_of_ne_zero hn)257  have hxm : (ω ^ n) ^ m = 1 := by rw [pow_mul_comm, hω.1, one_pow]258  have h0 := F.geom_sum_eq_zero m hxm hx1259  have hm' : m = (m - 1) + 1 := (FRC.Nat.sub_add_cancel hm).symm260  rw [hm', sumRange_succ', pow_zero] at h0261  have e : ∀ a, a < m - 1 → (fun a => ω ^ (n * (a + 1))) a = (fun l => (ω ^ n) ^ (l + 1)) a := fun a _ =>262    pow_mul ω n (a + 1)263  rw [sum_congr (m - 1) e]264  rw [add_comm] at h0265  exact eq_neg_of_add_eq_zero h0266267/-- 26:B5 — the Ramanujan sum at `n = 0`: `Σ_{a=1}^{m−1} ω^{0·a} = m − 1` (the additive character sum over the units268is `P − 1` for `c = 0`, against `−1` for `c ≠ 0`); no hypothesis on `ω`. -/269theorem ramanujan_zero (ω : Shell q) (m : Nat) :270    sumRange (fun a => ω ^ (0 * (a + 1))) (m - 1) = ofNat (m - 1) := by271  have e : ∀ a, a < m - 1 → (fun a => ω ^ (0 * (a + 1))) a = (fun _ => (1 : Shell q)) a := fun a _ => by272    show ω ^ (0 * (a + 1)) = 1273    rw [Nat.zero_mul, pow_zero]274  rw [sum_congr (m - 1) e, sum_const, mul_one]275276/-- 20:B7 [value] — on `𝔽₅₃` with `ω = 16` of order `13`: `c_{13}(n) = Σ_{a=1}^{12} ω^{an} = −1` for every277`0 < n < 13`, and `12 = m − 1` at `n = 0`. -/278theorem ramanujan53 :279    (∀ n, n < 13 → 0 < n → sumRange (fun a => (16 : Shell 53) ^ (n * (a + 1))) 12 = -1) ∧280    sumRange (fun a => (16 : Shell 53) ^ (0 * (a + 1))) 12 = 12 := by decide281282end ramanujan283284/-! ## The quadratic extension: the half-turn, the critical line, the two loci of agreement (20:B6, 20:B8, 20:B9) -/285286section extension287open FRC.Extension.Ext288289/-- The functional-equation half-turn `ρ : z ↦ 1 − z`. -/290def rho (z : Ext p ν) : Ext p ν := ⟨1 + -z.re, -z.im⟩291292/-- The product `σ = ρ ∘ φ : z ↦ 1 − z̄`. -/293def sigma (z : Ext p ν) : Ext p ν := rho (conj z)294295/-- 20:B9 — conjugation `φ` and the half-turn `ρ` generate a Klein four-group: both are involutions and they296commute, `φ ρ = ρ φ = σ`. -/297theorem klein_four (z : Ext p ν) :298    conj (conj z) = z ∧ rho (rho z) = z ∧ conj (rho z) = rho (conj z) := by299  refine ⟨Ext.ext rfl (neg_neg z.im), Ext.ext ?_ (neg_neg z.im), rfl⟩300  show 1 + -(1 + -z.re) = z.re301  rw [neg_add_rev, neg_neg, ← add_assoc, add_neg, zero_add]302303/-- 20:B8, 20:B9 — the finite critical line: `Tr z = 1` exactly when `Re z = 2⁻¹ = 2κ + 1`; it is the fixed locus304of `σ = ρ ∘ φ`; every `2⁻¹ + bη` lies on it, one point per residue `b` — `p` points. -/305theorem critical_line (F : Frame p κ g) (z : Ext p ν) :306    (trace z = 1 ↔ z.re = ofNat (2 * κ + 1)) ∧ (sigma z = z ↔ z.re = ofNat (2 * κ + 1)) ∧307    ∀ b : Shell p, trace (⟨ofNat (2 * κ + 1), b⟩ : Ext p ν) = 1 := by308  have hinv := (half_inverse F).1309  have key : z.re + z.re = 1 ↔ z.re = ofNat (2 * κ + 1) := by310    constructor311    · intro h312      apply F.mul_left_cancel F.two_ne_zero313      rw [two_mul', h, hinv]314    · intro h315      rw [h, ← two_mul', hinv]316  refine ⟨key, ?_, fun b => ?_⟩317  · constructor318    · intro h319      have h1 : 1 + -z.re = z.re := re_congr h320      apply key.1321      show z.re + z.re = 1322      calc z.re + z.re = (1 + -z.re) + z.re := by rw [h1]323        _ = 1 := by rw [add_assoc, neg_add, add_zero]324    · intro h325      apply Ext.ext326      · show 1 + -z.re = z.re327        have h1 := key.2 h328        calc 1 + -z.re = (z.re + z.re) + -z.re := by rw [h1]329          _ = z.re := by rw [add_assoc, add_neg, add_zero]330      · exact neg_neg z.im331  · show ofNat (2 * κ + 1) + ofNat (2 * κ + 1) = 1332    rw [← two_mul', hinv]333334/-- 20:B9 — the fixed locus of the half-turn `ρ` is the single point `2⁻¹`, the meeting of the prime meridian335and the critical line: `ρ z = z ⟺ (φ z = z ∧ σ z = z) ⟺ z = 2⁻¹ + 0η`. -/336theorem fixed_half_turn (F : Frame p κ g) (z : Ext p ν) :337    (rho z = z ↔ (conj z = z ∧ sigma z = z)) ∧ (rho z = z ↔ z = ⟨ofNat (2 * κ + 1), 0⟩) := by338  have hc := fixed_conj F z339  have hs := (critical_line F z).2.1340  have hr : rho z = z ↔ (z.im = 0 ∧ z.re = ofNat (2 * κ + 1)) := by341    constructor342    · intro h343      have h1 := re_congr h344      have h2 := im_congr h345      refine ⟨F.eq_zero_of_eq_neg h2.symm, hs.1 ?_⟩346      exact Ext.ext (show (sigma z).re = z.re from h1) (show (sigma z).im = z.im from neg_neg z.im)347    · intro h348      apply Ext.ext349      · have := hs.2 h.2350        exact (re_congr this : (sigma z).re = z.re)351      · show -z.im = z.im352        rw [h.1, neg_zero]353  exact ⟨⟨fun h => ⟨hc.2 (hr.1 h).1, hs.2 (hr.1 h).2⟩, fun h => hr.2 ⟨hc.1 h.1, hs.1 h.2⟩⟩,354    hr.trans ⟨fun h => Ext.ext h.2 h.1, fun h => ⟨im_congr h, re_congr h⟩⟩⟩355356/-- 20:B8 — the energy on the critical line: `N(2⁻¹ + bη) = (2⁻¹)² − νb²`, with `2 · 2⁻¹ = 1`. -/357theorem norm_on_line (F : Frame p κ g) (z : Ext p ν) (hz : z.re = ofNat (2 * κ + 1)) :358    norm z = ofNat (2 * κ + 1) * ofNat (2 * κ + 1) + -(ν * (z.im * z.im)) ∧359    (2 : Shell p) * ofNat (2 * κ + 1) = 1 := by360  refine ⟨?_, (half_inverse F).1⟩361  show z.re * z.re + -(ν * (z.im * z.im)) = _362  rw [hz]363364/-- 20:B6 — the quarter-turn `i = −g^κ`, as the element `i + 0η`, is fixed by conjugation and lies off the365circle: `N(i) = i² = −1 ≠ 1`. -/366theorem quarter_turn_off_circle (F : Frame p κ g) (ν : Shell p) :367    conj (⟨quarterTurn g κ, 0⟩ : Ext p ν) = ⟨quarterTurn g κ, 0⟩ ∧ norm (⟨quarterTurn g κ, 0⟩ : Ext p ν) = -1 ∧368    norm (⟨quarterTurn g κ, 0⟩ : Ext p ν) ≠ 1 := by369  have hn : norm (⟨quarterTurn g κ, 0⟩ : Ext p ν) = -1 := by370    show quarterTurn g κ * quarterTurn g κ + -(ν * (0 * 0)) = -1371    rw [F.quarter_turn_sq, zero_mul, mul_zero, neg_zero, add_zero]372  refine ⟨Ext.ext rfl neg_zero, hn, fun h => ?_⟩373  rw [hn] at h374  exact F.one_ne_zero (F.eq_zero_of_eq_neg h.symm)375376/-- 20:B6 [value] — on `𝔽₁₃(√2)` (`2` a nonsquare mod `13`): the norm-one circle has `13 + 1 = 14` points377among the `169` elements, and Frobenius `z ↦ z^{13}` is conjugation on every element. -/378theorem circle13 :379    natCount (fun k => norm (⟨ofNat (k / 13), ofNat (k % 13)⟩ : Ext 13 2) = 1) 169 = 14 ∧380    (∀ k, k < 169 → (⟨ofNat (k / 13), ofNat (k % 13)⟩ : Ext 13 2) ^ 13 =381      conj ⟨ofNat (k / 13), ofNat (k % 13)⟩) ∧382    (∀ x : Nat, x < 13 → 0 < x → (ofNat x : Shell 13) * ofNat x ≠ 2) := by decide +kernel383384end extension385386/-! ## Frame coincidence below the horizon (20:B2) -/387388section coincidence389390theorem le_mul_self : ∀ H : Nat, H ≤ H * H391  | 0 => Nat.le_refl 0392  | H + 1 => by393    show H + 1 ≤ (H + 1) * H + (H + 1)394    exact Nat.le_add_left (H + 1) ((H + 1) * H)395396/-- 20:B2 — below the horizon the reading is frame-exact: on any shell with `H² < p`, a residue `m ≤ H` is397the integer `m`, and the product of two window residues reads back as the integer product. -/398theorem window_readback {H : Nat} (hH : H * H < p) :399    (∀ m, m ≤ H → (ofNat m : Shell p).val = m) ∧400    ∀ a b, a ≤ H → b ≤ H → (ofNat a * ofNat b : Shell p).val = a * b := by401  have hlt : ∀ m, m ≤ H → m < p := fun m hm =>402    Nat.lt_of_le_of_lt (Nat.le_trans hm (le_mul_self H)) hH403  refine ⟨fun m hm => by rw [val_ofNat, FRC.Nat.mod_eq_of_lt (hlt m hm)], fun a b ha hb => ?_⟩404  rw [ofNat_mul, val_ofNat, FRC.Nat.mod_eq_of_lt (Nat.lt_of_le_of_lt (Nat.mul_le_mul ha hb) hH)]405406/-- 20:B2 — primality equals irreducibility in the window: for `m ≤ H` on a shell with `H² < p`, `m` factors407as `a · b` with `2 ≤ a, b ≤ H` read on the shell exactly when it factors so as an integer. The statement is the408same on every shell above the window — the Subject `𝔽_p` and the Carrier `𝔽_Ω` read the same primes. -/409theorem factorisation_iff {H : Nat} (hH : H * H < p) (m : Nat) (hm : m ≤ H) :410    (∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ a ≤ H ∧ b ≤ H ∧ (ofNat a * ofNat b : Shell p) = ofNat m) ↔411    ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ a * b = m := by412  have hrb := window_readback (p := p) hH413  constructor414  · intro h415    match h with416    | ⟨a, b, ha, hb, haH, hbH, e⟩ =>417      refine ⟨a, b, ha, hb, ?_⟩418      have := val_injective e419      rw [hrb.2 a b haH hbH, hrb.1 m hm] at this420      exact this421  · intro h422    match h with423    | ⟨a, b, ha, hb, e⟩ =>424      have hm' : a * b ≤ H := by rw [e]; exact hm425      have haab : a ≤ a * b := by426        have := Nat.mul_le_mul_left a (Nat.le_trans (Nat.le_succ 1) hb)427        rw [Nat.mul_one] at this; exact this428      have hbab : b ≤ a * b := by429        have := Nat.mul_le_mul_right b (Nat.le_trans (Nat.le_succ 1) ha)430        rw [Nat.one_mul] at this; exact this431      exact ⟨a, b, ha, hb, Nat.le_trans haab hm', Nat.le_trans hbab hm', by rw [ofNat_mul, e]⟩432433/-- 20:B2 — frame coincidence: on the Subject `𝔽_p` and the Carrier `𝔽_Ω`, both above the window `H² < p`,434`H² < Ω`, a window residue factors on one shell exactly when it factors on the other. -/435theorem frame_coincidence {Ω : Nat} [Pos Ω] {H : Nat} (hp : H * H < p) (hΩ : H * H < Ω) (m : Nat) (hm : m ≤ H) :436    (∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ a ≤ H ∧ b ≤ H ∧ (ofNat a * ofNat b : Shell p) = ofNat m) ↔437    (∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ a ≤ H ∧ b ≤ H ∧ (ofNat a * ofNat b : Shell Ω) = ofNat m) :=438  (factorisation_iff hp m hm).trans (factorisation_iff hΩ m hm).symm439440end coincidence441442/-! ## The laboratory pair (20:B1) -/443444/-- 20:B1 [value] — the pair `(13, 233)`: nested, `13² < 233`; both cycles carry the quarter-turn core445(`4 ∣ 12`, `4 ∣ 232`; `5² = −1` on `𝔽₁₃`, `89² = −1` on `𝔽₂₃₃`) and share nothing else (`3 ∤ 232`, so446`gcd(12, 232) = 4`); the Carrier's cycle does not project onto the Subject's (`12 ∤ 232`); the horizon window447`H = 3` is wrap-free on both (`9 < 13`, `9 < 233`). -/448theorem lab_pair :449    13 * 13 < 233 ∧ 12 % 4 = 0 ∧ 232 % 4 = 0 ∧ 232 % 3 ≠ 0 ∧ (5 : Shell 13) * 5 = -1 ∧450    (89 : Shell 233) * 89 = -1 ∧ 232 % 12 ≠ 0 ∧ 3 * 3 < 13 ∧ 3 * 3 < 233 := by decide451452/-! ## The closure of the heights (20:F7, Theorem closure; 13 October 2026) -/453454/-- 20:F7, the foundation clauses of Theorem closure. (i) The wrap of the height reading: a height `T + p` reads as the455residue `T` on the cycle of the shell of cardinality `p`, and the successor reaches every residue of the cycle from `0`456within `p` steps (00:A5, `successor_cycle`). (ii) Finitude: a reading of capacity `Ω` embeds the registered heights in457the shell of `Ω` members (00:A2, `registered_finite`). (iii) Observation: a reading of `o < Ω` states identifies two458residues of the Carrier's cycle, and a reading that identifies none has `Ω ≤ o` (00:A4, `observer_part`,459`complete_needs_whole`). No axioms. -/460theorem closure :461    (∀ {p : Nat} [Pos p] (T : Nat), (ofNat (T + p) : Shell p) = ofNat T) ∧462    (∀ {p : Nat} [Pos p], 2 ≤ p → ∀ y : Shell p, ∃ k, k < p ∧ FRC.Foundation.succIter (0 : Shell p) k = y) ∧463    (∀ {U : Type} (Ω : Nat) [Pos Ω] (ρ : U → Nat), (∀ u, ρ u < Ω) →464      ∃ ι : FRC.Foundation.Registered ρ → Shell Ω, ∀ a b, ι a = ι b → a = b) ∧465    (∀ {Ω o : Nat} [Pos Ω], o < Ω → ∀ ρ : Shell Ω → Nat, (∀ x, ρ x < o) → ∃ x y : Shell Ω, x ≠ y ∧ ρ x = ρ y) ∧466    (∀ {Ω o : Nat} [Pos Ω] (ρ : Shell Ω → Nat), (∀ x, ρ x < o) → (∀ x y, ρ x = ρ y → x = y) → Ω ≤ o) :=467  ⟨fun T => FRC.Shell.Frame.ofNat_add_self T, fun h2 y => (FRC.Foundation.successor_cycle h2).2.2 0 y,468   fun {U} Ω inst ρ hρ => @FRC.Foundation.registered_finite U Ω inst ρ hρ,469   fun ho ρ hρ => FRC.Foundation.observer_part ho ρ hρ,470   fun ρ hρ hinj => FRC.Foundation.complete_needs_whole ρ hρ hinj⟩471472/-- 20:F7, 20:F2, the laboratory instances: for each laboratory Carrier `Ω = 13, 233, 30089, 2408561` (prime, `≡ 1 mod 4`) the473largest embedded Subject `p* = 3, 13, 173, 1549` with `p*² < Ω < p'²`, `p'` the next prime (no prime between), so every474embedded Subject's cycle is shorter than the Carrier's and the Carrier's top cell is read from labels up to `√Ω`, beyond475every embedded window `√p*`. Primality by trial division to the root (`isPrime_of_bounded`), decided by the kernel. -/476theorem closure_lab :477    (3 * 3 < 13 ∧ 13 < 5 * 5 ∧ 13 % 4 = 1 ∧ FRC.Nat.isPrime 3 ∧ FRC.Nat.isPrime 5 ∧ FRC.Nat.isPrime 13 ∧478      ∀ q, q < 5 → 3 < q → ¬ FRC.Nat.isPrime q) ∧479    (13 * 13 < 233 ∧ 233 < 17 * 17 ∧ 233 % 4 = 1 ∧ FRC.Nat.isPrime 13 ∧ FRC.Nat.isPrime 17 ∧ FRC.Nat.isPrime 233 ∧480      ∀ q, q < 17 → 13 < q → ¬ FRC.Nat.isPrime q) ∧481    (173 * 173 < 30089 ∧ 30089 < 179 * 179 ∧ 30089 % 4 = 1 ∧ FRC.Nat.isPrime 173 ∧ FRC.Nat.isPrime 179 ∧482      FRC.Nat.isPrime 30089 ∧ ∀ q, q < 179 → 173 < q → ¬ FRC.Nat.isPrime q) ∧483    (1549 * 1549 < 2408561 ∧ 2408561 < 1553 * 1553 ∧ 2408561 % 4 = 1 ∧ FRC.Nat.isPrime 1549 ∧ FRC.Nat.isPrime 1553 ∧484      FRC.Nat.isPrime 2408561 ∧ ∀ q, q < 1553 → 1549 < q → ¬ FRC.Nat.isPrime q) := by485  refine ⟨⟨by decide, by decide, by decide, by decide +kernel, by decide +kernel, by decide +kernel, by decide +kernel⟩,486    ⟨by decide, by decide, by decide, by decide +kernel, by decide +kernel, ?_, by decide +kernel⟩,487    ⟨by decide, by decide, by decide, ?_, ?_, ?_, by decide +kernel⟩,488    ⟨by decide, by decide, by decide, ?_, ?_, ?_, by decide +kernel⟩⟩489  · exact FRC.Nat.isPrime_of_bounded 233 15 (by decide) (by decide) (by decide +kernel)490  · exact FRC.Nat.isPrime_of_bounded 173 13 (by decide) (by decide) (by decide +kernel)491  · exact FRC.Nat.isPrime_of_bounded 179 13 (by decide) (by decide) (by decide +kernel)492  · exact FRC.Nat.isPrime_of_bounded 30089 173 (by decide) (by decide) (by decide +kernel)493  · exact FRC.Nat.isPrime_of_bounded 1549 39 (by decide) (by decide) (by decide +kernel)494  · exact FRC.Nat.isPrime_of_bounded 1553 39 (by decide) (by decide) (by decide +kernel)495  · exact FRC.Nat.isPrime_of_bounded 2408561 1552 (by decide) (by decide) (by decide +kernel)496497/-! ## The finite negative control (20:D9; 13 October 2026) -/498499/-- 20:D9, the finite negative control: on `𝔽₁₃(√2)` (`η² = 2`, `2` a nonsquare, `2⁻¹ = 7`) the polynomial500`P(X) = ((X − 2)² − 2)((X + 1)² − 2)` has exactly the four roots `2 ± η`, `−1 ± η`, of traces `4, 4, 11, 11` against the501trace-one line's `1` (`Tr z = 1 ⟺ Re z = 7`), its root set closed under conjugation and under the half-turn `X ↦ 1 − X`:502finitude, conjugation and the functional-equation reflection do not force roots onto the line. Decided by the kernel on503all `169` elements. -/504theorem negative_control13 :505    (∀ k, k < 169 →506      ((((⟨ofNat (k / 13), ofNat (k % 13)⟩ : Ext 13 2) + -Ext.ofShell 2) * ((⟨ofNat (k / 13), ofNat (k % 13)⟩ : Ext 13 2) + -Ext.ofShell 2) + -Ext.ofShell 2) *507        (((⟨ofNat (k / 13), ofNat (k % 13)⟩ : Ext 13 2) + Ext.ofShell 1) * ((⟨ofNat (k / 13), ofNat (k % 13)⟩ : Ext 13 2) + Ext.ofShell 1) + -Ext.ofShell 2) = Ext.ofShell 0 ↔508      (k = 2 * 13 + 1 ∨ k = 2 * 13 + 12 ∨ k = 12 * 13 + 1 ∨ k = 12 * 13 + 12))) ∧509    (Ext.trace (⟨2, 1⟩ : Ext 13 2) = 4 ∧ Ext.trace (⟨2, 12⟩ : Ext 13 2) = 4 ∧510      Ext.trace (⟨12, 1⟩ : Ext 13 2) = 11 ∧ Ext.trace (⟨12, 12⟩ : Ext 13 2) = 11) ∧511    (∀ k, k < 169 → (Ext.trace (⟨ofNat (k / 13), ofNat (k % 13)⟩ : Ext 13 2) = 1 ↔ k / 13 = 7)) ∧512    (Ext.conj (⟨2, 1⟩ : Ext 13 2) = ⟨2, 12⟩ ∧ Ext.conj (⟨12, 1⟩ : Ext 13 2) = ⟨12, 12⟩) ∧513    (Ext.ofShell 1 + -(⟨2, 1⟩ : Ext 13 2) = ⟨12, 12⟩ ∧ Ext.ofShell 1 + -(⟨2, 12⟩ : Ext 13 2) = ⟨12, 1⟩) ∧514    (∀ x : Nat, x < 13 → 0 < x → (ofNat x : Shell 13) * ofNat x ≠ 2) := by515  decide +kernel516517518/-! ## The cells of the cycle (20:D5; 13 October 2026): the two finite lemmas of the count identity -/519520section cells521522open FRC.Shell.Frame (sumTo)523524/-- Monotonicity of the finite sum under a pointwise bound. -/525theorem sumTo_le (c n : Nat → Nat) : ∀ m, (∀ y, y < m → c y ≤ n y) → sumTo c m ≤ sumTo n m526  | 0, _ => Nat.le_refl _527  | m + 1, h => Nat.add_le_add (sumTo_le c n m fun y hy => h y (Nat.lt_succ_of_lt hy)) (h m (Nat.lt_succ_self m))528529/-- 20:D5, the cells: with `c y ≤ n y` on every cell `y < m` (the on-line count of the cell against its count), every530cell is clean, `c y = n y`, exactly when the two sums over the cycle agree — a sum of non-negative differences vanishes531only term by term. -/532theorem cells_clean_iff_cycle (c n : Nat → Nat) : ∀ m, (∀ y, y < m → c y ≤ n y) →533    ((∀ y, y < m → c y = n y) ↔ sumTo c m = sumTo n m)534  | 0, _ => ⟨fun _ => rfl, fun _ y hy => absurd hy (Nat.not_lt_zero y)⟩535  | m + 1, h =>536    have ih := cells_clean_iff_cycle c n m fun y hy => h y (Nat.lt_succ_of_lt hy)537    ⟨fun hall => by538      show sumTo c m + c m = sumTo n m + n m539      rw [ih.1 (fun y hy => hall y (Nat.lt_succ_of_lt hy)), hall m (Nat.lt_succ_self m)],540     fun hsum y hy =>541      have hs : sumTo c m + c m = sumTo n m + n m := hsum542      have h1 := sumTo_le c n m fun y hy => h y (Nat.lt_succ_of_lt hy)543      have h2 := h m (Nat.lt_succ_self m)544      have hm : c m = n m := match Nat.lt_or_ge (c m) (n m) with545        | .inl hlt => absurd hs (Nat.ne_of_lt (Nat.add_lt_add_of_le_of_lt h1 hlt))546        | .inr hge => Nat.le_antisymm h2 hge547      have hr : sumTo c m = sumTo n m := Nat.add_right_cancel (hm ▸ hs)548      match Nat.lt_or_ge y m with549      | .inl hlt => ih.2 hr y hlt550      | .inr hge => (Nat.le_antisymm (Nat.le_of_lt_succ hy) hge) ▸ hm⟩551552/-- 20:D5, the cells: the number of points of a finite list that the involution fixes (`fixed z = true`). -/553def fixedCount {α : Type} (fixed : α → Bool) : List α → Nat554  | [] => 0555  | a :: l => fixedCount fixed l + (match fixed a with | true => 1 | false => 0)556557theorem fixedCount_le {α : Type} (fixed : α → Bool) : ∀ l : List α, fixedCount fixed l ≤ l.length558  | [] => Nat.le_refl 0559  | a :: l => by560    show fixedCount fixed l + (match fixed a with | true => 1 | false => 0) ≤ l.length + 1561    cases fixed a with562    | true => exact Nat.add_le_add (fixedCount_le fixed l) (Nat.le_refl 1)563    | false => exact Nat.add_le_add (fixedCount_le fixed l) (Nat.zero_le 1)564565/-- 20:D5, the cells: a finite list of points with an involution (the reflection `s ↦ 1 − s̄`, say) has every point566fixed exactly when the count of fixed points equals the count. -/567theorem clean_iff_count {α : Type} (fixed : α → Bool) : ∀ l : List α,568    ((∀ z, z ∈ l → fixed z = true) ↔ fixedCount fixed l = l.length)569  | [] => ⟨fun _ => rfl, fun _ z hz => nomatch hz⟩570  | a :: l =>571    have ih := clean_iff_count fixed l572    ⟨fun hall => by573      have ha : fixed a = true := hall a (List.Mem.head l)574      show fixedCount fixed l + (match fixed a with | true => 1 | false => 0) = l.length + 1575      rw [ha, ih.1 fun z hz => hall z (List.Mem.tail a hz)],576     fun hlen z hz => by577      have hle := fixedCount_le fixed l578      have hlen' : fixedCount fixed l + (match fixed a with | true => 1 | false => 0) = l.length + 1 := hlen579      cases hfa : fixed a with580      | true =>581        rw [hfa] at hlen'582        have := ih.2 (Nat.succ.inj hlen')583        cases hz with584        | head => exact hfa585        | tail _ hz' => exact this z hz'586      | false =>587        rw [hfa] at hlen'588        have h0 : fixedCount fixed l = l.length + 1 := hlen'589        exact absurd (h0 ▸ hle) (Nat.not_succ_le_self _)⟩590591end cells592593/-! ## Turing's count on the shell (20:F1; 15 October 2026): the chain `C_y ≤ N^crit_y ≤ N_y`, the certificate at594equality, and the phantom -/595596section turing597598/-- 20:F1, Turing's count: `fixedCount` is monotone in the predicate — when every certified sign change of the list599is a point of the line (`sc z = true → onLine z = true`), the certified count is at most the on-line count. -/600theorem fixedCount_mono {α : Type} (sc onLine : α → Bool) : ∀ l : List α,601    (∀ z, z ∈ l → sc z = true → onLine z = true) → fixedCount sc l ≤ fixedCount onLine l602  | [], _ => Nat.le_refl 0603  | a :: l, h => by604    show fixedCount sc l + (match sc a with | true => 1 | false => 0) ≤605      fixedCount onLine l + (match onLine a with | true => 1 | false => 0)606    have ih := fixedCount_mono sc onLine l fun z hz => h z (List.Mem.tail a hz)607    cases hsa : sc a with608    | true =>609      rw [h a (List.Mem.head l) hsa]610      exact Nat.add_le_add ih (Nat.le_refl 1)611    | false => exact Nat.add_le_add ih (Nat.zero_le _)612613/-- 20:F1, the chain `C_y ≤ N^crit_y ≤ N_y`: on the finite list of a cell's zeros, the certified sign changes (each a614point of the line) count at most the on-line zeros, which count at most the zeros. -/615theorem turing_chain {α : Type} (sc onLine : α → Bool) (l : List α)616    (h : ∀ z, z ∈ l → sc z = true → onLine z = true) :617    fixedCount sc l ≤ fixedCount onLine l ∧ fixedCount onLine l ≤ l.length :=618  ⟨fixedCount_mono sc onLine l h, fixedCount_le onLine l⟩619620/-- 20:F1, the certificate: when the certified count reaches the count of the cell, every zero of the cell lies on621the line and is certified (simple, as a sign change). -/622theorem turing_equal {α : Type} (sc onLine : α → Bool) (l : List α)623    (h : ∀ z, z ∈ l → sc z = true → onLine z = true) (hc : fixedCount sc l = l.length) :624    ∀ z, z ∈ l → onLine z = true ∧ sc z = true := by625  have hsc := (clean_iff_count sc l).2 hc626  intro z hz627  exact ⟨h z hz (hsc z hz), hsc z hz⟩628629/-- 20:F1, the phantom: a zero off the line makes the on-line count fall short of the count, `N_y − N^crit_y > 0`. -/630theorem turing_phantom {α : Type} (onLine : α → Bool) (l : List α) (hz : ∃ z, z ∈ l ∧ onLine z = false) :631    fixedCount onLine l < l.length :=632  match Nat.lt_or_ge (fixedCount onLine l) l.length with633  | .inl hlt => hlt634  | .inr hge =>635    have heq : fixedCount onLine l = l.length := Nat.le_antisymm (fixedCount_le onLine l) hge636    have hall := (clean_iff_count onLine l).2 heq637    match hz with638    | ⟨z, hzl, hzf⟩ => absurd (hall z hzl) (by rw [hzf]; exact Bool.false_ne_true)639640end turing641642end FRC.Horizon643