CalibrationCert

formal source

 1183) the derived full `ExternalCalibration` used for SI reporting
 119
 120Everything beyond τ₀ is derived (or SI-definitional). -/
 121structure CalibrationCert where
 122  /-- The single empirical scalar: τ₀ in seconds (seconds per tick). -/
 123  tau0_seconds : Measurement ℝ
 124  /-- Protocol is the canonical single-anchor protocol. -/
 125  protocol_ok : tau0_seconds.protocol = tau0_seconds_protocol
 126  /-- Positivity: τ₀ must be positive. -/
 127  tau0_pos : 0 < tau0_seconds.value
 128
 129/-- The derived `ExternalCalibration` associated to a certificate. -/
 130noncomputable def calibration (cert : CalibrationCert) : ExternalCalibration :=
 131  externalCalibration_of_tau0_seconds cert.tau0_seconds.value cert.tau0_pos
 132
 133theorem calibration_protocol_hygienic (cert : CalibrationCert) :
 134    Protocol.hygienic cert.tau0_seconds.protocol := by
 135  simpa [cert.protocol_ok] using tau0_seconds_protocol_hygienic
 136
 137/-! ## Consistency checks (derived, not additional parameters) -/
 138
 139/-- Under the derived calibration, 1 voxel/tick reports exactly c_SI in m/s. -/
 140theorem c_reports_exact (cert : CalibrationCert) :
 141    IndisputableMonolith.Constants.RSNativeUnits.to_m_per_s (calibration cert)
 142        IndisputableMonolith.Constants.RSNativeUnits.c = c_SI := by
 143  -- This follows from the `speed_consistent` field plus `c_in_si`.
 144  -- Note: RSNativeUnits.c = 1 (voxel/tick).
 145  have := IndisputableMonolith.Constants.RSNativeUnits.c_in_si (calibration cert)
 146  simpa [c_SI] using this
 147
 148/-- Under the derived calibration, 1 act reports \(\hbar\) in SI \(J·s\). -/
 149theorem one_act_reports_hbar (cert : CalibrationCert) :
 150    IndisputableMonolith.Measurement.RSNative.Calibration.SI.to_joule_seconds
 151        (calibration cert) (⟨(1 : ℝ)⟩ : Act) = hbar_SI := by