Pith. sign in
module module high

IndisputableMonolith.Physics.PlanckConstantFromRS

show as:
view Lean formalization →

The module Physics.PlanckConstantFromRS fixes the coherence exponent at k=5 to produce explicit RS-native expressions for ħ and G. Physicists tracing constants from the J-function and phi-ladder cite these definitions when converting between RS units and laboratory values. The module is a short sequence of definitions and positivity statements that import the time quantum τ₀ from Constants and specialize the scaling.

claimThe module sets the coherence exponent $k=5$, yielding $\hbar_{RS}=\phi^{-5}$, $G_{RS}=\phi^5/\pi$, and the Einstein relation in RS-native units with $c=1$ and $\tau_0=1$.

background

Recognition Science obtains all constants from the J-cost functional equation and the self-similar fixed point phi. The upstream Constants module supplies the base time quantum $\tau_0=1$ tick. This module specializes the coherence exponent to the integer value 5, which places ħ on the phi-ladder at rung -5 and G at rung +5, consistent with the eight-tick octave and D=3 geometry.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the explicit constants ħ_RS and G_RS that enter the mass formula yardstick * phi^(rung-8+gap(Z)) and the alpha band (137.030,137.039). It realizes the T5 J-uniqueness step by fixing k=5, providing the numerical anchors used in downstream derivations of physical relations such as the Einstein relation.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)