k_fib
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.