externalCalibration_of_tau0_seconds
plain-language theorem explainer
This definition assembles an ExternalCalibration record from one positive real τ₀ (seconds per tick). It derives the voxel length as c_SI ⋅ τ₀ and the coherence energy as hbar_SI / τ₀ using the exact SI anchors. Measurement theorists cite it when converting RS-native tick/voxel/act quantities to SI reporting without extra fit parameters. The body is a direct structure literal that applies the positivity lemmas for c_SI and hbar_SI together with a one-line simp for the speed-consistency field.
Claim. Let τ₀ > 0 be a real scalar. Define the external calibration by the record with seconds_per_tick = τ₀, meters_per_voxel = c ⋅ τ₀ where c = 299792458, joules_per_coh = ℏ / τ₀ where ℏ = 1.054571817 × 10^{-34}, together with the three positivity assertions and the equality (c ⋅ τ₀) / τ₀ = c.
background
The module supplies a concrete single-anchor protocol for SI reporting of RS-native measurements. RS theory runs in tick/voxel/coh/act units with c = 1. Supplying one measured scalar τ₀ in seconds lets the structure derive the remaining scales from the exact SI definitions of c and ℏ; everything else is definitional or follows by arithmetic.
proof idea
The definition is a direct record constructor. It assigns the input τ₀ to seconds_per_tick, multiplies by c_SI for meters_per_voxel, and divides hbar_SI by τ₀ for joules_per_coh. Positivity of seconds_per_tick is the hypothesis; the other two follow from mul_pos c_SI_pos htau and div_pos hbar_SI_pos htau. The speed_consistent field is discharged by simp after noting τ₀ ≠ 0.
why it matters
This definition supplies the concrete seam used by the sibling calibration and one_act_reports_hbar results to produce SI values from RS-native quantities. It realizes the single-anchor protocol in the module documentation, where only one empirical scalar is supplied and the rest follows from the SI definitions of c and ℏ. In the framework it bridges RS-native units (c = 1, ħ = φ^{-5}) to laboratory reporting without introducing fit parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.