pith. machine review for the scientific record. sign in
def definition def or abbrev high

F_12

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 291def F_12 : ℕ := 144

proof body

Definition body.

 292

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.