hbar_codata
plain-language theorem explainer
hbar_codata supplies the CODATA numerical value for the reduced Planck constant in SI units. Researchers deriving G and related constants from Recognition Science primitives cite this definition to anchor numerical comparisons against experiment. The declaration consists of a direct real-number literal assignment with no computation or hypotheses.
Claim. $h = 1.054571817 × 10^{-34}$ (in J·s, SI units)
background
The module anchors derivations of physical constants to standard CODATA reference values: c = 299792458 m/s (exact), ℏ = 1.054571817×10⁻³⁴ J·s, and G = 6.67430×10⁻¹¹ m³/(kg·s²). These values serve as fixed inputs for positivity lemmas and equality checks that relate derived expressions back to measured constants. No upstream lemmas are required; the definition stands alone as a reference datum.
proof idea
This is a one-line definition that directly assigns the floating-point literal 1.054571817e-34 to the identifier.
why it matters
The definition supplies the empirical ℏ input required by G_relation_satisfied, which proves G_derived tau0 hbar_codata c_codata equals the CODATA G value, and by positivity results such as hbar_codata_pos and hbar_derived_pos. It thereby links the Recognition Science forcing chain (T5 J-uniqueness through T8 D=3) and the phi-ladder mass formula to laboratory data. Downstream uses also include planck_length and inner_nonneg.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.