IndisputableMonolith.Sociology.InstitutionalDesignFromJCost
IndisputableMonolith/Sociology/InstitutionalDesignFromJCost.lean · 32 lines · 2 declarations
show as:
view math explainer →
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