`IndisputableMonolith.Verification.Audit`

IndisputableMonolith/Verification/Audit.lean · 14 lines · 0 declarations

Explainer status: pending

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Verification
   5
   6/-! ### Audit Guard
   7
   8**SI Evaluation Policy**: All SI unit evaluations must go through BridgeData.
   9This ensures proper dimensional analysis and prevents accidental direct
  10numerics at the proof layer. -/
  11
  12end Verification
  13end IndisputableMonolith
  14

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