(3) — asymmetric positioning equilibrium
ProvedPPDifferentiation.ShortRun.asymmetric_positionsFor , suppose only A uses personalized pricing. A is the targeting follower and B is the uniform-price leader. The positioning subgame has an equilibrium at
The positioning comparison includes moves to every real point, including a move across the rival's location. It provides the positions used in the asymmetric implementation-payoff cells.
Formalization Note This is a weak equilibrium: A can move to the reflected position and tie its equilibrium gross profit. At coincident positions the leader may have multiple optimal prices, so the predicate chooses an optimal continuation after a deviation. The source optimizes over ordered locations; the statement checks the full real-location game.
import Mathlib import Definitions.Def_PPDifferentiation_ShortRun_Setting
namespace PPDifferentiation.ShortRun
theorem asymmetric_positions (t : ℝ) (ht : 0 < t) :
IsPosEqAS t (-1/2) (1/2) := by sorry
end PPDifferentiation.ShortRun
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.