def
definition
F_12
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Gravity.GravityParameters on GitHub at line 291.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
288
289/-- F_12 is the unique non-trivial Fibonacci-square.
290 F_12 = 144 = 12² is both a Fibonacci number and a perfect square. -/
291def F_12 : ℕ := 144
292
293theorem F_12_is_fibonacci_12 : F_12 = Nat.fib 12 := by native_decide
294
295theorem F_12_is_perfect_square : F_12 = 12 ^ 2 := by native_decide
296
297/-- The conjectured galactic timescale rung.
298 N_τ = F_12 - 2 = 144 - 2 = 142 -/
299def N_tau_conjecture : ℕ := F_12 - 2
300
301theorem N_tau_conjecture_eq_142 : N_tau_conjecture = 142 := by native_decide
302
303/-- The 16-rung offset is 2^4 = 4² (second non-trivial perfect square). -/
304def rung_offset : ℕ := 16
305
306theorem rung_offset_is_power_of_2 : rung_offset = 2 ^ 4 := by native_decide
307
308theorem rung_offset_is_perfect_square : rung_offset = 4 ^ 2 := by native_decide
309
310theorem rung_offset_is_two_8tick_cycles : rung_offset = 2 * 8 := by native_decide
311
312/-- The conjectured galactic radius rung.
313 N_r = N_τ - 16 = 142 - 16 = 126 -/
314def N_r_conjecture : ℕ := N_tau_conjecture - rung_offset
315
316theorem N_r_conjecture_eq_126 : N_r_conjecture = 126 := by native_decide
317
318/-- If the conjecture is correct, N_r = N_τ - 16 exactly. -/
319theorem rung_relationship : N_r_conjecture = N_tau_conjecture - rung_offset := rfl
320
321/-! ## Summary