A Lean proof that the low-dissipation efficiency-at-given-power bound is increasing in the asymmetry parameter (elementary; the engine-level bound is already known)

In the phenomenological low-dissipation Carnot engine model, Ma, Xu, Dong and Sun define an upper bound on the efficiency at given normalised power and dissipation asymmetry ζ ∈ [−1,1] (their Eq. (13)); they state that it increases with ζ, call the analytic proof “tedious and difficult” and check it numerically. We prove in Lean 4 that the root form of this bound (the positive root of the quadratic from their tangency condition) is strictly increasing in ζ on the whole box 0<ηC<1, P̃∈(0,1], ζ∈[−1,1] (Tier A, statement lock owed). The proof is elementary. We also machine-check their universal bound Eq. (1) for every engine of their Eqs. (3)–(4); that bound is a known result with analytic proofs (Ma and Fu, arXiv:2411.03849; Zhai, arXiv:2605.02732), so only the machine check is new. To our knowledge there is no earlier machine-checked proof of either statement; only the ζ-monotonicity lacks a published analytic proof (search not systematic). The identification of the root form with Eq. (13) as printed is not in Lean (symbolic identity up to the sign branch plus 50–60-digit numerics, Tier C). What this is NOT. Not a first proof of Eq. (1); not a statement about any real engine or power plant; not a proof that the bound is attained (it is a valid upper bound, not attained in general; Zhai, Yue and Sun, arXiv:2509.07721, give a tighter exact bound), nor that every engine with asymmetry ζ satisfies the bound (derivation and numerics only); the bound is not tight. Limitations. Independently audited by a different AI agent instance (AUDIT.md, ACCEPT_WITH_CORRECTIONS, nine corrections applied); no human audit and no statement lock (owed). The producer's preregistered transcription of Eq. (13) was wrong (a term inside instead of outside the square root) and was corrected; the original disagreement is kept in the logs. Unverified: the Lean lemma “engine with asymmetry ζ ⇒ η/ηC ≤ bound”; the + branch choice (numerical only); P̃=0 and the endpoints Mh=0, Mc=0; a Lean example that the engine-level hypotheses can be met; Esposito et al. 2010 not re-read. The Lean control pert_eta_not_mono is weak. The Elenchus ledger gate exits with code 1 (0 blocking findings, 3 flags LEDGER_UNAUDITED_TIER_A, one per Tier A row).