D_1_fibonacci_constraint
plain-language theorem explainer
The declaration verifies that dimension value 1 satisfies the Fibonacci constraint since both 1 and 2^1 belong to the enumerated Fibonacci sequence, though the case is marked degenerate. Researchers tracing dimensional selection in Recognition Science would cite it as a boundary check before the uniqueness argument for D=3. The proof is a direct term-mode wrapper that splits the conjunction and applies native decision to confirm list membership.
Claim. Let $f(n)$ be the predicate that the natural number $n$ belongs to the Fibonacci sequence. Then $f(1) land f(2)$.
background
The is_fibonacci predicate is defined by direct enumeration: it returns true precisely when its argument appears in the list [1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987, 1597]. The module derives the coherence energy exponent from the requirement that both the spatial dimension D and its octave 2^D must be Fibonacci numbers. The module documentation states that this constraint 'uniquely selects D = 3' and yields E_coh = φ^{-5} via the identity 8 - 3 = 5. Upstream results supply the is_fibonacci definition and the T8 dimension forcing that fixes D = 3 in the non-degenerate case.
proof idea
The proof is a one-line term wrapper. Constructor splits the conjunction into two goals; native_decide then evaluates each boolean membership test against the enumerated Fibonacci list.
why it matters
This boundary case anchors the main theorem of the module: the Fibonacci constraint on D and 2^D forces D = 3 = F_4 with 2^D = 8 = F_6, so the difference is F_5 and the coherence exponent is fixed at φ^{-5}. It illustrates the degenerate status of D = 1 before the uniqueness step that connects to T8 dimension forcing and the Recognition Composition Law. The result therefore supplies the negative instance needed to isolate the physically realized dimension in the coherence-exponent derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.