Remark: Local causal certificate versus global proof

Inside a convex developing chart, a straight developed spatial segment of length $R_0$, together with elapsed time $R_0$, is null for the host metric. This is the local certificate recorded in I-B CheungIB (:local-causal). It does not by itself establish a global formula across a missing worldsheet. Proposition prop:distance is a separate global argument for the specific cone with $0<\alpha <1$; its causal curves never pass through $\mathcal{W}$.