D_5_fails
plain-language theorem explainer
The declaration shows that 32 fails the Fibonacci membership test, excluding dimension 5 from the coherence selection process in Recognition Science. Workers deriving the phi-ladder mass formula or the coherence energy exponent would cite this to rule out candidate D values before invoking the main uniqueness result. The proof is a one-line native decision that evaluates the enumerated list membership directly.
Claim. $2^5 = 32$ does not belong to the Fibonacci sequence.
background
The module derives the coherence energy exponent from the requirement that both the spatial dimension D and 2^D must be Fibonacci numbers. D is defined as the constant 3, the unique value satisfying the constraint together with 2^D = 8. The predicate is_fibonacci(n) returns true precisely when n appears in the explicit list of small Fibonacci numbers [1,1,2,3,5,8,13,...]. Upstream results supply the collision-free and simplicial ledger structures that embed this dimension choice into the broader forcing chain from T0 to T8.
proof idea
The proof is a one-line wrapper that applies native_decide to the Boolean membership test for 32 against the enumerated Fibonacci list.
why it matters
This result closes one branch of the case analysis that forces D = 3 and thereby fixes the coherence exponent at phi^{-5}, as stated in the module's main theorem. It directly supports the claim that E_coh is structurally determined rather than free, consistent with the eight-tick octave and the phi-ladder mass formula. No downstream uses are recorded yet, but the sibling coherence_exponent_eq_5 depends on the same Fibonacci constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.