is_fibonacci
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not verify the Fibonacci recurrence for the enumerated terms.
- Does not extend the check to Fibonacci numbers larger than 1597.
- Does not prove that D = 3 is the unique solution to the constraint.
- Does not connect to J-uniqueness or the Recognition Composition Law.
Lean usage
theorem D_3_fibonacci_constraint : is_fibonacci 3 ∧ is_fibonacci (2 ^ 3) := by constructor <;> native_decideformal statement (Lean)
94def is_fibonacci (n : ℕ) : Bool :=
proof body
Definition body.
95 n ∈ [1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987, 1597]
96
97/-- D = 1 satisfies the Fibonacci constraint but is degenerate -/