hbar_derived
plain-language theorem explainer
This definition supplies the explicit formula for the reduced Planck constant as ħ = π c⁵ τ² / G, with τ the base time scale from the forcing chain. Researchers verifying Recognition Science constant derivations against CODATA values cite it to link the IR gate identity to measurable G and c. The definition is a direct algebraic expression requiring no lemmas or reductions.
Claim. The reduced Planck constant is given by $ħ = π c^5 τ^2 / G$, where $τ$ denotes the fundamental time interval, $G$ the gravitational constant, and $c$ the speed of light.
background
The Constants.Derivation module expresses physical constants from Recognition Science primitives, referencing CODATA values for c, ħ, and G. The upstream result states that ℏ = E_coh · τ₀ (the IR gate identity), noting this is derived from φ rather than measured. This definition supplies the equivalent closed form obtained by substituting the RS relations for G and c.
proof idea
This is a direct definition consisting of the single algebraic expression Real.pi * c_val ^ 5 * τ ^ 2 / G_val. No tactics or lemmas are invoked; the body is the closed-form formula.
why it matters
The definition feeds the downstream results hbar_derived_pos and planck_relation_satisfied, which verify that the expression equals the CODATA ħ value. It instantiates the constant derivations in the Recognition Science framework, connecting the IR gate identity to the phi-ladder scalings at T5-T8 where G = φ^5 / π and ħ = φ^{-5}. It touches the open question of exact numerical agreement with the alpha band without further parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.