pith. machine review for the scientific record. sign in
def definition def or abbrev high

h_SI

show as:
view Lean formalization →

Supplies the exact rational form of the 2019 SI Planck constant as 662607015 / 10^42. Single-anchor calibration protocols cite it to fix joules_per_coh once seconds_per_tick is chosen. The body is a direct literal assignment of the rational matching the exact SI value.

claimThe Planck constant equals $h = 662607015 / 10^{42}$ in joule-seconds (exact 2019 SI definition).

background

The module supplies a concrete single-anchor protocol for converting RS-native measurements (tick, voxel, coh, act) to SI reporting. RS-native theory runs with c = 1 and no SI numerals; one empirical scalar (seconds_per_tick) is supplied, after which meters_per_voxel follows from the SI definition of c and joules_per_coh follows from this h together with the identity 1 act = 1 coh × 1 tick. The upstream external anchor in Constants.ExternalAnchors provides the identical numerical value expressed in decimal form.

proof idea

One-line definition that directly assigns the rational (662607015 : ℝ) / ((10 : ℝ) ^ (42 : ℕ)) to represent the exact SI value 6.62607015 × 10^{-34}.

why it matters in Recognition Science

Provides the h anchor inside the single-anchor calibration that lets RS-native quantities be reported in SI units using only one empirical scalar. It is referenced by the downstream definitions hbar_SI and the positivity lemma h_SI_pos. This seam connects the RS-native constants (hbar = phi^{-5} in native units, RCL composition law) to the 2019 SI exact values without fit parameters.

scope and limits

formal statement (Lean)

  49noncomputable def h_SI : ℝ :=

proof body

Definition body.

  50  (662607015 : ℝ) / ((10 : ℝ) ^ (42 : ℕ))
  51

used by (3)

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

depends on (1)

Lean names referenced from this declaration's body.