proof

P21 Transport gain

Lean spine source

Declarations: P21_transport_gain_prefers_transport_model

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