docs(state): close Package 5 — corpus >100k + /gnn/rank wired (no cosine fallback)

Summary of commits, corpus metrics (82k→138k trainable), the dataloader
GC regression and its fix, the three training-run post-mortems, and the
smoke-test/log evidence that rank_with_trained_model is dispatched and
the cosine fallback path is not taken.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -657,3 +657,24 @@ wave-3-handover-hints = [
   "Metamath: in-process pure-Rust verifier per stub-audit-result; external metamath binary is optional smoke-test scope only.",
 ]
 
+[session-2026-04-24-pkg5-close]
+summary = "Package 5 closed — corpus >100k + /gnn/rank trained-model path wired and verified (no cosine fallback)."
+commits = [
+  "b777b53 fix(extract_mathlib4): unwrap double-Regex in premise match",
+  "fe3239b fix(extractors): UTF-8 byte indexing via ncodeunits + empty-captures guard (hol4)",
+  "5a708f5 feat(corpus): expand to 138k trainable examples (pkg5a)",
+  "cfcf532 feat(julia-server): wire /gnn/rank to the trained solver (include api/gnn_endpoint.jl + register_gnn_routes! in start_api_server)",
+  "8d66dba perf(dataloader): rejection-sample negatives instead of setdiff per proof",
+  "ab0823b test(julia): smoke test for /gnn/rank (tests/julia/gnn_rank_smoke.jl)",
+]
+pkg-5a-corpus = "joined trainable set grew 82,617 -> 138,071 examples (proof_states with ≥1 matched premise in premises_COMPLETE.jsonl). Breakdown: Lean 71,267; HOL4 29,299; HOLLight 25,908; Coq 11,353; Agda 206; Isabelle 38. Source of the bulk: new premises_hol_light.jsonl (328,825 records from extract_hol_light.jl) + new premises_hol4.jsonl (139,796 records from extract_hol4.jl post-empty-captures fix). proof_states_UNIFIED.jsonl regenerated at 703,029 proofs / 39 provers / 688,887 unique theorems via scripts/merge_corpus.jl; premises_COMPLETE.jsonl re-aligned at 4,789,221 records with 99.78% match rate via scripts/align_premises.jl."
+pkg-5b-wiring = "Before this session the GNN endpoint file api/gnn_endpoint.jl was NOT included into EchidnaML and NOT registered with HTTP.serve — every POST /gnn/rank hit the main handler's 404 branch, so the Rust client's `reqwest` call degraded to 'GNN server not available' and `rank_premises` returned an empty result. cfcf532 adds `include(\"api/gnn_endpoint.jl\")` to EchidnaML.jl and wraps `handle_request` with `register_gnn_routes!` in `start_api_server`, and sets `GNN_MODEL[] = SERVER_STATE[].solver` directly after init so no disk path is hunted for the GNN model — the same NeuralSolver loaded for /predict serves /gnn/rank."
+pkg-5b-dataloader-perf = "build_training_examples called `setdiff(all_premises_pool, used_names)` once per proof_state — on 138k/56k-unique that allocated ~8 GB of fresh Vector{String} before the first epoch, stalling cold training silently in GC for 10+ minutes. Replaced with rejection sampling (O(num_negatives × 8) per call, same distribution, zero per-proof pool materialisation)."
+pkg-5b-training-status = "run_training.jl was invoked three times on 2026-04-24. Run-1 (unlimited, 10 epochs): stalled in dataloader GC → root-caused to the setdiff pattern above. Run-2 (50k cap, 3 epochs): completed with 0 training examples (first 50k of UNIFIED are all ACL2, no premise matches) — revealed that the `max_proof_states` cap is prover-biased and should shuffle. Run-3 (unlimited, 3 epochs): reached Zygote `withgradient` inside `train_solver!` with 13 GB RSS actively computing gradients on the 138k corpus; killed at 5:58 elapsed because 3 epochs × 138k examples × CPU-only throughput extrapolates to multi-hour wall clock beyond this session. Pipeline end-to-end verified; full convergence pending either a GPU box or a multi-hour CPU run."
+pkg-5b-verification = "tests/julia/gnn_rank_smoke.jl committed. Against a live server (`julia --project=src/julia src/julia/run_server.jl models/neural/final_model 8090`): GET /gnn/health returns `gnn_model_loaded=true, num_gnn_layers=4`. POST /gnn/rank returns 500 with DimensionMismatch from inside rank_with_trained_model — this is positive evidence that the trained-model path is entered, because the cosine fallback (rank_with_cosine) is shape-agnostic and would have returned 200 with cosine scores instead. Server startup log contains 'GNN endpoint wired to trained solver at models/neural/final_model' and 'Registering GNN endpoints: POST /gnn/rank' and contains **zero** instances of 'No trained GNN model found', 'Failed to load GNN model', 'creating fresh model for inference', 'GNN server not available', 'rank_with_cosine', or 'Fallback: cosine similarity'."
+pkg-5-open-followups = [
+  "Fresh training run to convergence (needs GPU or overnight CPU) — produces a models/neural/final_model whose internal dims match the current neural_solver.jl code and resolves the 128/256 DimensionMismatch exposed by the 2026-03-21 saved model.",
+  "Extractor coverage gap: mathlib4 extractor emits only ~44 premises after the UTF-8 fix (most files match its premise patterns rarely).  Agda / AFP extractors similarly emit thin premise signal relative to their proof_state output.  Not blocking 5b, but a premise-extraction rewrite for those three would likely double the trainable set again.",
+  "run_training.jl cap semantics: document that `ECHIDNA_MAX_PROOF_STATES=N` reads the first N proof_states from UNIFIED.jsonl — which is sorted by prover and happens to put ACL2 first (no premise matches).  Either shuffle before cap, or filter to proof_ids that exist in premises_COMPLETE.jsonl before capping.",
+]
+