D_2_fails
Dimension 2 fails the Fibonacci constraint because 4 lies outside the enumerated sequence. Researchers deriving the spatial dimension from the self-similar forcing chain cite this exclusion before fixing D at 3. The proof is a one-line native decision that directly evaluates membership in the Fibonacci list.
claim$2^2 = 4$ is not a Fibonacci number.
background
The module shows that the coherence energy exponent equals -5 once the Fibonacci constraint forces both D and 2^D to be Fibonacci numbers. The predicate is_fibonacci checks membership by direct enumeration of the sequence up to 1597. The definition D fixes the spatial dimension at 3, consistent with the eight-tick octave period.
proof idea
The proof is a one-line wrapper that invokes native_decide on the negated membership test for 4 inside the Fibonacci list.
why it matters in Recognition Science
The result eliminates D=2 and thereby supports the main theorem that the coherence exponent is phi^{-5} via the identity 8-3=5. It fills the T8 dimension-forcing step in the unified chain by confirming that only D=3 satisfies the joint Fibonacci requirement on D and 2^D.
scope and limits
- Does not prove that D=3 satisfies the constraint.
- Does not derive the numerical value of the coherence exponent.
- Does not address dimensions outside the positive integers.
- Does not extend the Fibonacci check beyond the enumerated range.
formal statement (Lean)
102theorem D_2_fails : ¬ is_fibonacci (2^2) := by native_decide
proof body
Term-mode proof.
103
104/-- D = 3 satisfies the Fibonacci constraint -/