warWindow_ordered
plain-language theorem explainer
The theorem establishes that the lower bound of the J-cost war window is strictly less than its upper bound. Analysts extending power transition theory with Recognition Science would cite this ordering to confirm the interval (1/φ, φ) is well-defined before assessing instability at parity. The proof reduces the comparison directly to the quadratic identity for φ combined with a numerical lower bound.
Claim. The lower endpoint of the war window is strictly less than the upper endpoint: $1/φ < φ$, where the war window is the open interval of capability ratios in which J-cost stays below its value at the golden ratio boundary.
background
In this module the war window is the open interval of capability ratios r where the J-cost J(r) ≤ J(φ) ≈ 0.118. The J-cost is the function induced by a multiplicative recognizer on positive ratios, equivalently the cost of a recognition event. The module treats the parity band as the zero set of J-cost and identifies the war window with (1/φ, φ). Upstream, phi satisfies the quadratic identity φ² = φ + 1 and the bound φ > 1.5.
proof idea
The proof unfolds the definitions of warWindowLow and warWindowHigh to obtain the target inequality 1/φ < φ. It introduces the identity φ² = φ + 1, rewrites the reciprocal, applies the division inequality rule, and closes with nlinarith using the bound φ > 1.5.
why it matters
The ordering is required by the PowerTransitionCert, which assembles the structural facts (cost at parity, non-negativity, and window bounds) for the J-cost model of transitions. It supplies the first link from the Recognition Science phi-ladder to international relations, confirming that the parity band (1/φ, φ) forms a proper interval of maximal instability. The module falsifier remains any COW dataset analysis showing no clustering inside (0.618, 1.618).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.