KGateMeasurement

formal source

 175/-! Measurement Protocols and Falsifiers -/
 176
 177/-- Measurement protocol for K-gate validation -/
 178structure KGateMeasurement where
 179  /-- Measured τ_rec (time-first route) -/
 180  tau_rec_measured : ℝ
 181  /-- Measured λ_kin (length-first route) -/
 182  lambda_kin_measured : ℝ
 183  /-- RS units pack used for normalization -/
 184  units : RSUnits
 185  /-- Measurement uncertainties -/
 186  sigma_tau : ℝ
 187  sigma_lambda : ℝ
 188  /-- Derived: K from each route -/
 189  K_from_tau : ℝ := tau_rec_measured / units.tau0
 190  K_from_lambda : ℝ := lambda_kin_measured / units.ell0
 191
 192/-- K-gate validation: routes agree within uncertainty -/
 193noncomputable def validateKGate (meas : KGateMeasurement) : Prop :=
 194  let tolerance := K_gate_tolerance meas.units meas.sigma_tau meas.sigma_lambda
 195  |meas.K_from_tau - meas.K_from_lambda| < tolerance
 196
 197/-- Falsifier: K-gate mismatch beyond tolerance -/
 198noncomputable def falsifier_K_gate_mismatch (meas : KGateMeasurement) : Prop :=
 199  ¬validateKGate meas
 200
 201/-! Bridge Factorization -/
 202
 203/-- Observable displays factor through units quotient (sketch) -/
 204theorem observable_factors_through_quotient (O : RSUnits → ℝ)
 205    (hQuot : ∀ U α, α ≠ 0 → O {tau0 := α * U.tau0, ell0 := α * U.ell0, c := U.c,
 206                               c_ell0_tau0 := by calc U.c * (α * U.tau0) = α * (U.c * U.tau0) := by ring
 207                                                     _ = α * U.ell0 := by rw [U.c_ell0_tau0]} = O U) :
 208    ∀ U1 U2, UnitsEquivalent U1 U2 → O U1 = O U2 := by