proof

P20 Intentional MDL gain

Lean spine source

Declarations: P20_positive_intentional_gain_prefers_intentional

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 P20_positive_intentional_gain_prefers_intentional
    (h : Gain Intentional Mechanistic > 0) :
    Preferred Intentional Mechanistic :=
  S07_mdl_positive_gain_preferred Intentional Mechanistic h

/-- C-GT (P21): positive transport gain makes the transport model preferred. -/