cert
The cert definition supplies a concrete PowerTransitionCert instance that certifies the J-cost properties underlying power transition predictions. Researchers in international relations applying recognition science would cite this to quantify the instability band around capability parity. The construction directly references the module's lemmas for cost at parity, non-negativity, and war window bounds derived from the golden ratio.
claimDefine $cert$ as the structure satisfying: for all $c ≠ 0$, capabilityCost$(c,c)=0$; for all $r,i>0$, $0 ≤$ capabilityCost$(r,i)$; the lower war-window bound is positive; the upper war-window bound exceeds 1; the war-window bounds are ordered; and capabilityCost$($φ$,1) = φ - 3/2$.
background
The module develops Power Transition Theory from the J-cost function. CapabilityCost$(r,i)$ is defined as the J-cost of the capability ratio $r/i$, inheriting non-negativity from the upstream cost_nonneg theorem on RecognitionEvent. The war window is the interval (warWindowLow, warWindowHigh) with warWindowLow = 1/φ and warWindowHigh = φ, inside which J-cost remains below the boundary value at φ. MODULE_DOC states that the parity band is the J-cost zero set and that the system is maximally unstable at zero cost because the cost surface is at a local minimum.
proof idea
Direct record construction that populates each field of PowerTransitionCert using the corresponding sibling theorems: capabilityCost_at_parity supplies the zero-cost condition at parity, capabilityCost_nonneg supplies non-negativity, warWindowLow_pos and warWindowHigh_gt_one supply the strict bounds, warWindow_ordered supplies the ordering, and capabilityCost_at_phi_boundary supplies the boundary value.
why it matters in Recognition Science
This definition completes the structural theorem (0 sorry, 0 axiom) for the first International Relations module. It instantiates the certificate whose falsifier is any COW dataset analysis showing great-power conflict onset does not cluster near capability ratios in (0.618, 1.618). The construction rests on T5 J-uniqueness and T6 phi fixed point from the forcing chain, with the war window (1/φ, φ) as the quantitative prediction for the parity band.
scope and limits
- Does not establish empirical accuracy of the predicted war window against historical data.
- Does not extend the model beyond great-power capability ratios.
- Does not incorporate alliances, nuclear deterrence, or other geopolitical factors.
- Does not compute numerical probabilities of conflict onset.
formal statement (Lean)
84noncomputable def cert : PowerTransitionCert where
85 cost_at_parity := capabilityCost_at_parity
proof body
Definition body.
86 cost_nonneg := capabilityCost_nonneg
87 war_window_low_pos := warWindowLow_pos
88 war_window_high_gt_one := warWindowHigh_gt_one
89 war_window_ordered := warWindow_ordered
90 boundary_cost := capabilityCost_at_phi_boundary
91