Table G.1, OA p. 24 — optimal prices when independent repair costs at least δ
ProvedRightRepair.Equilibrium.table_G1Suppose and the standing assumptions hold. Table G.1 gives three optimal outcomes as production cost rises: no repair for , partial repair for , and full repair for . The new and used prices and repair probabilities in each case are exactly the Table G.1 formulas, and each outcome attains at least the profit of every admissible competing equilibrium.
In the partial-repair interval, , , and . Its repair probability is strictly between zero and one when .
Formalization Note At the printed left endpoint , , so the strict claim in Table G.1 is made only in the open interval. The statement still asserts optimality at that endpoint. Assumption 1 excludes the table's row. The nonnegative unit-cost pins, the zero-price excess-supply equilibrium corner, and the none encoding of are part of the shared model.
import Mathlib import Definitions.Def_RightRepair_Equilibrium_Setting
namespace RightRepair.Equilibrium
theorem table_G1 (P : Params) (hP : Standing P)
(hI : P.δ ≤ P.cI) :
(P.c < cLow P →
OptimalOutcome P (pnNo P) none (puNo P) 0) ∧
(cLow P ≤ P.c → P.c < cBar P →
OptimalOutcome P (pnNo P) (some ((P.δ + P.cM) / 2))
((P.δ + P.cM) / 2)
(alphaHat P (pnNo P) ((P.δ + P.cM) / 2))) ∧
(cLow P < P.c → P.c < cBar P →
0 < alphaHat P (pnNo P) ((P.δ + P.cM) / 2) ∧
alphaHat P (pnNo P) ((P.δ + P.cM) / 2) < 1) ∧
(cBar P ≤ P.c →
OptimalOutcome P (pnFull P) (some 0) (puFull P) 1) := by sorry
end RightRepair.Equilibrium
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.