hbar_bounds
plain-language theorem explainer
The theorem proves that the reduced Planck constant ħ in RS-native units satisfies 0.088 < ħ < 0.093 when the golden ratio lies in the interval 1.61 < φ < 1.62. Researchers building numerical mass predictions on the phi-ladder cite this bound to fix ħ for downstream calculations. The proof substitutes the identity ħ = φ^{-5}, applies the supplied φ inequalities to bound φ^5 via real exponentiation, and inverts to obtain the numerical interval.
Claim. If $1.61 < φ < 1.62$ then $0.088 < ħ < 0.093$, where ħ = φ^{-5} denotes the reduced Planck constant in RS-native units with c = 1 and τ₀ = 1 tick.
background
Recognition Science fixes the golden ratio φ as the self-similar fixed point of the J-cost functional. The reduced Planck constant is defined by ħ = φ^{-5} in units where the fundamental time quantum τ₀ equals one tick. The lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo supply the tight bounds 1.61 < φ < 1.62, while hbar_eq_phi_inv_fifth records the identity ħ = φ^{-5}. These constants belong to the forcing chain that also yields the eight-tick octave and D = 3 spatial dimensions.
proof idea
The tactic proof rewrites the goal with hbar_eq_phi_inv_fifth. It invokes phi_gt_onePointSixOne and phi_lt_onePointSixTwo, then applies Real.rpow_lt_rpow twice to bound φ^5. Separate blocks invert the inequalities using one_div_lt_one_div and div_lt_div_iff₀, followed by norm_num to confirm the concrete thresholds 1/1.62^5 > 0.088 and 1/1.61^5 < 0.093. The two resulting inequalities are packaged with exact.
why it matters
The result is reused verbatim by hbar_range inside the NumericalPredictions module and thereby contributes to the master certificate NumericalPredictionsCert that also certifies the interval 137.030 < α^{-1} < 137.039. It closes the numerical bounds section of the constants chain, anchoring the RS-native value ħ = φ^{-5} required for consistent mass formulas on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.