fix(08-05): D-03 optimality gate green — fromTable families removed from the ALT potential

Task 1: the D-03 gate script (measure-optimality-gate.mjs) reads the frozen
pre-ALT record, re-routes the same coordinate-pinned pairs on the current
ARG2 binary, and gates on seconds-equality (±0.1%) + verdict-class
preservation — never on node paths (equal-cost ties are documented behavior).

Rule-1 deviation the gate forced on its first run: routeAstar returned
SUBOPTIMAL real-graph routes (x038: 1234.6s vs the 1214.8s Dijkstra optimum;
x045: 1475.5s vs 1460.6s) — the fixture sweep could not see it. Root cause:
the fromTable bound d̂(ℓ,t) − d̂(ℓ,v) is one-directional Lipschitz (its u-side
term needs the REVERSE edge; a oneway does not provide one — the anchor
reached node 264611 126.8s faster than its own 1.49s upstream neighbour
264610), and the shared Ikeda average p = (h_f − h_b)/2 is consistent only
when every family inside h_f/h_b is two-sided. The toTable bound
d̂(v,ℓ) − d̂(t,ℓ) rides stored traversable edges in BOTH directions; it alone
joins the haversine now. Stop rule, reductions, meet probes, reconstruction:
untouched. landmarkTables/build verified EXACT (0 mismatches vs independent
integer Dijkstras, both rows, all 24 anchors).

- measure-optimality-gate.mjs: exported core + CLI guard (route-corpus
  pattern); epsilon mirror + argVersion asserts precede any measurement;
  per-pair rows, extract-drift WARNING (never a re-record), honest exit law
- astar.ts: potential() consults landmarkTo only; doc-comments carry the
  one-directional-Lipschitz law and the x038/x045 evidence
- astar.test.mjs: A11 re-pinned (landmarkFrom must NOT appear in the
  comment-stripped search — re-adding it trips the pin); A12 oneway-ring
  sweep added (directed reach asymmetry stays Dijkstra-equal on every pair)

