`IndisputableMonolith.URCAdapters.UnitsIdentity`

IndisputableMonolith/URCAdapters/UnitsIdentity.lean · 16 lines · 2 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace URCAdapters
   6
   7/-- Units identity as a Prop: c·τ0 = ℓ0 for all anchors. -/
   8def units_identity_prop : Prop :=
   9  ∀ U : IndisputableMonolith.Constants.RSUnits, U.c * U.tau0 = U.ell0
  10
  11lemma units_identity_holds : units_identity_prop := by
  12  intro U; simpa using U.c_ell0_tau0
  13
  14end URCAdapters
  15end IndisputableMonolith
  16

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