def
definition
F_12
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
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