hbarL
plain-language theorem explainer
The reduced Planck constant is realized on the recovered real line as the golden-ratio power φ to the minus five. Anyone transporting RS-native constants through LogicReal cites this binding. The body is a one-line composition of the recovered golden ratio with the transported real power map at exponent −5.
Claim. On the recovered real line, set $\hbar_L := \varphi_L^{-5}$, where $\varphi_L$ is the recovered golden ratio and the power is Mathlib real exponentiation transported into the recovered line via $x^y \mapsto \mathrm{fromReal}(\mathrm{toReal}(x)^{\mathrm{toReal}(y)})$.
background
LogicRealConstants mirrors Recognition Science constants on LogicReal, the Cauchy completion of the recovered rationals (a thin wrapper around Mathlib's completed reals via CompareReals). Each constant is written in LogicReal; companion theorems show that transport by toReal recovers the ordinary real constant from IndisputableMonolith.Constants.
The golden ratio on this line is $\varphi_L = (1 + \sqrt{5})/2$ via fromReal and sqrtL. Real powers are rpowL, defined by round-tripping through Mathlib: rpowL x y := fromReal (Real.rpow (toReal x) (toReal y)). fromReal embeds an ordinary real into LogicReal by the inverse comparison equivalence.
In RS-native units the primer fixes $c = 1$ and $\hbar = \varphi^{-5}$. This definition is exactly that identity, written on LogicReal rather than on $\mathbb{R}$.
proof idea
Pure definition, not a proof. The right-hand side applies rpowL to phiL and the embedded ordinary real −5 (fromReal (−(5 : ℝ))). No tactics, no lemmas beyond the upstream defs phiL, rpowL, and fromReal.
why it matters
This is the LogicReal carrier for the RS landmark $\hbar = \varphi^{-5}$. Downstream, toReal_hbarL is the simp lemma that transport recovers Constants.hbar (via Constants.hbar_eq_phi_inv_fifth and toReal_phiL). hbarL_eq_phi_inv_fifth is the reflexivity form of the same identity. hbarL_bounds pushes the ordinary numerical sandwich $0.088 < \hbar < 0.093$ across toReal, so later LogicReal arguments can quote concrete bounds without leaving the recovered line.
Together with siblings (phiL, tickL, gravL, alphaInvL) it populates the RS constant table on the foundation real line used by the forcing chain and verification certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.