tau0_seconds_protocol

formal source

  73
  74This is an *explicit* seam. It does not tune any dimensionless RS predictions;
  75it only fixes the SI reporting scale. -/
  76def tau0_seconds_protocol : Protocol :=
  77  { name := "calibration.single_anchor.tau0_seconds"
  78    summary :=
  79      "Single-anchor SI calibration. Supply τ0 (seconds per tick) as the only empirical scalar. " ++
  80      "Derive meters_per_voxel via SI-defined c=299792458 and derive joules_per_coh via SI-defined h (hbar=h/(2π)) " ++
  81      "together with RS identity 1 act = 1 coh * 1 tick. No mass-data fitting; this is a reporting seam only."
  82    status := .hypothesis
  83    assumptions :=
  84      [ "A1: τ0 (one RS tick) corresponds to a stable physical duration that can be measured in SI seconds using a declared lab protocol."
  85      , "A2: SI definitional constants (c and h) are treated as exact conventions; they introduce no fit freedom."
  86      ]
  87    falsifiers :=
  88      [ "F1: Two independent anchors for τ0 (e.g. time-first vs length-first) disagree beyond stated uncertainties."
  89      , "F2: Under the derived calibration, the SI speed consistency check fails beyond uncertainty."
  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