PowerTransitionCert
PowerTransitionCert bundles the J-cost properties required for power transition theory in the Recognition Science framework. Modelers of interstate conflict would cite it to establish zero cost at capability parity and the war window between the inverse golden ratio and the golden ratio. The definition assembles six field properties, each supplied by a direct lemma in the module.
claimA structure asserting: for nonzero $c$, the J-cost of the capability ratio $c/c$ equals zero; for positive rising and incumbent capabilities the J-cost is nonnegative; the lower war-window bound is positive; the upper bound exceeds one; the lower bound is less than the upper; and the J-cost at ratio $phi$ with incumbent 1 equals $phi - 3/2$.
background
The module applies Recognition Science to Organski's power transition theory, where conflict probability peaks when a rising power's capabilities approach parity with the incumbent. capabilityCost(r,i) denotes the J-cost of the ratio r/i, with the canonical J-cost function satisfying nonnegativity as proved in ObserverForcing.cost_nonneg. The war window is defined as the interval (warWindowLow, warWindowHigh) = (1/phi, phi), inside which J(r) remains below its value at the boundary phi.
proof idea
The structure definition directly enumerates its six fields without additional proof steps. Each field is populated downstream by applying the corresponding sibling lemma such as capabilityCost_at_parity for the parity condition and warWindowLow_pos for the positivity of the lower bound.
why it matters in Recognition Science
This structure serves as the type for the cert instance that witnesses the power transition properties, and cert_inhabited proves it is nonempty. It realizes the first International Relations application in the codebase, connecting the J-uniqueness property to the prediction that the parity band (1/phi, phi) is the region of maximal instability. The module doc notes the falsifier as any COW dataset analysis showing no clustering of great-power conflicts in that interval.
scope and limits
- Does not compute numerical values for specific country capabilities.
- Does not prove that J-cost is the sole driver of conflict.
- Does not address multipolar systems beyond dyadic parity.
- Does not derive the golden ratio from the forcing chain in this module.
formal statement (Lean)
76structure PowerTransitionCert where
77 cost_at_parity : ∀ c : ℝ, c ≠ 0 → capabilityCost c c = 0
78 cost_nonneg : ∀ r i : ℝ, 0 < r → 0 < i → 0 ≤ capabilityCost r i
79 war_window_low_pos : 0 < warWindowLow
80 war_window_high_gt_one : 1 < warWindowHigh
81 war_window_ordered : warWindowLow < warWindowHigh
82 boundary_cost : capabilityCost phi 1 = phi - 3 / 2
83