Battery: routing 80/80, bot 126/126, both typechecks green.
D-03 gate: GATE PASS — 53/53 routed pairs equal within ±0.1% (max |Δ| 0.005%),
verdict classes preserved (6 unreachable + 41 unsnappable, 0 re-snapped).
This commit is contained in:
araharah-executor
2026-10-25 19:54:24 +08:00
parent ab0b465218
commit 149636ce0a
3 changed files with 441 additions and 46 deletions
+56 -45
View File
@@ -219,22 +219,31 @@ function reverseFor(graph: RoadGraph): ReverseAdj {
* exhaustive 625-pair Dijkstra-equivalence sweep is the standing proof,
* re-run on every pass.
*
* ALT (plan 08-03): the h_f/h_b bodies are max(ALT triangle bounds,
* haversine) over the ARG2 landmark tables (graph.landmarkTo /
* graph.landmarkFrom, quantized at graph.landmarkQuantumS). The tables
* come from landmark.ts's integer ĉ-metric Dijkstras — floor-quantized
* EDGE WEIGHTS make the stored distances an exact metric, so the triangle
* bounds derived from them are exactly admissible and exactly consistent
* against the real f32 seconds (no admissibility epsilon). Sentinel laws
* (research Pattern 3): a landmark whose goal/origin-side cell is the
* 0xFFFF sentinel (DATA) drops for the WHOLE search — the search-scoped
* constant skip; a per-node sentinel cell skips that ℓ; a node sentinel
* for every remaining ℓ falls back to the pure haversine bound (admissible
* + consistent everywhere). The survey's (πf−πr)/2 combination is what the
* ALT (plan 08-03, amended 08-05): the h_f/h_b bodies are max(ALT triangle
* bounds, haversine) over the ARG2 landmark tables (graph.landmarkTo,
* quantized at graph.landmarkQuantumS) — the toTable families ONLY. The
* tables come from landmark.ts's integer ĉ-metric Dijkstras —
* floor-quantized EDGE WEIGHTS make the stored distances an exact metric,
* so the triangle bounds derived from them are exactly admissible and
* exactly consistent against the real f32 seconds (no admissibility
* epsilon). 08-05 amendment (the D-03 gate's catch): the fromTable
* families d̂(ℓ,t) − d̂(ℓ,v) are one-directional Lipschitz — their
* u-side bound needs the REVERSE edge (d̂(ℓ,u) ≤ d̂(ℓ,v) + ĉ(v→u)),
* which a oneway does not provide — and the shared Ikeda average
* p = (h_f − h_b)/2 is only consistent when EVERY family inside h_f/h_b
* is two-sided. Mixing them returned suboptimal real-graph routes
* (x038: 1234.6s vs 1214.8s optimum). The toTable bound d̂(v,ℓ) − d̂(t,ℓ)
* rides stored traversable edges in BOTH directions (u→v→ℓ, v→u→ℓ) —
* it alone joins the haversine. Sentinel laws (research Pattern 3): a
* landmark whose goal/origin-side to-cell is the 0xFFFF sentinel (DATA)
* drops for the WHOLE search — the search-scoped constant skip; a
* per-node sentinel cell skips that ℓ; a node sentinel for every
* remaining ℓ falls back to the pure haversine bound (admissible +
* consistent everywhere). The survey's (πf−πr)/2 combination is what the
* p_f below already implements — ONLY the h_f/h_b bodies changed; the
* reductions, meet probes, stop rule, and reconstruction are the proven
* BH skeleton, and A1's sweep re-run under ALT (with A9/A10's island +
* skip seals) is the standing optimality proof.
* BH skeleton, and A1's sweep re-run under ALT (with A9/A10/A12's island,
* skip, and oneway seals) is the standing optimality proof.
*/
export function routeAstar(graph: RoadGraph, originNode: number, goalNode: number): AstarResult | null {
const n = graph.nodeCount;
@@ -249,31 +258,40 @@ export function routeAstar(graph: RoadGraph, originNode: number, goalNode: numbe
const origLat = graph.lat[originNode]!;
const origLng = graph.lng[originNode]!;
// ALT per-search constants (plan 08-03): the goal/origin-side table cells
// hoisted ONCE per search, kept in QUANTA units with a 0xFFFF sentinel
// written as NaN. A sentinel constant drops that landmark for the WHOLE
// search — the search-scoped skip; these constant tables are the ONLY
// ALT per-search constants (plan 08-03, amended 08-05): the goal/origin-side
// to-table cells hoisted ONCE per search, kept in QUANTA units with a 0xFFFF
// sentinel written as NaN. A sentinel constant drops that landmark for the
// WHOLE search — the search-scoped skip; these constant tables are the ONLY
// place skip decisions live (never a per-node ℓ-mask mid-max, which would
// vary the landmark set inside the max and break the max-of-Lipschitz
// consistency argument). L >= 1 is a decodeGraph guarantee (ARG2 refuses
// landmarkCount 0 — D-01), so there is no L===0 branch and no dead
// fallback path: one search path.
//
// 08-05 AMENDMENT — the fromTable families are GONE, and that is the fix:
// the D-03 optimality gate caught routeAstar returning suboptimal real-graph
// routes (pair x038: 1234.6s vs the 1214.8s Dijkstra optimum; x045: 1475.5s
// vs 1460.6s). Root cause: a fromTable bound d̂(ℓ,t) − d̂(ℓ,v) is Lipschitz
// across an edge ONLY in the direction the anchor's reach confirms —
// d̂(ℓ,u) ≤ d̂(ℓ,v) + ĉ(v→u) needs the REVERSE edge, which a oneway does
// not have (KL: the anchor reached a node 126.8 s faster than its own 1.49 s
// upstream neighbour). The toTable bound d̂(v,ℓ) − d̂(t,ℓ) is two-sided:
// u→v→ℓ AND v→u→ℓ both ride stored traversable edges. The Ikeda average
// p = (h_f − h_b)/2 is shared by BOTH search directions, so every family
// inside h_f/h_b must be two-sided-Lipschitz — only the toTable pair is.
// haversine is two-sided (its chord ≤ road cost in both directions). The
// fixture sweep never caught this: bidirectional synthetic edges have no
// one-way reach asymmetry.
const L = graph.landmarkCount;
const Q = graph.landmarkQuantumS;
const goalToU = new Float64Array(L);
const goalFromU = new Float64Array(L);
const origToU = new Float64Array(L);
const origFromU = new Float64Array(L);
for (let l = 0; l < L; l++) {
const base = l * n;
const gTo = graph.landmarkTo[base + goalNode]!;
goalToU[l] = gTo === 0xffff ? Number.NaN : gTo;
const gFrom = graph.landmarkFrom[base + goalNode]!;
goalFromU[l] = gFrom === 0xffff ? Number.NaN : gFrom;
const oTo = graph.landmarkTo[base + originNode]!;
origToU[l] = oTo === 0xffff ? Number.NaN : oTo;
const oFrom = graph.landmarkFrom[base + originNode]!;
origFromU[l] = oFrom === 0xffff ? Number.NaN : oFrom;
}
// Directional heuristics + opposite potentials, lazy per node — only
@@ -283,49 +301,42 @@ export function routeAstar(graph: RoadGraph, originNode: number, goalNode: numbe
const pf = new Float64Array(n); // p_f(v) = (h_f - h_b)/2; p_b = -p_f — valid once both caches are set
// One directional bound: the max-rule (research Pattern 1) — the sharper
// of the haversine bound and the best ALT triangle bound toward the target
// whose constants are constTo/constFrom. Four families per landmark ℓ
// (Bast et al. survey §2.2), evaluated in quanta and converted to seconds
// ONCE at the end:
// family A: d(v,t) >= d(v,ℓ) − d(t,ℓ) (toTable both terms)
// family B: d(v,t) >= d(ℓ,t) − d(ℓ,v) (fromTable both terms)
// (mirrored toward the origin by the hb call site). Per-node sentinel
// cells skip that ℓ — compared RAW (u16) BEFORE any float conversion
// (the sentinel read as a float would be a large-but-finite bogus bound
// dominating the max). A node sentinel for every remaining ℓ degrades to
// exactly the
// of the haversine bound and the best ALT triangle bound toward the target.
// TWO families per landmark ℓ — the toTable pair (amended 08-05, see the
// per-search comment above for why the fromTable pair is excluded):
// family A toward goal: d(v,t) >= d(v,ℓ) − d(t,ℓ) (this call)
// family A toward origin: d(v,o) >= d(v,ℓ) − d(o,ℓ) (the hb call site)
// evaluated in quanta and converted to seconds ONCE at the end. Per-node
// sentinel cells skip that ℓ — compared RAW (u16) BEFORE any float
// conversion (the sentinel read as a float would be a large-but-finite
// bogus bound dominating the max). A node sentinel for every remaining ℓ
// degrades to exactly the
// pure haversine bound. A family value may sit below zero (v closer to ℓ
// than t is) — legal: p_f already goes negative when h_b > h_f, the BH
// meet-sum law is algebraic in its sign, and the max with the
// non-negative haversine bound keeps h_f/h_b >= 0 anyway.
function bound(v: number, lat2: number, lng2: number, constTo: Float64Array, constFrom: Float64Array): number {
function bound(v: number, lat2: number, lng2: number, constTo: Float64Array): number {
let bestTo = Number.NEGATIVE_INFINITY;
let bestFrom = Number.NEGATIVE_INFINITY;
for (let l = 0; l < L; l++) {
const base = l * n;
const tv = graph.landmarkTo[base + v]!;
if (tv === 0xffff) continue; // per-node sentinel skip — RAW u16 compare
const cTo = constTo[l]!;
if (!Number.isNaN(cTo)) bestTo = Math.max(bestTo, tv - cTo); // family A: d(v,ℓ) − d(t,ℓ)
const fv = graph.landmarkFrom[base + v]!;
if (fv === 0xffff) continue;
const cFrom = constFrom[l]!;
if (!Number.isNaN(cFrom)) bestFrom = Math.max(bestFrom, cFrom - fv); // family B: d(ℓ,t) − d(ℓ,v)
}
const hav = metersTo(graph, v, lat2, lng2) * heuristicScale;
const alt = Math.max(bestTo, bestFrom);
return alt > Number.NEGATIVE_INFINITY ? Math.max(hav, alt * Q) : hav;
return bestTo > Number.NEGATIVE_INFINITY ? Math.max(hav, bestTo * Q) : hav;
}
function potential(v: number): number {
let hf = hfCache[v]!;
if (Number.isNaN(hf)) {
hf = bound(v, goalLat, goalLng, goalToU, goalFromU);
hf = bound(v, goalLat, goalLng, goalToU);
hfCache[v] = hf;
}
let hb = hbCache[v]!;
if (Number.isNaN(hb)) {
hb = bound(v, origLat, origLng, origToU, origFromU);
hb = bound(v, origLat, origLng, origToU);
hbCache[v] = hb;
}
const value = (hf - hb) / 2;