F_12
plain-language theorem explainer
F_12 assigns the integer 144, the unique non-trivial Fibonacci number that is also a perfect square. Workers on the phi-ladder model for galactic acceleration parameters cite this constant when fixing the conjectured timescale rung N_tau. The declaration is a direct definition with no further computation.
Claim. Let $F_{12}$ denote the natural number 144, which equals both the twelfth Fibonacci number and twelve squared.
background
The GravityParameters module derives galactic gravity parameters from the golden ratio phi in Recognition Science. It distinguishes derived quantities (such as alpha = 1 - 1/phi) from those with RS basis or phenomenological status, and lists a0 as linked to the phi-ladder via the theorem a0_phi_ladder_formula. F_12 supplies the numerical anchor for the conjectured galactic timescale rung N_tau = F_12 - 2.
proof idea
This is a direct definition that assigns the constant 144 to F_12 with no lemmas or tactics applied.
why it matters
The definition feeds the downstream theorems a0_phi_ladder_formula, N_tau_conjecture, rung_relationship, and F_12_is_fibonacci_12. It supplies the Fibonacci-square value required for the phi-ladder formula a0 = 2 pi c / tau0 * phi^(N_r - 2 N_tau) and the conjecture N_tau = 142. It touches the open question of whether the galactic timescale rung is exactly F_12 - 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.