This appendix develops the mathematical results of Section IV of the main paper self-contained. We first prove supporting lemmas, then restate and prove each theorem in full. Throughout, time is measured in seconds, distances in metres, speeds in m/s, and accelerations in m/s$^2$. We assume the kinematic model of Assumptions 1–3: longitudinal motion is governed by $\ddot{x} = a(t)$ with $|a(t)| \leq a_b$ and an actuation delay $t_r$ during which $a(t) = 0$.
Scope of the proofs. The proofs are conventional mathematical proofs, written and checked by hand rather than by a proof assistant. Every result below is a conditional statement: given exact inputs that satisfy the stated assumptions, the conclusion follows. The proofs do not bound perception error, signal-timing uncertainty, or actuator performance, and they do not assert that the measured inputs equal the ground truth. The mathematical guarantee therefore covers the decision logic itself, not the perception chain that feeds it.
Under constant deceleration $a_b$ from initial speed $v_e$, the distance travelled until rest is $v_e^2 / (2a_b)$.
The equation of motion during braking is $\ddot{x} = -a_b$, with initial conditions $x(0)=0$, $\dot{x}(0)=v_e$. Integrating twice: $\dot{x}(t) = v_e - a_b t$ and $x(t) = v_e t - \tfrac{1}{2}a_b t^2$. The vehicle is at rest when $\dot{x}(t_s) = 0$, i.e. $t_s = v_e/a_b$. Substituting:
During the reaction delay $t_r$, during which no braking is applied, the vehicle travels $v_e t_r$ at constant speed.
With $a(t) = 0$ for $t \in [0, t_r]$, $\dot{x} = v_e$ is constant, hence $x(t_r) = v_e t_r$.
□Let $x_\alpha(t)$ be the trajectory obtained by applying deceleration $\alpha \in [0, a_b]$ after the reaction delay. Then the stopping position $x_\alpha(\infty) = v_e t_r + v_e^2/(2\alpha)$ (with the convention that $\alpha = 0$ means “never stops”) is continuous and strictly decreasing in $\alpha$ on $(0, a_b]$.
By Lemma A.1, the braking contribution is $v_e^2/(2\alpha)$, which is continuous and strictly decreasing in $\alpha$ on $(0, a_b]$; the reaction contribution $v_e t_r$ is independent of $\alpha$. Hence the total stopping position is continuous and strictly decreasing in $\alpha$.
□If $d_s > d_{\mathrm{req}}(v_e)$, there exists a deceleration $\alpha^* \in (0, a_b)$ such that the vehicle stops exactly at the stop line: $x_{\alpha^*}(\infty) = d_s$.
By Lemma A.3, the map $\alpha \mapsto x_\alpha(\infty)$ is continuous on $(0, a_b]$, with $x_{a_b}(\infty) = d_{\mathrm{req}}(v_e) < d_s$ and $\lim_{\alpha \to 0^+} x_\alpha(\infty) = +\infty > d_s$. The intermediate value theorem yields $\alpha^* \in (0, a_b)$ with $x_{\alpha^*}(\infty) = d_s$.
□Any trajectory with $|\ddot{x}| \leq a_b$ that begins at $x(0)=0$ with $\dot{x}(0) = v_e$ and applies no braking before $t_r$ satisfies $x(t) \geq x_{\min}(t)$ for all $t$, where $x_{\min}$ is the maximum-braking trajectory.
For $t \in [0, t_r]$ all admissible trajectories coincide ($x = v_e t$). For $t > t_r$, the trajectory with the largest deceleration $a = -a_b$ has the smallest velocity and hence the smallest position at every subsequent time; any smaller deceleration (or acceleration) yields $x(t) \geq x_{\min}(t)$ by monotone comparison of the integrated velocity.
□Theorem 1. Under Assumptions 1–3, the minimum distance within which the ego vehicle can be brought to rest, measured from the instant of decision, is $d_{\mathrm{req}}(v_e) = v_e t_r + v_e^2/(2a_b)$.
The admissible trajectory is the concatenation of the reaction phase (no braking, $t \in [0, t_r]$) and the braking phase (maximal deceleration $a_b$). By Lemma A.2 the reaction phase contributes $v_e t_r$; by Lemma A.1 the braking phase contributes $v_e^2/(2a_b)$. No braking profile can do better: by Lemma A.4, any trajectory that stops must cover at least the distance covered by the maximum-braking trajectory, and delaying braking beyond $t_r$ or braking at less than $a_b$ only increases the stopping distance (Lemma A.3). Hence $d_{\mathrm{req}}(v_e) = v_e t_r + v_e^2/(2a_b)$ is the exact minimum.
□Theorem 2. Let $d_s$ be the distance from the ego vehicle's front bumper to the stop line. A safe stop is physically possible if and only if $d_s > d_{\mathrm{req}}(v_e)$.
($\Rightarrow$) Suppose a safe stop exists: some trajectory $x$ with $|a| \leq a_b$ and $a(t) = 0$ for $t \in [0, t_r]$ satisfies $x(t) < d_s$ for all $t$ and $\dot{x}(t) \to 0$. By Lemma A.4, $x(t) \geq x_{\min}(t)$, hence $d_s > \sup_t x(t) \geq x_{\min}(\infty) = d_{\mathrm{req}}(v_e)$. Thus $d_s > d_{\mathrm{req}}(v_e)$.
($\Leftarrow$) Suppose $d_s > d_{\mathrm{req}}(v_e)$. By Corollary A.1 there exists $\alpha^* \in (0, a_b)$ such that the trajectory stops exactly at $d_s$. This trajectory satisfies $x(t) \leq d_s$ with equality only at the stopping instant, so it is a safe stop. Hence stopping feasibility is equivalent to $d_s > d_{\mathrm{req}}(v_e)$.
□Theorem 3. Let $\epsilon > 0$ be the safety margin. Under the constant-velocity policy, the ego vehicle can clear the intersection before the red phase if and only if $t_c(v_e, d_s) < t_y - \epsilon$.
Under the constant-velocity policy of Assumption 1, the longitudinal position is $x(t) = v_e t$ for $t \geq 0$. The far boundary $d_s + L_i$ is reached exactly at $t = t_c = (d_s + L_i)/v_e$.
($\Rightarrow$) If the vehicle clears before the red phase, then $x(t_y - \epsilon) \geq d_s + L_i$ (Definition 3 requires occupancy only for $t \geq t_y - \epsilon$; clearing means no occupancy thereafter). Since $x$ is strictly increasing, $t_c \leq t_y - \epsilon$. Requiring strict inequality $t_c < t_y - \epsilon$ guarantees that the entire vehicle has exited with margin to spare.
($\Leftarrow$) If $t_c < t_y - \epsilon$, then $x(t_y-\epsilon) = v_e(t_y-\epsilon) > v_e \cdot t_c = d_s + L_i$, so the vehicle has fully crossed the far boundary strictly before the margin instant and hence before the red phase.
□Theorem 4. A CRITICAL warning is necessary and sufficient if and only if $\left( d_s \leq d_{\mathrm{req}}(v_e) \right) \land \left( \frac{d_s + L_i}{v_e} \geq t_y - \epsilon \right)$.
We prove the two implications separately, using the equivalence of stopping feasibility (Theorem 2) and clearance feasibility (Theorem 3) under Assumption 1.
Sufficiency. Assume $d_s \leq d_{\mathrm{req}}(v_e)$ and $t_c \geq t_y - \epsilon$. By Theorem 2, no safe stop exists; by Theorem 3, no safe clearance exists. Consider any admissible trajectory. If it never crosses the stop line, it must eventually stop (Assumption 1 leaves only braking as a way to remain bounded); but stopping is impossible without crossing the line by the first conjunct, contradiction. Therefore every trajectory crosses the stop line, and since it cannot clear before $t_y - \epsilon$ (second conjunct), it occupies the box $[d_s, d_s+L_i]$ at some $t \geq t_y - \epsilon$. By Definition 3 the vehicle is blocked under every admissible trajectory, so a CRITICAL warning is necessary.
Necessity. Suppose a CRITICAL warning is required, i.e., blockage is unavoidable for every admissible trajectory. If a safe stop were possible ($d_s > d_{\mathrm{req}}(v_e)$), then by Theorem 2 the driver could avoid blockage by stopping; contradiction. Hence $d_s \leq d_{\mathrm{req}}(v_e)$. Similarly, if a safe clearance were possible ($t_c < t_y - \epsilon$), the driver could avoid blockage by clearing; contradiction. Hence $t_c \geq t_y - \epsilon$. Both conjuncts hold, so the criterion is also sufficient for the warning.
□With the constants of Table I and $t_y = 3.5$ s, the clearance boundary is $d_s = 2.7v_e - 16$ and the stopping boundary is $d_{\mathrm{req}}(v_e) = v_e + v_e^2/8$. Their difference is $d_{\mathrm{req}}(v_e) - (2.7v_e - 16) = v_e^2/8 - 1.7v_e + 16$, a convex quadratic with discriminant $(-1.7)^2 - 4(1/8)(16) = 2.89 - 8 = -5.11 < 0$ and positive leading coefficient. Hence $d_{\mathrm{req}}(v_e) > 2.7v_e - 16$ for all $v_e$, so the dilemma band $\{ (v_e, d_s) : 2.7v_e - 16 \leq d_s \leq d_{\mathrm{req}}(v_e) \}$ is non-empty for every $v_e \geq 5.93$ (below which the lower bound is negative and the band extends to $d_s = 0$).
□Theorem 5. If $t_c^{\mathrm{eff}} \geq t_y - \epsilon$ and $d_l < d_{\mathrm{req}}(v_e)$, the ego vehicle will become trapped behind the leader and block the intersection.
Let $x_{\mathrm{lead}}(t)$ denote the leader's longitudinal position. The collision-avoidance constraint is $x_{\mathrm{ego}}(t) \leq x_{\mathrm{lead}}(t) - \Delta$ for some positive stand-off $\Delta$; the analysis is insensitive to $\Delta \geq 0$, so take $\Delta = 0$ for the bound. The leader's clearance time is $t_{\mathrm{lead}} = (d_l + L_i)/v_l$, which is exactly $t_c^{\mathrm{eff}}$ of Definition 7 (the small constant $\delta$ prevents division by zero when $v_l = 0$ and makes the inequality strict in the border case). If $t_c^{\mathrm{eff}} \geq t_y - \epsilon$, the leader occupies the box at $t = t_y - \epsilon$, i.e., $x_{\mathrm{lead}}(t_y-\epsilon) < d_l + L_i$. By the collision-avoidance constraint, $x_{\mathrm{ego}}(t_y-\epsilon) \leq x_{\mathrm{lead}}(t_y-\epsilon) < d_l + L_i \leq d_s + L_i$ (using $d_l \leq d_s$), so the ego has not cleared the far boundary by the margin instant; moreover the ego has already crossed the stop line, since it cannot stop (see below). Hence the ego is blocked (Definition 3).
It remains to show the ego cannot abort. At the decision instant the gap to the leader is $d_l < d_{\mathrm{req}}(v_e)$. By Theorem 2, any braking trajectory that halts the ego does so at a position at least $d_{\mathrm{req}}(v_e)$ beyond the decision point, i.e., at or beyond the leader's current position; since the leader is moving forward (or is stopped), the ego cannot come to rest strictly behind the leader without violating the collision-avoidance constraint. The ego therefore cannot stop in time and must proceed, which we have shown leads to blockage.
□Theorem 6. Let $d_a$ be the distance to an adjacent vehicle with an active turn signal. If $t_i < t_y$ and $d_a < d_{\mathrm{req}}(v_e)$, then the ego must issue a warning.
By Definition 8, the intruding vehicle crosses the lane boundary at $t = t_i = W_l/|v_{\mathrm{lat}}|$. If $t_i < t_y$, the intrusion occurs strictly before the signal transition. At the intrusion instant, the longitudinal separation between ego and intruder is at most $d_a$ (the intruder is ahead at the ego's lane entry point; if it enters behind the ego the situation is not safety-relevant, so consider the ahead case). Since $d_a < d_{\mathrm{req}}(v_e)$, by Theorem 2 the ego cannot brake to a halt before reaching the intruder's position. Two cases arise:
Case 1 (ego brakes): the ego cannot stop before the intruder, so it either collides with the intruder or, if the intruder is beyond the stop line, stops beyond the stop line and occupies the box. Both outcomes violate Definition 3 or safe operation.
Case 2 (ego proceeds): the intruder now occupies the ego's lane and acts as a slow lead vehicle; by Theorem 5 with the intruder as leader (its gap $d_a < d_{\mathrm{req}}(v_e)$ and its speed implying a clearance failure), blockage follows.
In either case the kinematic constraints are violated and a warning is required.
□Let $\ell^*$ be the output of evaluate_safety on any scene.
Then $\ell^* = \max_{\text{severity}} \{\ell_r\}$ over all rules $r$ that fire,
where the severity order is
SAFE $<$ CAUTION $<$ WARNING $<$ CRITICAL; if no
rule fires, $\ell^* = $ SAFE.
The pipeline evaluates the rules in the fixed order
[rule_light, rule_dilemma, rule_lead, rule_cutin, rule_stale], and
find_map returns the first element that evaluates to
Some. Inspection of each rule shows its maximum severity level:
rule_light and rule_dilemma can emit
CRITICAL (the highest); rule_lead can emit CRITICAL
(sub-rule 3a) or WARNING; rule_cutin emits at most
WARNING; rule_stale emits at most CAUTION. Because
the pipeline order is non-increasing in the severity bound of each rule, the
first firing rule carries the maximum severity among all firing rules. If none
fires, unwrap_or(Safe) returns SAFE.
If LightState::Red, the output is CRITICAL regardless of
all other inputs.
rule_light maps Red to CRITICAL and is
evaluated first; by Lemma A.5 the output is the maximum severity, i.e.,
CRITICAL.