pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Foundation.CoherenceExponentUniqueness

show as:
view Lean formalization →

The CoherenceExponentUniqueness module defines the Fibonacci deficit k_fib(D) = 2^D - D and proves that the coherence exponent equals 5 uniquely at D = 3. Researchers deriving the phi-ladder mass formula or RS-native constants cite it to fix the scaling after the eight-tick octave. The structure consists of auxiliary deficit functions, agreement lemmas at D = 3, disagreement lemmas at neighboring integers, and a final uniqueness statement.

claimThe Fibonacci deficit is given by $k(D) = 2^D - D$. The coherence exponent is the unique value equal to 5 at spatial dimension 3, with the integer counterpart agreeing only at that point and disagreeing at D = 1, 2, 4.

background

This module belongs to the Foundation layer and supplies the uniqueness step after the forcing chain reaches the eight-tick octave and three spatial dimensions. It introduces the Fibonacci deficit k_fib(D) = 2^D - D as a measure of deviation from self-similarity between exponential base-2 growth and the linear term D. Companion definitions include the integer deficit k_int together with coherenceExponent and einsteinKappaExponent, all placed in the context of the Recognition Composition Law and J-uniqueness.

proof idea

The module first declares the two deficit functions. It then proves agreement at D = 3 by direct substitution, showing both versions equal 5. Separate lemmas establish explicit mismatch at D = 1, 2 and 4. The uniqueness result coherenceExponent_eq_5 is obtained by combining the single agreement point with the surrounding disagreements; k5_forced_at_D3 is an immediate corollary.

why it matters in Recognition Science

The module fixes the coherence exponent at 5, which is required for the mass formula yardstick times phi to the power (rung minus 8 plus gap(Z)) and for the constants G = phi^5 / pi together with hbar = phi^{-5}. It supplies the input to einsteinKappaExponent and supports the alpha inverse interval (137.030, 137.039). The result closes the T7 octave and T8 dimension steps in the forcing chain.

scope and limits

declarations in this module (16)