hbar_lt_one
plain-language theorem explainer
The declaration proves that the reduced Planck constant ħ in Recognition Science native units satisfies ħ < 1. Researchers normalizing physics to the recognition time quantum τ₀ = 1 would cite this result when confirming that the action quantum lies below the unit scale. The proof rewrites ħ via its defining identity as φ^{-5} and reduces the inequality to the elementary fact that φ > 1 using real exponentiation rules.
Claim. $\hbar < 1$, where $\hbar = \phi^{-5}$ in RS-native units with $\phi$ the golden ratio.
background
In the Constants module the reduced Planck constant is defined as ħ = E_coh · τ₀ with τ₀ the fundamental time quantum equal to one tick. The upstream lemma hbar_eq_phi_inv_fifth states that ħ = φ^{-5} in these units. The lemma one_lt_phi establishes 1 < φ. The module sets the RS-native time quantum τ₀ = 1 tick.
The theorem sits among a cluster of results establishing the numerical properties of ħ relative to the unit scale.
proof idea
The proof begins by rewriting the goal with hbar_eq_phi_inv_fifth to obtain φ^{-5} < 1. It then proves φ^5 > 1 by applying one_lt_phi together with the monotonicity of real exponentiation for positive bases. A separate step rewrites the negative exponent as a reciprocal and concludes the inequality by the properties of division.
why it matters
This result is labeled THEOREM C-004.3 and supplies the strict inequality ħ < 1 required for the action quantum to be small compared to natural units. It follows directly from the identity ħ = φ^{-5} (C-004.1) and the forcing of φ > 1. The declaration supports downstream statements about quantum dynamics in the Recognition framework, including the interpretation of ħ as minimal action for a recognition event.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.