`IndisputableMonolith.ILG.Params`

IndisputableMonolith/ILG/Params.lean · 20 lines · 2 declarations

Explainer status: pending

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace ILG
   5
   6/-- Minimal parameter record used by downstream ILG modules outside the sealed Relativity subtree. -/
   7structure Params where
   8  alpha : ℝ := 1
   9  Clag  : ℝ := 0
  10
  11/-- Basic positivity properties for ILG parameters. -/
  12structure ParamProps (P : Params) : Prop :=
  13  (alpha_nonneg : 0 ≤ P.alpha)
  14  (Clag_nonneg : 0 ≤ P.Clag)
  15
  16end ILG
  17end IndisputableMonolith
  18
  19
  20

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