IndisputableMonolith.Foundation.CoherenceExponentUniqueness
The module defines the Fibonacci deficit k_fib(D) = 2^D - D and establishes uniqueness of the coherence exponent at D = 3 with value 5. Researchers deriving the eight-tick octave and spatial dimensions from the forcing chain would cite these lemmas. The argument consists of direct evaluations at small integers plus case checks for agreement and disagreement.
claim$k_{\rm fib}(D) := 2^D - D$. The coherence exponent equals 5 at $D=3$ and is unique there; $k_{\rm int}$ and related predicates confirm agreement only at this point.
background
The module sits in the Foundation layer and introduces the Fibonacci deficit to quantify deviation from pure dyadic scaling. It defines k_fib together with integer comparison functions and a collection of small-D lemmas (agreement_at_3, disagreement_at_1, disagreement_at_2, disagreement_at_4, both_equal_5_at_3). These support the coherenceExponent and einsteinKappaExponent declarations that appear as siblings.
proof idea
This is a definition module with supporting lemmas. The results are obtained by direct computation of k_fib at D = 1,2,3,4 followed by exhaustive case verification that only D = 3 yields the integer value 5.
why it matters in Recognition Science
The module supplies the uniqueness step required for T7 (eight-tick octave) and T8 (D = 3) in the forcing chain. It feeds the parent declarations coherenceExponent_eq_5 and einsteinKappaExponent, closing the exponent choice before higher-dimensional or mass-ladder results are invoked.
scope and limits
- Does not derive k_fib from the J-cost or RCL.
- Does not treat D outside {1,2,3,4}.
- Does not connect the exponent to the phi-ladder or alpha band.
- Does not address continuous D or non-integer cases.
declarations in this module (16)
-
def
k_fib -
def
k_int -
theorem
agreement_at_3 -
theorem
both_equal_5_at_3 -
theorem
disagreement_at_1 -
theorem
disagreement_at_2 -
theorem
disagreement_at_4 -
theorem
exponent_unique_at_D3 -
theorem
k5_forced_at_D3 -
def
coherenceExponent -
theorem
coherenceExponent_eq_5 -
def
einsteinKappaExponent -
def
einsteinKappaPeriod -
theorem
kappa_eq_8phi5 -
structure
CoherenceExponentCert -
def
coherenceExponentCert