arah2/docs/ALT-DIRECTION-SPLIT-EXPERIMENT.md

# Direction-split ALT: proof gate (research branch only)

Status: P-1 and P-2 proved for **pair-restricted domain and independent A* stopping** below; measurements pending. 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.

## Experiment and verdict

Pending runner, adversarial oracle checks and paired host measurements. The 8 ms Worker budget is **NOT MEASURED** here; no synthetic speedup or host-local result can certify the Worker free-plan gate.