capabilityCost_nonneg
plain-language theorem explainer
The theorem shows that capabilityCost, defined as J-cost on the ratio of rising to incumbent capabilities, is non-negative whenever both inputs are positive. International relations modelers extending Organski's power transition theory to Recognition Science would cite it to anchor stability claims at parity. The proof is a one-line term wrapper that unfolds the definition and applies an upstream Jcost non-negativity lemma to the positive ratio r/i.
Claim. If $r > 0$ and $i > 0$, then $0 ≤ J(r/i)$, where $J(x) = (x + x^{-1})/2 - 1$ is the J-cost function.
background
In this module the capabilityCost definition applies the J-cost function directly to the relative-capability ratio (rising power capabilities divided by incumbent power capabilities). Upstream lemmas establish that J(x) ≥ 0 for every x > 0 by the AM-GM inequality x + 1/x ≥ 2, which rearranges to the required non-negativity after algebraic simplification. The module itself is the first International Relations component in the Recognition Science codebase and translates Organski-Lemke power transition theory into J-cost language, identifying the parity threshold (ratio = 1) with the J-cost zero set and the war window with the interval (1/φ, φ).
proof idea
The proof is a term-mode one-liner. It unfolds capabilityCost to obtain Jcost (r / i), then invokes the lemma Jcost_nonneg on the strictly positive quantity produced by div_pos hr hi.
why it matters
The result is invoked inside the PowerTransitionCert constructor in the same module, supplying the required non-negativity field alongside parity cost and war-window bounds. It thereby completes one structural piece of the module's claim that the J-cost surface governs conflict probability near capability parity. Within the broader framework it rests on the non-negativity property of J (T5 J-uniqueness) and supports the quantitative prediction that the parity band is the J-cost zero set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.