one_act_reports_hbar
plain-language theorem explainer
Given a calibration certificate supplying the empirical seconds-per-tick anchor τ₀, one act converts exactly to the SI value of ħ in joule-seconds. Metrologists bridging RS-native computations to laboratory units would cite this to validate single-anchor reporting. The proof is a term-mode simplification that first extracts positivity of τ₀ then cancels the scaling factor via direct expansion of the conversion definition.
Claim. Let cert be a certificate supplying positive τ₀ seconds per tick under the single-anchor protocol. Then the SI conversion of one act under the derived external calibration equals the exact SI reduced Planck constant: to_joule_seconds(calibration(cert), 1) = ħ_SI.
background
The module implements single-anchor SI calibration for RS-native units (tick, voxel, coh, act) with c = 1. A CalibrationCert bundles one measured scalar τ₀ (seconds per tick), a protocol flag, and positivity. From this the module derives meters_per_voxel from the SI definition of c and joules_per_coh from the SI definition of h (hence ħ), using the identity that one act equals one coherence times one tick. The upstream constant hbar_SI is the exact 2019 SI anchor 1.054571817 × 10^{-34} J·s. The conversion to_joule_seconds multiplies the act count by joules_per_coh and seconds_per_tick.
proof idea
The term proof first constructs the auxiliary fact that the certificate's τ₀ value is nonzero by applying ne_of_gt to the tau0_pos field of the certificate. It then calls simp on the definitions of to_joule_seconds, calibration, externalCalibration_of_tau0_seconds, the auxiliary nonzero fact, and hbar_SI; the simplifier cancels the τ₀ factor and matches the SI anchor directly.
why it matters
This theorem closes the single-anchor calibration path that lets RS-native measurements report in SI without fit parameters. It sits inside the calibration module whose parent is the external anchor hbar_SI and the RS identity 1 act = 1 coh × 1 tick. The result supports the broader framework goal of matching native units (where ħ = phi^{-5}) to laboratory constants while keeping only one empirical scalar.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.