F_12_is_perfect_square
plain-language theorem explainer
F_12 equals 144 and therefore 12 squared, the unique non-trivial Fibonacci square. Galactic gravity modelers cite the identity when fixing the timescale rung N_τ = F_12 - 2. The proof is a one-line native_decide that verifies the arithmetic equality from the constant definition.
Claim. Let $F_{12}$ denote the unique non-trivial Fibonacci number that is also a perfect square. Then $F_{12} = 12^{2}$.
background
The GravityParameters module classifies galactic gravity parameters by their derivation status from the golden ratio φ. F_12 is introduced as the basis for the conjectured galactic timescale rung N_τ = F_12 - 2. The module distinguishes derived quantities (such as α = 1 - 1/φ) from those with RS basis or phenomenological status, and records a0_phi_ladder_formula as a proven theorem.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the equality F_12 = 12^2. No additional lemmas are invoked; the tactic evaluates the definition of F_12 as the constant 144 directly.
why it matters
The identity anchors the galactic timescale parameter N_τ = 142 inside the Recognition Science gravity model. It supplies a concrete numerical link to the phi-ladder used for mass formulas and to the eight-tick octave structure. The result supports downstream derivations of a0 and r0 via the relation τ★ = √(2π r0 / a0).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.