is_fibonacci
plain-language theorem explainer
The definition supplies a Boolean predicate that returns true exactly when its natural-number argument equals one of the first seventeen Fibonacci numbers. Researchers deriving the coherence exponent in Recognition Science cite it to enforce the simultaneous Fibonacci condition on dimension D and 2^D. The implementation consists of a direct membership test against the enumerated sequence.
Claim. The predicate that returns true if and only if its natural-number input belongs to the finite initial segment of the Fibonacci sequence given by the numbers 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987, 1597.
background
The module derives the coherence exponent from the Fibonacci constraint that both the spatial dimension D and 2^D must belong to the Fibonacci sequence. This definition implements the membership test used to check that constraint for candidate values of D. The local theoretical setting is the proof that the coherence energy exponent equals -5 because D = 3 = F_4 and 2^D = 8 = F_6 force the difference 5 = F_5.
proof idea
The definition is realized by a direct membership check of the input natural number against a hardcoded list of the first seventeen Fibonacci numbers. No lemmas are applied; the body performs the enumeration test natively.
why it matters
This predicate is invoked by the theorems D_3_fibonacci_constraint, D_1_fibonacci_constraint and the failure statements for D = 2, 5, 8. It thereby supports the main theorem that the coherence exponent is uniquely 5. In the framework this fills the eight-tick octave step with period 2^3, selects D = 3, and fixes the coherence energy as φ^{-5} on the phi-ladder without free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.