IndisputableMonolith.Sociology.LegalTraditionsFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Legal Traditions from configDim — Jurisprudence Depth
   6
   7Five canonical world legal traditions (= configDim D = 5):
   8  civil law (Roman-Germanic), common law, Islamic (sharia),
   9  customary, socialist/post-socialist.
  10
  11These cover > 95 % of the world's jurisdictions as commonly classified
  12by comparative law.
  13
  14Lean status: 0 sorry, 0 axiom.
  15-/
  16
  17namespace IndisputableMonolith.Sociology.LegalTraditionsFromConfigDim
  18
  19inductive LegalTradition where
  20  | civilLaw
  21  | commonLaw
  22  | islamicSharia
  23  | customary
  24  | socialist
  25  deriving DecidableEq, Repr, BEq, Fintype
  26
  27theorem legalTradition_count : Fintype.card LegalTradition = 5 := by decide
  28
  29structure LegalTraditionsCert where
  30  five_traditions : Fintype.card LegalTradition = 5
  31
  32def legalTraditionsCert : LegalTraditionsCert where
  33  five_traditions := legalTradition_count
  34
  35end IndisputableMonolith.Sociology.LegalTraditionsFromConfigDim
  36