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

coherenceExponent

show as:
view Lean formalization →

The coherence exponent is fixed at the natural number 5. Researchers deriving ħ and G in Recognition Science units cite this value when expressing the reduced Planck constant as φ to the power of minus five. The declaration is a direct assignment with no lemmas or reduction steps.

claimDefine the coherence exponent by the equation $k = 5$, so that the reduced Planck constant satisfies $ħ = φ^{-5}$ in RS units.

background

The Coherence Exponent Uniqueness module records that two independent routes force the exponent k to equal 5 only when the spatial dimension equals 3. The Fibonacci deficit route defines k_fib(D) = 2^D - D and evaluates to 5 at D = 3. The integration measure route defines k_int(D) = D + 2 and likewise equals 5 at D = 3. Agreement holds solely at D = 3; the other tabulated dimensions disagree.

proof idea

This is a direct definition that assigns the literal natural number 5 to the coherence exponent. No lemmas are invoked and no tactics are applied; the body is the constant numeral itself.

why it matters in Recognition Science

This definition supplies the numerical anchor required by the downstream theorem coherenceExponent_eq_5 and by the constant definitions ħ_RS, G_RS, and kappa_RS in the PlanckConstantFromRS module. It closes the uniqueness argument at D = 3 stated in the module documentation and aligns with the eight-tick octave (T7) and the forcing of three spatial dimensions (T8). The parent uniqueness result exponent_unique_at_D3 depends on this fixed value.

scope and limits

formal statement (Lean)

  67def coherenceExponent : ℕ := 5

used by (9)

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

depends on (1)

Lean names referenced from this declaration's body.