k5_forced_at_D3
plain-language theorem explainer
The declaration shows that the Fibonacci deficit and integration measure both evaluate to 5 at spatial dimension 3 and coincide there. A physicist deriving the coherence exponent from dimension-dependent constraints in Recognition Science would cite this to confirm unique forcing at D=3. The proof is a one-line decision procedure that evaluates the finite arithmetic equalities directly.
Claim. Let $k(D) = 2^D - D$ and $m(D) = D + 2$. Then $k(3) = 5$, $m(3) = 5$, and $k(3) = m(3)$.
background
The module derives uniqueness of the coherence exponent from two independent routes that agree only at D=3. The Fibonacci deficit is defined by $k(D) = 2^D - D$, which yields 5 at D=3. The integration measure is defined by $m(D) = D + 2$, which also yields 5 at D=3. The module document states: 'Two independent routes force k = 5, and they agree ONLY at D = 3.' Upstream definitions supply the explicit formulas for both expressions.
proof idea
The proof is a one-line wrapper that applies the decidable equality checker to the conjunction of the three arithmetic statements.
why it matters
This corollary supplies the agreement fact used by coherenceExponentCert to certify that the exponent equals 5 uniquely at D=3. It fills the uniqueness step in the Beltracchi response and aligns with the framework forcing of D=3 spatial dimensions. The result closes the argument that the coherence exponent is forced to 5 only in three dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.