proof

P10 B-IQ upper bound

Lean spine source

Declarations: P10_biq_upper_bound

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P10_biq_upper_bound
    (Ipred Ictrl Hmem Surprise Csens Cact beta gamma : Int)
    (hpred : Ipred ≤ Csens)
    (hctrl : Ictrl ≤ Cact)
    (hmem : 0 ≤ beta * Hmem)
    (hsurp : 0 ≤ gamma * Surprise) :
    BIQ Ipred Ictrl Hmem Surprise beta gamma ≤ Csens + Cact := by
  unfold BIQ; omega

/-- Integer Markov-blanket/B-IQ profile: predictive and control information are
    bounded by sensory/action channel capacities, while memory/surprise penalties
    are nonnegative. This keeps the BIQ-paper arithmetic separate from the
    empirical bridge that a deployed system's measured blanket satisfies it. -/