agreement_at_3
plain-language theorem explainer
The Fibonacci deficit and integration measure expressions for the coherence exponent agree at dimension three. A physicist working on dimension selection within Recognition Science would cite this to confirm that k equals five only when D equals three. The proof is a direct numerical verification via the decide tactic on the unfolded natural-number definitions.
Claim. Let $k_{fib}(D) = 2^D - D$ and $k_{int}(D) = D + 2$. Then $k_{fib}(3) = k_{int}(3)$.
background
The Coherence Exponent Uniqueness module presents two independent routes to the exponent k. The Fibonacci deficit route defines $k_{fib}(D) := 2^D - D$. The integration measure route defines $k_{int}(D) := D + 2$ (from the Beltracchi response to outstanding issues in the module documentation). These expressions are shown to agree only at D = 3, where both evaluate to 5, while disagreeing at D = 1, 2, and 4. The upstream results supplying the definitions are the sibling declarations k_fib and k_int.
proof idea
One-line wrapper that applies the decide tactic to the equality after unfolding k_fib and k_int to explicit natural-number arithmetic.
why it matters
This supplies the agree_at_3 field inside the coherenceExponentCert record, which bundles the agreement and disagreement facts to certify uniqueness of k = 5 at D = 3. It supports the module's master claim exponent_unique_at_D3. In the Recognition Science framework the result confirms T8 (D = 3 spatial dimensions) and the eight-tick octave, since 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.