warWindow_ordered
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.
claimThe 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 in Recognition Science
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).
scope and limits
- Does not prove empirical clustering of conflicts near parity ratios.
- Does not derive the explicit form of J-cost from the forcing chain.
- Does not extend the model beyond two-state transitions.
- Does not quantify probability density inside the window.
formal statement (Lean)
63theorem warWindow_ordered : warWindowLow < warWindowHigh := by
proof body
Term-mode proof.
64 unfold warWindowLow warWindowHigh
65 -- phi⁻¹ < phi since phi > 1 implies phi * phi > 1 > phi * phi⁻¹ = 1... direct:
66 have hphi_sq : phi ^ 2 = phi + 1 := phi_sq_eq
67 rw [inv_eq_one_div]
68 rw [div_lt_iff₀ phi_pos]
69 nlinarith [phi_gt_onePointFive]
70
71/-- At the φ-boundary, J-cost equals the canonical recognition quantum. -/