tau0_seconds_protocol_hygienic

formal source

  90      ]
  91  }
  92
  93theorem tau0_seconds_protocol_hygienic : Protocol.hygienic tau0_seconds_protocol := by
  94  simp [Protocol.hygienic, tau0_seconds_protocol]
  95
  96/-! ## Derive the full `ExternalCalibration` from one scalar -/
  97
  98/-- Build a full `ExternalCalibration` from one scalar: τ₀ in seconds. -/
  99noncomputable def externalCalibration_of_tau0_seconds (tau0_s : ℝ) (htau : 0 < tau0_s) :
 100    ExternalCalibration :=
 101  { seconds_per_tick := tau0_s
 102    meters_per_voxel := (c_SI : ℝ) * tau0_s
 103    joules_per_coh := hbar_SI / tau0_s
 104    seconds_pos := htau
 105    meters_pos := mul_pos c_SI_pos htau
 106    joules_pos := div_pos hbar_SI_pos htau
 107    speed_consistent := by
 108      have htau_ne : tau0_s ≠ 0 := ne_of_gt htau
 109      -- (c_SI * tau0_s) / tau0_s = 299792458
 110      simp [c_SI, htau_ne]
 111  }
 112
 113/-! ## Certificate: one-scalar calibration seam (explicit) -/
 114
 115/-- A calibration certificate bundling:
 1161) the single-anchor protocol
 1172) one measured scalar τ₀ in seconds
 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 ℝ