IndisputableMonolith.Measurement.RSNative.Calibration.SI

   1import Mathlib
   2import IndisputableMonolith.Measurement.RSNative.Core
   3import IndisputableMonolith.Constants.RSNativeUnits
   4
   5/-!
   6# RS-Native → SI Calibration Adapter
   7
   8This module is the explicit seam where RS-native quantities can be *reported* in SI.
   9
  10Key rule:
  11- RS-native theory and RS-native measurement catalogs must not depend on CODATA numerals.
  12- SI conversion happens only through an explicit `ExternalCalibration` record supplied externally.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Measurement
  17namespace RSNative
  18namespace Calibration
  19namespace SI
  20
  21open IndisputableMonolith.Constants.RSNativeUnits
  22
  23/-! ## Scalar conversions -/
  24
  25@[simp] noncomputable def to_seconds (cal : ExternalCalibration) (t : Tick) : ℝ :=
  26  (t : ℝ) * cal.seconds_per_tick
  27
  28@[simp] noncomputable def to_meters (cal : ExternalCalibration) (L : Voxel) : ℝ :=
  29  (L : ℝ) * cal.meters_per_voxel
  30
  31@[simp] noncomputable def to_joules (cal : ExternalCalibration) (E : Coh) : ℝ :=
  32  (E : ℝ) * cal.joules_per_coh
  33
  34/-- Convert action quanta (act) to SI \(J·s\).
  35
  36In RS-native units, `1 act` corresponds to `1 coh * 1 tick`.
  37So the SI conversion is `joules_per_coh * seconds_per_tick`.
  38-/
  39@[simp] noncomputable def to_joule_seconds (cal : ExternalCalibration) (A : Act) : ℝ :=
  40  (A : ℝ) * (cal.joules_per_coh * cal.seconds_per_tick)
  41
  42/-! ## Measurement-level conversion helpers -/
  43
  44private def scaleUncertainty (c : ℝ) (hc : 0 ≤ c) (u : Uncertainty) : Uncertainty :=
  45  match u with
  46  | .sigma σ hσ =>
  47      .sigma (σ * c) (mul_nonneg hσ hc)
  48  | .interval lo hi hlohi =>
  49      .interval (lo * c) (hi * c) (mul_le_mul_of_nonneg_right hlohi hc)
  50  | .discrete support =>
  51      .discrete (support.map (fun vw => (vw.1 * c, vw.2)))
  52
  53noncomputable def measure_to_seconds (cal : ExternalCalibration) (m : Measurement Tick) : Measurement ℝ :=
  54  Measurement.map (to_seconds cal)
  55    (Measurement.mapUncertainty
  56      (fun u => scaleUncertainty cal.seconds_per_tick (le_of_lt cal.seconds_pos) u) m)
  57
  58noncomputable def measure_to_meters (cal : ExternalCalibration) (m : Measurement Voxel) : Measurement ℝ :=
  59  Measurement.map (to_meters cal)
  60    (Measurement.mapUncertainty
  61      (fun u => scaleUncertainty cal.meters_per_voxel (le_of_lt cal.meters_pos) u) m)
  62
  63noncomputable def measure_to_joules (cal : ExternalCalibration) (m : Measurement Coh) : Measurement ℝ :=
  64  Measurement.map (to_joules cal)
  65    (Measurement.mapUncertainty
  66      (fun u => scaleUncertainty cal.joules_per_coh (le_of_lt cal.joules_pos) u) m)
  67
  68noncomputable def measure_to_joule_seconds (cal : ExternalCalibration) (m : Measurement Act) : Measurement ℝ :=
  69  Measurement.map (to_joule_seconds cal)
  70    (Measurement.mapUncertainty
  71      (fun u =>
  72        scaleUncertainty (cal.joules_per_coh * cal.seconds_per_tick)
  73          (mul_nonneg (le_of_lt cal.joules_pos) (le_of_lt cal.seconds_pos)) u) m)
  74
  75end SI
  76end Calibration
  77end RSNative
  78end Measurement
  79end IndisputableMonolith
  80