P32 Cooperativity threshold

Declarations: P32_kappa_threshold

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P32_kappa_threshold
    (b p rho c : Int)
    (_hc : 0 < c) :
    c < b * p * rho ↔ KappaNumerator b p rho > c := by
  unfold KappaNumerator; omega