to_joule_seconds
plain-language theorem explainer
This definition converts an RS-native action quantum in act units to SI joule-seconds by multiplying the act value by the product of joules per coherence quantum and seconds per tick drawn from an ExternalCalibration record. Experimental physicists comparing RS predictions to measured action values would cite it when reporting native results in standard units. The implementation is a direct scalar multiplication that follows immediately from the one-act-equals-one-coh-times-one-tick correspondence.
Claim. Let $cal$ be an $ExternalCalibration$ record with scaling factors $joules_per_coh$ and $seconds_per_tick$. For an action $a$ in act units the SI value in joule-seconds is $a · joules_per_coh · seconds_per_tick$.
background
The module supplies the explicit seam for reporting RS-native quantities in SI without embedding CODATA numerals in the core theory. An $ExternalCalibration$ structure holds the three conversion constants: seconds per tick, meters per voxel, and joules per coherence quantum. The $Act$ type is an abbreviation for $Quantity ActUnit$, the native unit in which one act equals one coherence quantum times one fundamental tick.
proof idea
One-line definition that casts the act value to ℝ and multiplies it by the product of the two calibration fields. No lemmas are applied; the body directly encodes the unit rule given in the doc-comment.
why it matters
The definition is called by $measure_to_joule_seconds$ to lift the scaling to full measurement records and by $one_act_reports_hbar$ to prove that one act equals ħ in SI units. It therefore closes the reporting interface between RS-native theory and laboratory data, supporting direct numerical checks against the Planck constant while preserving the separation of native axioms from external constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.