IndisputableMonolith.Certificates.UnitsKGate

   1import Mathlib
   2import IndisputableMonolith.Constants.KDisplay
   3
   4namespace IndisputableMonolith
   5namespace Certificates
   6
   7open IndisputableMonolith.Constants
   8
   9/-! # Units / K-gate Audit Certificate
  10
  11Evaluates the K-gate identities (time-first vs length-first displays) on a
  12canonical RS units pack and on a rescaled pack, ensuring the quotient is
  13dimensionless and invariant under admissible rescalings.
  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
  48  let baseMatch := approxEq baseClock baseLength tol
  49  let baseMatchesK := approxEq baseClock (Float.ofInt 1) tol
  50  let scaledMatch := approxEq scaledClock scaledLength tol
  51  let crossMatch := approxEq baseClock scaledClock tol
  52  let ok := baseMatch && baseMatchesK && scaledMatch && crossMatch
  53  let errors :=
  54    if ok then []
  55    else ["Units/K-gate mismatch detected (τ-route vs λ-route)"]
  56  { ok := ok,
  57    tolerance := tol,
  58    baseClockRatio := baseClock,
  59    baseLengthRatio := baseLength,
  60    scaledClockRatio := scaledClock,
  61    scaledLengthRatio := scaledLength,
  62    errors := errors }
  63
  64end Certificates
  65end IndisputableMonolith
  66