k_int
plain-language theorem explainer
The definition supplies the integration measure route to the coherence exponent by setting k_int(D) to D plus 2. Researchers working on the uniqueness of the exponent value 5 at three spatial dimensions cite this definition together with the Fibonacci deficit function k_fib. The declaration is a direct arithmetic definition requiring no lemmas or computation steps.
Claim. $k(D) = D + 2$ for natural-number dimension $D$, where $k$ denotes the integration measure in the coherence-exponent comparison.
background
The Coherence Exponent Uniqueness module compares two routes that both yield the value 5 only at dimension 3. The Fibonacci deficit route is given by the sibling definition k_fib(D) = 2^D - D. The integration measure is the companion definition k_int(D) = D + 2. The module records that the two expressions agree solely at D = 3 and disagree at D = 1, 2, and 4.
proof idea
The declaration is a direct definition implementing the arithmetic expression D + 2. No lemmas are invoked; the body is the literal expression that downstream equality checks such as agreement_at_3 apply by decide.
why it matters
This definition supplies the second independent route in the argument that the coherence exponent equals 5 uniquely at D = 3. It is used by agreement_at_3, both_equal_5_at_3, the CoherenceExponentCert structure, and the master theorem exponent_unique_at_D3. In the Recognition Science framework the construction aligns with the forcing of three spatial dimensions (T8) and the eight-tick octave (T7).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.