hbar_pos
plain-language theorem explainer
Proves that the reduced Planck constant ħ is positive in RS-native units, where ħ equals phi to the power of negative five. Researchers deriving quantum scales from the phi-ladder cite it to secure inequalities for action and energy. The proof is a direct term-mode application of mul_pos to the positivity of cLagLock and tau0.
Claim. $0 < ħ$ where $ħ := c_{LagLock} · τ_0$, $c_{LagLock} = φ^{-5}$, and $τ_0 = 1$ tick in RS-native units.
background
The Constants module defines ħ as the product cLagLock * tau0. Here cLagLock is the canonical locked lag constant φ^{-5} and tau0 is the fundamental RS time quantum of one tick. The module derives constants from the forcing chain with phi as self-similar fixed point and the eight-tick octave. Upstream, tau0_pos states 0 < tau0 by simplification to zero_lt_one, while cLagLock_pos uses Real.rpow_pos_of_pos on phi_pos. The hbar definition states: ħ = E_coh · τ₀ = φ^{-5} · 1.
proof idea
One-line term proof that applies mul_pos directly to cLagLock_pos and tau0_pos.
why it matters
This lemma supplies the positivity of ħ required by the Physical structure in Bridge.DataCore, which supports lambda_rec_pos and G_pos. It closes the C-004.1 identity ħ = φ^{-5} from the RS derivation, consistent with the framework landmark hbar = phi^{-5} obtained from J-uniqueness and the phi fixed point. It is referenced by hbar_positive and Codata hbar_ne_zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.