12 KiB
Direction-split ALT: proof gate (research branch only)
Verdict: NO-GO for deployment and the 8 ms Worker budget. P-1 and P-2 proved for pair-restricted domain and independent A stopping* below; the measured branch-only implementation is 4.35× slower at paired p95 than the original control despite fewer expansions. This is not a proof for the shipped Ikeda sum-of-tops rule with asymmetric families.
Graph and tables
Let c(u,v) be the stored finite nonnegative edge seconds, for directed CSR edge u→v only when bit0 is clear. Neither search traverses bit0 edges, even in reverse. Let q>0 be landmarkQuantumS, ĉ(u,v)=floor(c(u,v)/q) and D be shortest path in integer quanta. Row-major to[ℓ*n+v]=D(v,ℓ), from[ℓ*n+v]=D(ℓ,v); 0xffff means unreachable, never the number 65535. All finite stored values are at most 65000. Distances in seconds obey qD triangle inequalities against real c since qĉ≤c.
For this fixed query o→g, select to-columns T={ℓ | to[ℓ*n+g] finite} and from-columns F={ℓ | from[ℓ*n+o] finite}. If to[o] is sentinel for any ℓ in T, or from[g] is sentinel for any ℓ in F, return unreachable: otherwise an o→g path would respectively concatenate with g→ℓ or ℓ→o. Define the search domain S as nodes where to[ℓ*n+v] is finite for every ℓ in T and from[ℓ*n+v] finite for every ℓ in F. Exclude nodes outside S in both traversals. Every vertex of every actual o→g path belongs to S: its suffix reaches g then ℓ in T; its prefix is reached from o, which ℓ in F reaches. Thus domain restriction cannot remove any solution. It can remove dead-end branches and can change landmark shortest distances, but the original full-graph labels still satisfy the required triangle inequalities for every remaining edge. When T or F is empty the respective condition is vacuous and haversine remains available. Both endpoints are in S after the early reachability checks.
P-1, independently: on S use
h_f(v)=max(haversine(v,g)/vmax, 0, max_{ℓ∈T} q*(to[ℓ*n+v]-to[ℓ*n+g]));
h_b(v)=max(haversine(v,o)/vmax, 0, max_{ℓ∈F} q*(from[ℓ*n+v]-from[ℓ*n+o])).
For each traversable u→v inside S, to[u]≤ĉ(u,v)+to[v] implies h_f(u)≤c(u,v)+h_f(v) for each to-family. Independently from[v]≤from[u]+ĉ(u,v) implies h_b(v)≤c(u,v)+h_b(u) for each from-family on the reverse search edge v→u. Spherical haversine obeys both inequalities if real edge seconds lower-bound its endpoint chord at vmax; use the same maxSpeedKmh scaling as shipped A*, and require this graph assumption on test fixtures. The max of individually consistent families is consistent. Both heuristics vanish at their targets; by path telescoping they are admissible on S. Family values can be signed; max with zero/haversine keeps h nonnegative. Active sets T and F are query-scoped and unchanged across each edge within S. There is no numeric sentinel subtraction or per-node family skip.
Clean-column selection on the actual 0/24-clean binary gives 0 active landmarks globally. This domain construction instead selects endpoint-reachable columns for each query and excludes their holes before search: giant-component queries can activate 24 columns despite sentinel island cells; island queries may activate none. It cannot be replaced by evaluating a family only at the finite end of a cross-edge: if to[u]=100, to[v]=0xffff, and u→v costs 1, returning 100 at u and fallback 0 at v violates forward consistency. Likewise from[u]=0xffff, from[v]=100 on u→v violates reverse consistency if the family is skipped at u. These edges are excluded when the corresponding column is selected. If they lie on an actual path to g or from o respectively, the endpoint selection/concatenation proves they cannot occur; if the column is not selected it contributes nowhere.
P-2: independent frontier lower bound, NOT the BH sum rule
Maintain actual seconds distances df from o, db to g on the reversed induced graph, with keys Kf(v)=df(v)+h_f(v) and Kb(v)=db(v)+h_b(v). These keys are not opposite potentials; do not add their minima or apply a v-independent offset. There is no v-independent cancellation of h_f(v)+h_b(v) for unrelated directed families: for example, a oneway chain o→a→g may have h_f(a)=1,h_b(a)=1, while a parallel dead-end has either bound 0 or a very large bound. Instead use the conservative stop min_valid(Kf)≥U or min_valid(Kb)≥U, where U is the best real discovered complete route (node meet df(v)+db(v) or traversable bridge df(u)+c(u,v)+db(v)). Strict floating-point tolerance must not weaken the inequality; all emitted seconds come from a traversable reconstructed path, not from subtracting potentials.
For each side, consistency gives reduced edge c+h(next)-h(current)≥0 on that side, so settling min key fixes its actual distance; duplicate heap entries whose stored g differs from current g or whose vertex is closed are stale and must be discarded before reading the frontier minimum. Better g to a closed vertex is impossible under this premise; assert/fail loud if it occurs (or reopen if consistency is abandoned, but then this proof and stop do not apply). For a hypothetical route P of cost <U, consider the first vertex on P not yet forward-settled. Its predecessor is settled (or it is o); relaxation inserted a tentative g no larger than P's prefix, and admissibility bounds Kf≤cost(P)<U. Its live entry must still be in the forward heap. Therefore a forward minimum ≥U excludes P; the symmetric argument applies to the backward minimum. A bridge meet can only lower U via a genuine chain. If a frontier empties after stale removal, it has exhausted its induced reachable set: if no complete path was found, return null; if U finite the same first-unsettled argument shows U optimal. No assumption of simultaneous frontier growth or of a sum-of-minima bound is needed. Signed raw family differences are harmless since h is nonnegative and keys use real g; each direction has its own independent reduction and no shared potential.
Hand checks: oneway ring 0→1→2→0 with a forbidden bit0 mirror 1→0, forward to[0] labels (0,2,1) for unit edges and backward from[0] (0,1,2); all allowed edges respect their respective oriented inequalities while mirror never relaxes. Bridge A→B costing 1 with no return, anchor in A: from[B] finite and to[B] sentinel; anchor in B: to[A] finite and from[A] sentinel. For a query A→B, applicable columns require origin/goal finite and S retains the bridge; B→A fails the endpoint reachability check and returns null. Disconnected anchored island vs unanchored component has sentinel endpoint(s); a route wholly in the unanchored component retains an empty active set and can still succeed, while a cross-component route is null. In all three examples, cross-boundary edges are excluded only if they cannot be on an o→g path.
Measured experiment and verdict
Branch-only routing/scripts/experiment-alt-direction-split.mjs implements these independent A* keys, single-vertex meets, stale-key pruning and a query-domain mask. New suite routing/test/alt-direction-split-experiment.test.mjs tests every pair across one-way rings with blocked mirrors/spurs and equal costs, both directions of one-way bridges, isolated anchored/unanchored islands, endpoints and interior 0xffff cells, mixed columns and a finite→sentinel cross-edge per-node skip adversary. Each checks independent O(V²) Dijkstra seconds, null classes and legal reconstructed edges. On real graph, sweepOracle uses the exact 200 compared snapped cross-metro pairs (seed 0x08f1, 600 draws, 12 km minimum, 120 rejected snap misses) and independent heap-Dijkstra; 182 routed, 18 unreachable; suboptimal 0, oracle-mismatch 0, class-break 0 at symmetric ±1e-6 s. No synthetic or real pair disproved this conservative stop; the counterexample to naive per-node masking is above, not a measured result of this runner.
Measured 2026-10-26 on HAFu, Node v24.18.0, Linux, binary SHA-256 366e1be2ca270e5e67cb0debc98887b6dcb66f29849747d59f4e0e58739ec5b8, ARG2 311,361 nodes / 677,126 edges. This checkout's routing/data/kl-roadgraph.v1.bin is an existing read-only symlink to the other checkout; no binary modifications. Reproduction: node routing/scripts/experiment-alt-direction-split.mjs. The experimental instrumented comparison used an automatically removed temporary source-identical shipped clone with only two settled counters injected, and also timed original unmodified routeAstar on the same snapped endpoints. Clone/original seconds agreed to ±1e-6 for each routed sample. A dedicated warm-up (not included) took experimental 0.935 ms, original 20.005 ms, clone 27.471 ms.
The seed 0x08a1 100-pair, ≥12 km extended draw produced 41 snap misses, 6 unreachable and 53 routed; each routed pair was measured twice, reversed run order across rounds (106 routed measurements each). Misses are outside routed p95; each pair was compared at identical snapped endpoints. Times are Node hrtime wall elapsed for search call on this host, not Cloudflare Worker CPU instrumentation, so they cannot establish a Worker CPU PASS.
| Search | n | Median ms | Mean ms | p95 ms | Total settled expansions (106 calls) |
|---|---|---|---|---|---|
| Direction-split / domain-mask experimental | 106 | 150.845 | 197.490 | 516.778 | 9,958,938 (forward/backward split NOT MEASURED) |
| Source-identical isolated shipped clone + settled counters | 106 | 73.588 | 72.331 | 129.327 | 14,037,662 (6,764,880 fwd / 7,272,782 bwd) |
Original shipped haversine-only routeAstar, unmodified |
106 | 73.619 | 71.864 | 118.923 | NOT MEASURED directly (clone is expansion proxy) |
Experimental/clone expansion ratio 0.709×; experimental/original shipped paired p95 4.35× slower despite fewer settles. The experiment selected an average of 22.64 to- and 18.87 from-columns per routed call (2400/106 and 2000/106 respectively); shipped has 0/24 clean columns and is the actual haversine-only control. No claim of runtime speedup. Search-scoped domain scanning, per-vertex Math.max, and heaps/allocations in this research runner may account for some overhead, but optimization is NOT demonstrated and no performance claim is transferable to an optimized Worker implementation.
Control gates unchanged: npm run routing:test 85 passed, 0 failed, including shipped A1/625; npm run routing:typecheck PASS. node routing/scripts/measure-optimality-gate.mjs D-03 frozen record PASS (53 routed equal, 6 unreachable, 41 unsnappable; 0 class breaks). node routing/scripts/measure-route-cpu.mjs --extended shipped-control FAIL: 53 routed/100, p95 127.933 ms, >8 ms; 47 misses printed separately. Early test invocation lacked installed dependencies and failed L2/tsc; npm ci --ignore-scripts --no-audit --no-fund installed local dependencies, and both gates then passed; no source changes to those gates.
Proof status: P-1 PASS for induced pair domain; P-2 PASS for the conservative independent-frontier stopping bound, NOT a proof of asymmetric Ikeda sum stopping. Oracle status: 0 violations in synthetic exhaustive and real seeded runs. Budget status: local original control FAIL on 8 ms test; candidate local p95 FAIL; representative free-plan Worker 8 ms NOT MEASURED. Recommendation: NO-GO on integration; retain original A*, baseline and bot/web unchanged. A later, separately approved investigation could evaluate typed-array/precomputed component labels and a separately proved stronger meet bound, then rerun identical oracle and actual Worker-host CPU gates. No merge or Worker-budget retirement is justified.