`IndisputableMonolith.Verification.Exports`

IndisputableMonolith/Verification/Exports.lean · 12 lines · 1 declarations

Explainer status: pending

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Verification
   5
   6/-- Export: 45-gap clock-lag fraction identity (dimensionless): δ_time = 3/64. -/
   7theorem gap_delta_time_identity : (45 : ℚ) / 960 = (3 : ℚ) / 64 := by
   8  norm_num
   9
  10end Verification
  11end IndisputableMonolith
  12

source mirrored from github.com/jonwashburn/shape-of-logic