  14-/
  15
  16/-- Absolute difference helper for floats. -/
  17@[inline] def floatAbs (x : Float) : Float := Float.abs x
  18
  19/-- Approximate equality for floats with configurable tolerance. -/
  20@[inline] def approxEq (a b : Float) (tol : Float := 1e-6) : Bool :=
  21  floatAbs (a - b) ≤ tol
  22
  23/-- Compute the τ-route and λ-route ratios for a given RSUnits pack. -/
  24noncomputable def computeRatios (U : RSUnits) : Float × Float :=
  25  let clock : ℝ := RSUnits.tau_rec_display U / U.tau0
  26  let length : ℝ := RSUnits.lambda_kin_display U / U.ell0
  27  (Real.toFloat clock, Real.toFloat length)
  28
  29/-- Units/K-gate certificate with diagnostic ratios. -/
  30structure UnitsKGateCert where
  31  ok               : Bool
  32  tolerance        : Float := 1e-6
  33  baseClockRatio   : Float
  34  baseLengthRatio  : Float
  35  scaledClockRatio : Float
  36  scaledLengthRatio : Float
  37  errors           : List String := []
  38deriving Repr
  39
  40@[simp] def UnitsKGateCert.verified (c : UnitsKGateCert) : Prop := c.ok = true
  41
  42noncomputable def UnitsKGateCert.fromSource (_src : String) : UnitsKGateCert :=
  43  let base : RSUnits := { tau0 := 1, ell0 := 1, c := 1, c_ell0_tau0 := by simp }
  44  let scaled : RSUnits := { tau0 := 2, ell0 := 2, c := 1, c_ell0_tau0 := by simp }
  45  let (baseClock, baseLength) := computeRatios base
  46  let (scaledClock, scaledLength) := computeRatios scaled
  47  let tol : Float := 1e-6

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.