F_12_is_fibonacci_12
plain-language theorem explainer
F_12 equals the twelfth Fibonacci number, where F_12 is fixed at 144 as the unique non-trivial Fibonacci square in the gravity parameters. Researchers deriving galactic constants from the phi-ladder in Recognition Science reference this identity to connect Fibonacci properties to gravitational formulas. The proof evaluates both sides by direct computation.
Claim. Let $F_{12}$ denote the constant 144. Then $F_{12}$ equals the twelfth term of the Fibonacci sequence defined by the recurrence $F_0 = 0$, $F_1 = 1$, $F_n = F_{n-1} + F_{n-2}$ for $n > 1$.
background
The GravityParameters module derives phenomenological galactic gravity parameters from Recognition Science using the golden ratio φ, classifying each as derived, RS-basis, or phenomenological. F_12 is defined locally as the unique non-trivial Fibonacci square with value 144. Upstream Fibonacci definitions appear in Gap45.Derivation (recurrence starting at 1,1), ContinuedFractionPhi (starting at 0,1), and ZeckendorfJCost (abbreviating Nat.fib), all supplying the standard additive recurrence used here.
proof idea
One-line wrapper that applies the native_decide tactic to evaluate the concrete natural numbers 144 and Nat.fib 12 directly.
why it matters
The result anchors the Fibonacci-square property inside the gravity parameters module, supporting downstream links between Fibonacci numbers and phi-ladder constants such as α_gravity. It aligns with Recognition Science landmarks that employ Fibonacci sequences for J-cost and Zeckendorf representations. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.