hbar_lt_one
plain-language theorem explainer
The theorem establishes that the reduced Planck constant ħ in RS-native units is strictly less than one. Researchers deriving quantum scales from the Recognition Science forcing chain would cite it to bound the action quantum below the natural unit scale set by φ. The proof rewrites ħ as φ^{-5} via the equality lemma, shows φ^5 > 1 from φ > 1 using real exponentiation, and concludes via division after handling the negative power.
Claim. In RS-native units with time quantum τ₀ = 1, the reduced Planck constant satisfies ħ < 1, where ħ = φ^{-5} and φ > 1 is the golden-ratio fixed point.
background
The Constants module works in RS-native units where the fundamental time quantum τ₀ equals one tick. The reduced Planck constant is introduced by the definition ħ = E_coh · τ₀, which the upstream lemma hbar_eq_phi_inv_fifth reduces to φ^{-5}. The lemma one_lt_phi supplies the key inequality φ > 1 that drives the comparison. Upstream doc-comment states: 'Reduced Planck constant ħ in RS-native units: ħ = E_coh · τ₀ = φ^{-5} · 1.'
proof idea
The tactic proof first rewrites the goal with hbar_eq_phi_inv_fifth to obtain φ^{-5} < 1. It proves φ^5 > 1 by applying Real.rpow_lt_rpow to one_lt_phi together with the positive exponent 5. The negative exponent is rewritten as 1/φ^5 via Real.rpow_neg, positivity of the denominator is obtained by positivity, and div_lt_iff₀ together with linarith finishes the inequality.
why it matters
Labeled THEOREM C-004.3, the result confirms that the action quantum is small compared to natural units and supports the physical reading ħ = E_coh · τ₀. It follows directly after the equality lemma hbar_eq_phi_inv_fifth and the positivity of φ. Within the framework it anchors the scale for quantum dynamics inside the eight-tick octave and the three spatial dimensions obtained from the T0-T8 forcing chain. No downstream uses appear yet, leaving open its insertion into mass-ladder or Berry-threshold arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.