warWindowHigh
plain-language theorem explainer
The definition sets the upper endpoint of the J-cost war window to the golden ratio φ. International-relations modelers applying recognition cost to power transitions cite it to bound the interval of elevated conflict probability around capability parity. It is introduced by direct assignment to the phi constant imported from the constants module.
Claim. The upper endpoint of the J-cost war window is defined to be the golden ratio $φ$.
background
The module develops a recognition-science version of power transition theory. The J-cost function J(r) = (r + r^{-1})/2 - 1 vanishes at capability ratio r = 1 (recognition equilibrium) and the war window is the band (1/φ, φ) in which J(r) ≤ J(φ) ≈ 0.118. Conflict probability is predicted to peak inside this band because the cost surface reaches a local minimum at parity.
proof idea
The declaration is a direct definition that assigns the constant phi to warWindowHigh. No lemmas or tactics are applied.
why it matters
This supplies the upper limit required by PowerTransitionCert to certify the three war-window properties (low positive, high greater than one, and ordered). It implements the quantitative RS prediction that the J-cost band is (φ^{-1}, φ), connecting the international-relations application to the core T6 result that phi is the self-similar fixed point. The module falsifier is any Correlates of War analysis showing great-power conflict onset does not cluster inside (0.618, 1.618).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.