k_int
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 in Recognition Science
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).
scope and limits
- Does not prove that the two routes agree only at D = 3.
- Does not supply a physical derivation of the integration measure.
- Does not compute numerical values for dimensions outside the arithmetic definition.
- Does not reference the CirclePhaseLift log-derivative bound.
formal statement (Lean)
40def k_int (D : ℕ) : ℕ := D + 2
proof body
Definition body.
41
42/-- k_fib and k_int agree at D = 3. -/