pith. machine review for the scientific record. sign in
def definition def or abbrev high

coherence_exponent

show as:
view Lean formalization →

The coherence exponent is the integer difference between the octave period 2^D and the spatial dimension D. Researchers deriving particle masses from the Recognition Science phi-ladder cite this definition to obtain the exponent -5 for the coherence energy. It is introduced as a direct subtraction of the two upstream constants that encode the Fibonacci constraint.

claimLet $D=3$ denote the forced spatial dimension and let the octave be the period $2^D$. The coherence exponent is defined to be the natural number $2^D - D$.

background

In the Coherence Exponent module the spatial dimension D is fixed at 3 by the T8 forcing step of the Unified Forcing Chain. The octave is defined as 2 raised to D, yielding 8, which is the eighth tick in the eight-tick octave period. This setup encodes the Fibonacci constraint that both D and 2^D must be Fibonacci numbers, selecting D=3 uniquely as F_4 with 2^D = F_6.

proof idea

The definition is a direct subtraction coherence_exponent := octave - D. It inherits the numerical value 5 from the upstream definitions of octave as 2^D and D as 3, which are verified by norm_num in the dependent theorems.

why it matters in Recognition Science

This definition supplies the exponent 5 that appears in the coherence energy E_coh = phi^{-5}. It is used by the uniqueness theorem coherence_exponent_unique and by the electron mass definitions to fix the mass scale on the phi-ladder. The result closes the derivation that the coherence energy is structurally determined by the Fibonacci-phi framework rather than chosen freely, consistent with the T7 eight-tick octave and T8 dimension forcing.

scope and limits

formal statement (Lean)

  75def coherence_exponent : ℕ := octave - D

proof body

Definition body.

  76
  77/-- The coherence exponent equals 5 -/

used by (9)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.