hbar_range
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.
claimIn 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 in Recognition Science
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.
scope and limits
- Does not compute or reference the CODATA experimental value of ħ.
- Does not derive the interval without the prior phi bounds theorem.
- Does not extend the bound to other constants or units.
formal statement (Lean)
132theorem hbar_range : (0.088 : ℝ) < hbar ∧ hbar < (0.093 : ℝ) := hbar_bounds
proof body
Term-mode proof.
133
134/-! ## Mass generation ratios -/
135
136/-- The muon/electron mass ratio involves φ¹¹ ≈ 199.
137 Specifically m_μ/m_e ≈ φ^(r_μ - r_e) = φ^(13-2) = φ¹¹. -/