proof

P21 Transport gain

Lean spine source

Declarations: P21_transport_gain_prefers_transport_model

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 P21_transport_gain_prefers_transport_model
    (h : Gain TransportModel BaselineModel > 0) :
    Preferred TransportModel BaselineModel :=
  S07_mdl_positive_gain_preferred TransportModel BaselineModel h