hbar_derived
plain-language theorem explainer
The declaration defines the reduced Planck constant as the product of coherence energy and base time in RS units. Researchers deriving constants from the phi ladder would cite this as the IR gate identity. The definition is a direct multiplication implementing the gate without additional computation.
Claim. $ℏ = E_{coh} ⋅ τ₀$ where $E_{coh} = φ^{-5}$ (in RS units).
background
The module derives all constants from φ via gate identities in the chain φ → E_coh → τ₀ → c → ℏ → G → α^{-1}. E_coh is defined as φ^{-5} and represents the coherence energy scale (≈ 0.09 eV). The IR gate states that ℏ equals the product of this energy and the base time τ₀. Upstream, the sibling hbar_derived in Constants.Derivation supplies a different expression involving π, c^5, τ^2 and G for the Planck relation.
proof idea
One-line definition that directly multiplies the two real inputs to realize the IR gate identity.
why it matters
This definition supplies the IR gate identity that feeds the Planck relation theorem and the fine-structure derivation. It closes the step from E_coh and τ₀ to ℏ in the Recognition Science constant chain, enabling downstream results such as planck_relation_satisfied and the IR_gate_identity theorem that equates the product to the derived hbar.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.