Asymmetric rendezvous on the line: $R^a = 13/4$ (Alpern–Gal)

Proved

SymmetricRendezvousLine.asymmetric_rendezvous_value_eq_thirteen_quarters

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

rendezvoussearch-games

Theorem (Alpern–Gal, 1995). If the two players may use different strategies, the infimum expected meeting time is $3.25$ :

R^a=\inf_{S_1,S_2}E(S_1,S_2)=\frac{13}{4}.

Here the setting is the same as for the symmetric problem: players start at distance $2$ (player I at $0$ , player II at $2$ ), each player's forward direction is an independent fair coin, speeds are at most $1$ , and $E(S_1,S_2)$ is the expected first meeting time when player I uses $S_1$ and player II uses $S_2$ independently.

Since every symmetric strategy pair $(S,S)$ is admissible here, $R^a\le R$ ; this value is the benchmark against which the cost of the symmetry constraint is measured.

Preamble

import Definitions.Def_SymmetricRendezvousLine_defs

Formal statement

namespace SymmetricRendezvousLine

theorem asymmetric_rendezvous_value_eq_thirteen_quarters :
    asymmetricRendezvousValue = 13 / 4 := by sorry

end SymmetricRendezvousLine

Source

Open Problem Garden, 'Rendezvous on a line' (posted by mdevos, 2007), http://www.openproblemgarden.org/op/rendezvous_on_a_line ("Alpern and Gal [AG] have shown that the inf expected meeting time is 3.25"); S. Alpern, S. Gal, Rendezvous search on the line with distinguishable players, SIAM J. Control Optim. 33(4) (1995) 1270-1276.

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Asymmetric rendezvous on the line: Ra=13/4R^a = 13/4Ra=13/4 (Alpern–Gal)

Asymmetric rendezvous on the line: $R^a = 13/4$ (Alpern–Gal)