both_equal_5_at_3
plain-language theorem explainer
The declaration shows that the Fibonacci deficit and integration measure routes both yield coherence exponent 5 precisely when the spatial dimension is 3. Researchers tracing the Recognition Science forcing chain would cite this result when confirming that only D=3 satisfies the dual constraints on the exponent. The proof is a direct computation via the decide tactic on the explicit definitions of the two expressions.
Claim. Let $k_{fib}(D) := 2^D - D$ and $k_{int}(D) := D + 2$. Then $k_{fib}(3) = 5$ and $k_{int}(3) = 5$.
background
In the Coherence Exponent Uniqueness module, two independent expressions are defined for the coherence exponent k. The Fibonacci deficit route sets k_fib(D) = 2^D - D, which at D=3 yields 5, matching the fifth Fibonacci number. The integration measure route sets k_int(D) = D + 2, which also equals 5 at D=3.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to verify the equality after substituting the explicit definitions of k_fib and k_int at the natural number 3.
why it matters
This result supplies the agreement clause in the coherenceExponentCert certificate, which collects the agreements and disagreements to certify that k=5 is forced uniquely at D=3. It directly supports the master theorem exponent_unique_at_D3 in the module. Within the Recognition Science framework, it confirms the eight-tick octave and D=3 spatial dimensions by showing the exponent matches the required value only in three dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.