validateKGate

formal source

 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
 209  intro U1 U2 h
 210  obtain ⟨hc, α, hα, hτ, hℓ⟩ := h
 211  -- U2 = scaled version of U1
 212  have h1 := hQuot U1 α hα
 213  -- Need to show the scaled U1 equals U2
 214  have hU2_eq : U2 = {tau0 := α * U1.tau0, ell0 := α * U1.ell0, c := U1.c,
 215                       c_ell0_tau0 := by calc U1.c * (α * U1.tau0) = α * (U1.c * U1.tau0) := by ring
 216                                             _ = α * U1.ell0 := by rw [U1.c_ell0_tau0]} := by
 217    cases U2
 218    simp only [RSUnits.mk.injEq]
 219    exact ⟨hτ, hℓ, hc.symm⟩
 220  rw [hU2_eq]
 221  exact h1.symm
 222
 223/-! Documentation and Usage -/