GeopoliticalPower
plain-language theorem explainer
GeopoliticalPower enumerates the five canonical categories of state power used to model international order as a recognition equilibrium in Recognition Science. Political scientists and sociologists working in the RS framework cite it to set configDim D equal to 5. The declaration is an inductive definition that automatically derives DecidableEq, Repr, BEq, and Fintype instances, enabling immediate cardinality computation.
Claim. The set of geopolitical power categories is the five-element inductive type with constructors military, economic, diplomatic, cultural, and technological, equipped with decidable equality and finite cardinality.
background
Recognition Science treats international order as an equilibrium between states where the recognition cost J vanishes. The module equates the five power categories to the configuration dimension D = 5, with balance of power at J = 0 and transitions at J > 0. This definition supplies the discrete carrier set for those statements.
proof idea
Inductive definition enumerating the five constructors, followed by a deriving clause that installs the four type-class instances.
why it matters
The definition is required by the downstream theorem geopoliticalPowerCount, which proves Fintype.card = 5, and by the structure GeopoliticsCert, which pairs that cardinality with the equilibrium condition Jcost 1 = 0. It directly realizes the Recognition Science claim that international order is a recognition equilibrium with configDim D = 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.