pith. machine review for the scientific record. sign in

IndisputableMonolith.Sociology.InstitutionalDesignFromJCost

IndisputableMonolith/Sociology/InstitutionalDesignFromJCost.lean · 32 lines · 2 declarations

show as:
view math explainer →

open module explainer GitHub source

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Common.CanonicalJBand
   3
   4/-!
   5# E7: Institutional Design from J-Cost on Power-Distribution Ratio
   6
   7Compounds with `Sociology/PoliticalSystemsFromSigmaConservation` (5
   8canonical institutions = `configDim D`). Per-institution-pair J-cost
   9on `r := observed_power_concentration / balanced_distribution`. Stable
  10governance keeps J-cost below the canonical band on every pair;
  11institutional capture / runaway authoritarianism is the regime that
  12crosses it.
  13
  14Lean status: 0 sorry, 0 axiom.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Sociology
  19namespace InstitutionalDesignFromJCost
  20
  21open Common.CanonicalJBand
  22
  23structure InstitutionalDesignCert where
  24  base : CanonicalCert
  25
  26def institutionalDesignCert : InstitutionalDesignCert where
  27  base := cert
  28
  29end InstitutionalDesignFromJCost
  30end Sociology
  31end IndisputableMonolith
  32

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