warWindowHigh_gt_one
plain-language theorem explainer
The theorem establishes that the upper edge of the J-cost war window exceeds one. International relations modelers applying Recognition Science to power transitions cite it to confirm the war window extends above capability parity. The proof is a direct one-line wrapper applying the golden ratio inequality one_lt_phi.
Claim. $1 < phi$, where $phi$ is the golden ratio that defines the upper limit of the J-cost war window interval around capability parity.
background
The module formalizes Power Transition Theory via the J-cost function, where the war window is the interval of capability ratios $r$ with low J-cost, specifically $(1/phi, phi)$. warWindowHigh is defined as $phi$. The J-cost satisfies the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$, with zero at parity ($r=1$) producing maximal instability.
proof idea
The proof is a one-line wrapper that applies the lemma one_lt_phi, which establishes $1 < phi$ via algebraic comparison of square roots of 1 and 5.
why it matters
It supplies the war_window_high_gt_one field to the PowerTransitionCert definition that aggregates J-cost properties for the power transition model. This confirms the asymmetric interval around parity using the phi self-similar fixed point from the forcing chain. The module falsifier is any Correlates of War analysis showing no conflict clustering in $(0.618, 1.618)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.