k_fib
k_fib supplies the Fibonacci deficit route 2^D - D to the coherence exponent. It is cited in uniqueness arguments that compare it against the integration measure to isolate D=3. The definition is a direct arithmetic expression that downstream theorems evaluate at fixed natural numbers.
claimThe Fibonacci deficit function is given by $k_{fib}(D) = 2^D - D$ for natural number $D$.
background
The module compares two routes that both yield the coherence exponent value 5, but agree only when the spatial dimension is 3. The Fibonacci deficit is introduced as k_fib(D) = 2^D - D, which equals the fifth Fibonacci number at D=3. The upstream integration measure is defined by k_int(D) = D + 2, which also equals 5 at D=3. Upstream doc-comment states: 'Integration measure: k_int(D) = D + 2.'
proof idea
Direct definition of the arithmetic expression 2^D - D. Downstream theorems invoke it through the decide tactic at concrete values D=1,2,3,4.
why it matters in Recognition Science
It supplies the first of the two independent routes that force the coherence exponent to 5 uniquely at D=3. The definition feeds agreement_at_3, both_equal_5_at_3, disagreement_at_1/2/4, and the CoherenceExponentCert structure, all of which support the master theorem exponent_unique_at_D3. This matches the framework requirement that D=3 is the unique dimension where the routes coincide.
scope and limits
- Does not prove agreement or disagreement between the two routes.
- Does not extend the expression beyond natural numbers D.
- Does not incorporate the J-cost or Recognition Composition Law.
- Does not derive mass formulas or physical constants.
formal statement (Lean)
37def k_fib (D : ℕ) : ℕ := 2^D - D
proof body
Definition body.
38
39/-- Integration measure: k_int(D) = D + 2. -/