geopoliticalPowerCount
plain-language theorem explainer
The declaration establishes that the inductive type of geopolitical powers contains exactly five elements. Sociologists extending Recognition Science to international relations would cite this count when fixing the canonical power categories. The proof is a one-line decision procedure that enumerates the constructors of the finite inductive type.
Claim. The finite type of canonical geopolitical power categories has cardinality five: $ |$ {military, economic, diplomatic, cultural, technological} $ | = 5 $.
background
The module formalizes geopolitical power as an inductive type whose five constructors are military, economic, diplomatic, cultural, and technological. This count is identified with the configuration dimension D = 5 in the sociological extension of Recognition Science, where international order is a recognition equilibrium between states and balance of power corresponds to vanishing J-cost.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. The tactic computes Fintype.card directly from the inductive definition by enumerating its five constructors and confirming the cardinality.
why it matters
It supplies the five_powers field inside the downstream GeopoliticsCert definition, which also records the equilibrium condition. The result fills the configuration-dimension step in the sociology module, linking to the spatial dimension D = 3 and the eight-tick octave while leaving open a direct derivation of the five categories from the phi-ladder or J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.