hbarL_eq_phi_inv_fifth
plain-language theorem explainer
On the recovered real line, the RS action quantum equals the golden ratio raised to −5. Anyone citing the LogicReal mirror of ℏ = φ⁻⁵ uses this identity. The proof is pure definitional equality (rfl): the constant is defined as that power.
Claim. The recovered action quantum equals the recovered golden ratio raised to the power $-5$: $\hbar_L = \varphi_L^{-5}$, where the power and the embedding of $-5$ are taken in the recovered real line.
background
LogicRealConstants mirrors Recognition Science constants on the recovered real line LogicReal. Each definition is written in that type; companion theorems show that transport via toReal recovers the ordinary real constants from IndisputableMonolith.Constants.
In RS-native units the action quantum is fixed as $\hbar = E_{\mathrm{coh}}\cdot\tau_0 = \varphi^{-5}$. The recovered golden ratio $\varphi_L$ is $(1+\sqrt{5})/2$ built from recovered operations; real powers on LogicReal are the transport of Mathlib Real.rpow through fromReal/toReal. The recovered $\hbar_L$ is defined exactly as that power of $\varphi_L$.
proof idea
One-line term proof by rfl. The declaration of the recovered action quantum is literally rpowL phiL (fromReal (-5)), so equality to that expression is definitional and needs no lemmas beyond unfolding.
why it matters
Closes the recovered-side identity that matches the RS-native convention $\hbar = \varphi^{-5}$ (primer constants; cf. the Constants file note that hbar_eq_phi_inv_fifth is intentional definitional closure of the RS action unit, not a CODATA claim). It anchors the LogicReal mirror of the action quantum beside the other recovered constants ($\varphi_L$, tick, octave, $E_{\mathrm{coh}}$, $G$, $\alpha^{-1}$). No downstream users are wired yet; the natural consumers are transport lemmas that send $\hbar_L$ to the real $\hbar$ and any LogicReal derivations that need the $\varphi^{-5}$ form without leaving the recovered line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.