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

coherenceExponent

show as:
view Lean formalization →

The coherence exponent k is fixed at the natural number 5 to set the RS-native Planck constant ħ = φ^{-5}. Derivations of fundamental constants from the forcing chain at D=3 cite this pinning to obtain G = φ^5/π and κ = 8φ^5. The declaration is a direct constant assignment that propagates algebraically through uniqueness and positivity results.

claimThe coherence exponent equals the natural number 5, so that ħ = φ^{-5} in RS-native units.

background

The module derives the Planck constant from Recognition Science by pinning the coherence exponent k at D=3. Module documentation states that k=5 follows from the Fibonacci route k_fib(D)=2^D - D =5 and the integration route k_int(D)=D+2=5. Upstream definitions include ħ = E_coh · τ₀ = φ^{-5} · 1 from Constants and the uniqueness result that forces this exponent from the J-cost functional equation.

proof idea

The declaration is a direct definition assigning the natural number 5. It is referenced by the reflexivity theorem coherenceExponent_eq_5 and supplies the exponent for the algebraic definitions of hbar_RS and G_RS.

why it matters in Recognition Science

This definition supplies the exponent required by the parent results in CoherenceExponentUniqueness and the derivations of hbar_RS, G_RS, and kappa_RS. It fills the forcing-chain step where the eight-tick octave and D=3 determine k=5, as stated in the module documentation. The pinning closes the algebraic path to the RS-native constants with zero sorry statements.

scope and limits

formal statement (Lean)

  29def coherenceExponent : ℕ := 5

proof body

Definition body.

  30
  31/-- hbar = φ^(-5) in RS units. -/

used by (9)

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

depends on (5)

Lean names referenced from this declaration's body.