hbarL_bounds
plain-language theorem explainer
The LogicReal-mirrored reduced Planck constant lies strictly between the embedded bounds 0.088 and 0.093. Anyone citing the RS-native ℏ = φ^{-5} band on the recovered real line uses this. The proof is a two-sided transport: rewrite each inequality via toReal, then apply the ordinary real bounds theorem.
Claim. On the recovered real line, the mirrored reduced Planck constant $\hbar_L$ satisfies $\iota(0.088) < \hbar_L < \iota(0.093)$, where $\iota$ embeds ordinary reals into the LogicReal carrier.
background
The module LogicRealConstants mirrors Recognition Science constants on the recovered real line (LogicReal). Each definition is stated in LogicReal; companion theorems show that transport through toReal recovers the ordinary real constant from IndisputableMonolith.Constants.
In RS-native units one has $\hbar = \varphi^{-5}$. The upstream theorem C-004.5 (hbar_bounds) records the numerical consequence of the golden-ratio window $\varphi \in (1.61, 1.62)$: ordinary $\hbar$ lies in $(0.088, 0.093)$. The present declaration is the same band for the LogicReal lift $\hbar_L$, with bounds pushed in via the embedding fromReal.
Comparison of LogicReal elements is reduced to ordinary real comparison by the equivalence lt_iff_toReal_lt, together with the round-trip identities toReal_fromReal and toReal_hbarL.
proof idea
Split the conjunction with constructor. On each side, rewrite the LogicReal inequality by lt_iff_toReal_lt, cancel the embedding with toReal_fromReal, and identify the transported constant via toReal_hbarL. The resulting ordinary inequalities are exactly the two conjuncts of Constants.hbar_bounds, which are applied directly. No new arithmetic is performed here; the work is pure transport of the existing real band.
why it matters
This closes the LogicReal mirror of the RS-native $\hbar = \varphi^{-5}$ numerical window (primer: $\hbar = \varphi^{-5}$). It sits in the Foundation layer that re-expresses Constants on the recovered line so later LogicReal developments can quote the same band without dropping to $\mathbb{R}$ by hand. Upstream C-004.5 already ties the band to the $\varphi \in (1.61, 1.62)$ forcing; this declaration only lifts that fact. No downstream consumers are recorded yet; the sibling pattern (phiL, tickL, alphaInvL, ...) indicates it is part of the uniform constant-mirror suite rather than a one-off lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.