disagreement_at_1
plain-language theorem explainer
disagreement_at_1 establishes that the Fibonacci deficit route and integration measure route to the coherence exponent yield unequal values at dimension 1. Researchers tracing dimensional uniqueness in Recognition Science cite it to complete the agreement table showing coincidence only at D=3. The proof is a one-line wrapper that invokes the decide tactic on the explicit definitions.
Claim. $k_1(1) = 2^1 - 1 = 1$ and $k_2(1) = 1 + 2 = 3$, hence $k_1(1) ≠ k_2(1)$, where $k_1(D) := 2^D - D$ and $k_2(D) := D + 2$.
background
The Coherence Exponent Uniqueness module examines two independent routes that both force the coherence exponent to equal 5. The Fibonacci deficit route is defined by $k_1(D) = 2^D - D$. The integration measure route is defined by $k_2(D) = D + 2$. The module documentation states that these routes agree only at D=3, with explicit values listed for D=1,2,3,4.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic evaluates the concrete natural-number expressions from the definitions of k_fib and k_int at argument 1 and confirms the resulting inequality holds.
why it matters
This result supplies the D=1 disagreement entry inside coherenceExponentCert, the structure that certifies uniqueness of the exponent at D=3. It completes the table from the module documentation and thereby supports the claim that D=3 is the sole dimension of agreement, consistent with the eight-tick octave and the forcing of D=3 in the unified chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.