h_SI_pos
plain-language theorem explainer
Positivity of the exact SI Planck constant follows from its decimal representation as an external anchor. Calibration protocols converting RS-native tick and voxel units to SI cite this result to guarantee sign consistency when deriving ħ and related scales. The tactic proof unfolds the definition then applies norm_num and the division-positivity rule to the explicit numerator and denominator.
Claim. $0 < h_{SI}$ where $h_{SI} = 6.62607015 × 10^{-34}$ (J s) is the exact 2019 SI definition of Planck's constant.
background
The SingleAnchor module supplies a concrete calibration protocol that reports RS-native measurements in SI units using only one empirical scalar, seconds per tick. All other factors are derived from the exact SI definitions of c and h together with the identity that one act equals one coh times one tick. The constant h_SI is the external anchor imported from ExternalAnchors and defined explicitly as the 2019 exact value 6.62607015e-34. Upstream results include the RS-native ħ expressed as cLagLock times tau0 and the ledger-factorization structure that governs J-cost.
proof idea
The proof unfolds h_SI to expose its decimal form. Separate norm_num steps establish positivity of the numerator 662607015 and of the denominator 10^42 via pow_pos. The final step applies the division-positivity lemma to obtain the result.
why it matters
This lemma is invoked directly by the downstream positivity statement for ħ_SI inside the same module. It closes the single-anchor calibration by confirming that the supplied Planck constant satisfies the positivity required for all derived SI conversions. The module context stresses that only one empirical scalar enters while the remainder is fixed by SI definitions and the RS act-coh-tick identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.