D_8_fails
plain-language theorem explainer
The theorem shows that 256 is not a Fibonacci number. Researchers deriving the coherence energy exponent from the Fibonacci constraint on spatial dimension would cite this to exclude D=8. The proof is a direct Boolean evaluation of the membership predicate for the enumerated Fibonacci list.
Claim. The integer 256 does not belong to the set of Fibonacci numbers used to enforce the dimension constraint.
background
The module derives the coherence exponent from the requirement that both spatial dimension D and octave period 2^D must be Fibonacci numbers. D is defined as 3 from the dimension forcing chain. The predicate checks membership in the explicit list of small Fibonacci numbers up to 1597. Upstream results include the identity event at J-cost minimum and the primitive distinction axioms that lead into the forcing chain.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the Boolean membership test 256 in the enumerated Fibonacci list, returning false.
why it matters
This result supports the main theorem that the coherence exponent is uniquely 5 via the Fibonacci identity F6 - F4 = F5. It closes the D=8 case in the eight-tick octave and D=3 selection from the forcing chain (T7-T8). It feeds the parent claim that E_coh = phi^{-5} is structurally determined by the Fibonacci-phi framework rather than a free parameter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.