warWindowLow_pos
The theorem establishes strict positivity of the lower war window bound in the J-cost model of power transitions. International relations modelers applying Recognition Science cite it when assembling certificates that the capability ratio interval begins above zero. The proof is a one-line wrapper applying inv_pos.mpr to the known positivity of phi.
claim$0 < phi^{-1}$, where $phi^{-1}$ is the lower edge of the war window interval $(1/phi, phi)$ in the J-cost formulation of capability ratios.
background
The module applies Recognition Science to Power Transition Theory, predicting that inter-state conflict probability peaks at capability parity (ratio = 1), the zero set of the J-cost function. The war window is the interval of ratios r where J(r) ≤ J(phi) ≈ 0.118, specifically r ∈ (1/phi, phi). warWindowLow is defined as phi inverse, the lower capability ratio threshold. This rests on the constants module where phi is the self-similar fixed point from the forcing chain (T5-T6). Upstream, warWindowLow is introduced as the capability ratio in (1/φ, φ).
proof idea
The proof is a one-line wrapper that applies inv_pos.mpr to phi_pos.
why it matters in Recognition Science
This positivity result supplies the war_window_low_pos field required by the PowerTransitionCert, which packages J-cost nonnegativity at parity together with the ordered war window bounds. It supports the RS prediction that the parity band is the J-cost zero set and aligns with the phi-ladder and eight-tick octave in the forcing chain. The module falsifier remains any empirical analysis of the Correlates of War dataset showing that great-power conflict onset does not cluster near capability parity ratios in (0.618, 1.618).
scope and limits
- Does not prove positivity of the upper war window bound.
- Does not derive the J-cost function or locate its zero set.
- Does not perform empirical testing against historical conflict data.
- Does not generalize the model to n-state systems.
formal statement (Lean)
58theorem warWindowLow_pos : 0 < warWindowLow :=
proof body
One-line wrapper that applies inv_pos.mpr.
59 inv_pos.mpr phi_pos
60