disagreement_at_2
plain-language theorem explainer
disagreement_at_2 shows that the Fibonacci deficit exponent and the integration measure exponent differ at dimension 2. Researchers establishing uniqueness of the coherence exponent k=5 in Recognition Science cite this to confirm agreement occurs only at D=3. The proof is a direct numerical check via the decide tactic on the concrete values of the two functions.
Claim. Let $k(D) = 2^D - D$ be the Fibonacci deficit and $m(D) = D + 2$ the integration measure. Then $k(2) ≠ m(2)$.
background
The module examines two independent routes to the coherence exponent. The Fibonacci deficit route sets k(D) = 2^D - D. The integration measure route sets m(D) = D + 2. Module documentation states these agree only at D=3, with explicit disagreement tabulated for D=1, 2 and 4.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the two functions at D=2 and confirm inequality.
why it matters
This supplies one disagreement witness collected inside coherenceExponentCert, which certifies that the two routes agree exclusively at D=3. It supports the master claim that the coherence exponent is forced to 5 uniquely at D=3, consistent with the eight-tick octave and D=3 spatial dimensions in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.