pith. machine review for the scientific record. sign in
def definition def or abbrev high

warWindowHigh

show as:
view Lean formalization →

The definition sets the upper endpoint of the J-cost war window to the golden ratio φ. International-relations modelers applying recognition cost to power transitions cite it to bound the interval of elevated conflict probability around capability parity. It is introduced by direct assignment to the phi constant imported from the constants module.

claimThe upper endpoint of the J-cost war window is defined to be the golden ratio $φ$.

background

The module develops a recognition-science version of power transition theory. The J-cost function J(r) = (r + r^{-1})/2 - 1 vanishes at capability ratio r = 1 (recognition equilibrium) and the war window is the band (1/φ, φ) in which J(r) ≤ J(φ) ≈ 0.118. Conflict probability is predicted to peak inside this band because the cost surface reaches a local minimum at parity.

proof idea

The declaration is a direct definition that assigns the constant phi to warWindowHigh. No lemmas or tactics are applied.

why it matters in Recognition Science

This supplies the upper limit required by PowerTransitionCert to certify the three war-window properties (low positive, high greater than one, and ordered). It implements the quantitative RS prediction that the J-cost band is (φ^{-1}, φ), connecting the international-relations application to the core T6 result that phi is the self-similar fixed point. The module falsifier is any Correlates of War analysis showing great-power conflict onset does not cluster inside (0.618, 1.618).

scope and limits

formal statement (Lean)

  56def warWindowHigh : ℝ := phi

proof body

Definition body.

  57

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.