hbar_range
plain-language theorem explainer
The theorem establishes that the reduced Planck constant ħ in RS-native units lies strictly between 0.088 and 0.093. Researchers verifying Recognition Science numerical predictions would cite this to confirm the φ^{-5} derivation matches the required interval. The proof is a direct one-line reference to the hbar_bounds theorem.
Claim. In RS-native units, the reduced Planck constant satisfies $0.088 < ħ < 0.093$, where ħ = φ^{-5}.
background
The module supplies machine-verified bounds on Recognition Science predictions, each proved as a formal inequality in Lean rather than a floating-point check. The table lists ħ (RS-native) as φ^{-5} with proved interval (0.088, 0.093). Upstream, hbar is defined as cLagLock * tau0 and equals φ^{-5} in native units; hbar_bounds proves the interval from the phi bounds phi_gt_onePointSixOne and phi_lt_onePointSixTwo via algebraic reduction of φ^{-5}.
proof idea
One-line wrapper that applies the hbar_bounds theorem.
why it matters
This supplies the verified interval for ħ in the module's table of predictions, confirming the constant ħ = φ^{-5} from the RS-native units definition. It anchors the framework's claim that all key quantities fall in intervals containing measured values, consistent with the phi-ladder and T5 J-uniqueness. No open questions are touched; the result is closed by the upstream phi bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.