capabilityCost_at_parity
plain-language theorem explainer
The theorem establishes that J-cost on the relative capability ratio vanishes at exact parity. International relations theorists modeling power transitions within Recognition Science would cite this to anchor the zero-cost point at capability ratio one. The proof is a one-line wrapper that unfolds the capabilityCost definition, cancels the ratio via division by self, and invokes the lemma that Jcost at unity is zero.
Claim. For any nonzero real number $c$, the J-cost of the relative-capability ratio $c/c$ is zero: $J(1)=0$, where $J(x)=((x-1)^2)/(2x)$.
background
The module develops Power Transition Theory by expressing inter-state instability via J-cost on capability ratios. Upstream, Jcost is defined as $J(x)=((x-1)^2)/(2x)$ and satisfies Jcost at unity equals zero, per the lemma Jcost_unit0. The sibling definition sets capabilityCost to Jcost of the ratio of rising to incumbent capabilities. In the local setting, the parity threshold corresponds to the J-cost zero set, interpreted as a recognition equilibrium at a local minimum of the cost surface. The module falsifier is any empirical analysis of the Correlates of War dataset showing that great-power conflict does not cluster near capability ratios in (0.618, 1.618).
proof idea
This is a one-line wrapper. It unfolds the definition of capabilityCost to obtain Jcost of the ratio c over c, rewrites the ratio to one using the nonzero hypothesis, and applies the upstream lemma Jcost_unit0.
why it matters
The declaration supplies the cost_at_parity field of the PowerTransitionCert structure defined downstream in the same module. It fills the structural claim that the parity band is the J-cost zero set, anchoring the recognition equilibrium at ratio one and aligning with J-uniqueness in the framework. This closes the basic parity case without touching open questions on war-window boundaries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.