capabilityCost_at_phi_boundary
plain-language theorem explainer
capabilityCost_at_phi_boundary shows that the J-cost for a capability ratio of the golden ratio φ equals φ minus 3/2. International relations analysts using power transition models would cite this to define the upper edge of the instability window. The proof is a one-line wrapper that unfolds the capabilityCost definition and applies the Jcost_phi_val lemma.
Claim. The J-cost of the relative capability ratio $φ$ (rising power capabilities over incumbent) equals $φ - 3/2$.
background
In this module, capabilityCost is defined as Jcost applied to the ratio of rising to incumbent capabilities. The upstream lemma Jcost_phi_val states that J(φ) = φ - 3/2 exactly, derived from φ² = φ + 1. The module context is Power Transition Theory recast in Recognition Science terms, where the war window is the interval of ratios (1/φ, φ) in which J-cost is bounded by this value, with zero cost at parity ratio 1.
proof idea
The proof is a one-line wrapper. It unfolds capabilityCost to reveal the Jcost call on the ratio φ/1, then uses simp to reduce and applies the exact lemma Jcost_phi_val from Constants.
why it matters
This theorem supplies the boundary cost value consumed by the PowerTransitionCert record, which bundles the cost properties for the power transition model. It completes the quantitative specification of the J-cost band in the Recognition Science treatment of international relations, consistent with the phi self-similar fixed point. The module falsifier remains any empirical disconfirmation from the Correlates of War dataset outside the predicted interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.