`cert`

definition

show as: view math explainer →

module: IndisputableMonolith.InternationalRelations.PowerTransitionFromJCost
domain: InternationalRelations
line: 84 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.InternationalRelations.PowerTransitionFromJCost on GitHub at line 84.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  81  war_window_ordered : warWindowLow < warWindowHigh
  82  boundary_cost : capabilityCost phi 1 = phi - 3 / 2
  83
  84noncomputable def cert : PowerTransitionCert where
  85  cost_at_parity := capabilityCost_at_parity
  86  cost_nonneg := capabilityCost_nonneg
  87  war_window_low_pos := warWindowLow_pos
  88  war_window_high_gt_one := warWindowHigh_gt_one
  89  war_window_ordered := warWindow_ordered
  90  boundary_cost := capabilityCost_at_phi_boundary
  91
  92theorem cert_inhabited : Nonempty PowerTransitionCert := ⟨cert⟩
  93
  94end
  95end PowerTransitionFromJCost
  96end InternationalRelations
  97end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.