D_2_fails
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.