pith. machine review for the scientific record. sign in
theorem proved term proof high

coherenceExponent_eq_5

show as:
view Lean formalization →

The coherence exponent is fixed at 5 in Recognition Science native units to enforce ħ = φ^{-5}. Researchers normalizing Planck-scale constants or phi-ladder masses cite this value when working in RS units. The equality follows immediately by reflexivity from the definition coherenceExponent := 5.

claimIn RS-native units the coherence exponent satisfies $k=5$, so that $ħ=φ^{-5}$.

background

The module CoherenceExponentUniqueness records that two routes force the exponent k only at D=3: the Fibonacci deficit route gives k_fib(D)=2^D - D while the integration measure gives k_int(D)=D+2. These routes agree solely at D=3, both yielding 5. The definition coherenceExponent : ℕ := 5 encodes this forced value, with the Planck constant following as ħ = φ^{-5}. Upstream constants supply the fundamental tick τ₀ = 1 and the period function period(k) = φ^k.

proof idea

The proof is a one-line reflexivity that matches the declared value 5 in the definition of coherenceExponent.

why it matters in Recognition Science

This equality anchors the Planck constant derivation and supports the master uniqueness result exponent_unique_at_D3 that k=5 is forced only at D=3. It aligns with the eight-tick octave (T7) and the forcing chain step that sets the coherence scale. The result closes the agreement table showing disagreement at all other dimensions.

scope and limits

formal statement (Lean)

  68theorem coherenceExponent_eq_5 : coherenceExponent = 5 := rfl

proof body

Term-mode proof.

  69
  70/-- Einstein coupling κ = 8φ^5 in RS units (from k=5 and 8-tick period). -/

depends on (7)

Lean names referenced from this declaration's body.