pith. machine review for the scientific record. sign in
lemma proved term proof high

hbar_pos

show as:
view Lean formalization →

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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 308lemma hbar_pos : 0 < hbar := mul_pos cLagLock_pos tau0_pos

proof body

Term-mode proof.

 309
 310/-- **THEOREM C-004.1**: ℏ = φ⁻⁵ in RS-native units.
 311
 312    This is the fundamental identity: ℏ = E_coh · τ₀ = φ⁻⁵ · 1 = φ⁻⁵. -/

used by (24)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (15)

Lean names referenced from this declaration's body.