disagreement_at_4
plain-language theorem explainer
The theorem shows that the Fibonacci deficit and integration measure routes to the coherence exponent disagree when the dimension is set to 4. Researchers tracing the uniqueness argument for the exponent at D=3 cite this result to close the agreement table. The proof is a one-line decision procedure that evaluates the two explicit arithmetic expressions at 4 and confirms they are unequal.
Claim. Let $k_{fib}(D) = 2^D - D$ and $k_{int}(D) = D + 2$. Then $k_{fib}(4) ≠ k_{int}(4)$.
background
The module establishes that two independent routes force the coherence exponent k=5 and agree only at D=3. Route 1 defines the Fibonacci deficit $k_{fib}(D) = 2^D - D$. Route 2 defines the integration measure $k_{int}(D) = D + 2$. The agreement table in the module doc lists explicit values: at D=1 the routes give 1 and 3; at D=2 they give 2 and 4; at D=3 both give 5; at D=4 they give 12 and 6.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the concrete inequality obtained by substituting D=4 into the two definitions.
why it matters
This result supplies the final disagreement entry required by coherenceExponentCert, which packages agreement_at_3, both_equal_5_at_3, and the three disagreement theorems. The module doc states that D=3 is the unique dimension in {1,2,3,4} where the routes agree, completing the step that forces the exponent to 5 only at D=3 in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.