c_reports_exact

formal source

 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
 152  -- Expand definitions and cancel τ0_s.
 153  have htau_ne : cert.tau0_seconds.value ≠ 0 := ne_of_gt cert.tau0_pos
 154  -- to_joule_seconds uses: (A:ℝ) * (joules_per_coh * seconds_per_tick)
 155  simp [IndisputableMonolith.Measurement.RSNative.Calibration.SI.to_joule_seconds,
 156    calibration, externalCalibration_of_tau0_seconds, htau_ne, hbar_SI]
 157
 158/-! ## Convenience constructor (for use in examples/tests) -/
 159
 160/-- Build a certificate from a chosen τ₀ (seconds per tick).
 161
 162This is a helper for downstream modules; real usage should supply a `Protocol`d
 163measurement record coming from a declared empirical procedure. -/
 164def mkCert (tau0_s : ℝ) (htau : 0 < tau0_s) : CalibrationCert :=
 165  { tau0_seconds :=
 166      { value := tau0_s
 167        protocol := tau0_seconds_protocol
 168        notes := ["Units: SI seconds per RS tick (single-anchor calibration seam)."] }
 169    protocol_ok := rfl
 170    tau0_pos := htau