chore(checkpoint): 2026-06-05 repo reconciliation + docs/machine_readable refresh — resume tracker

[hyperpolymath]

Durable resume-point for the 2026-06-05 estate checkpoint (echidna + echidnabot), created so a compacted/next session continues without losing the audit. Spans the dogfood proof-CI work that just went green.

Decisions (owner-confirmed)

• PR fix(proofs+ci): repair proof corpus, unbreak Agda CI, and gate every proof in CI #234 (proof corpus + dogfood proof-CI, all green): squash-merge.
• Stale branches: delete only test-gpg-sign + test/ci-echidna-hypatia-fix (leave claude/dev-self-provision).
• rsr-template ↔ standards divergence: attempt via WebFetch (repos outside this session's scope; no add_repo/list_repos).

Remaining actions

echidna

• Squash-merge PR fix(proofs+ci): repair proof corpus, unbreak Agda CI, and gate every proof in CI #234 (flip draft→ready first). Squash msg drafted below.
• Delete test-gpg-sign + test/ci-echidna-hypatia-fix. NOTE: git push origin --delete failed ("remote end hung up; Everything up-to-date") — retry via colon refspec git push origin :refs/heads/<b> or a delete-ref MCP path.
• On a new claude/checkpoint-2026-06-05 branch off post-merge main (draft PR), refresh:
  • .machine_readable/6a2/STATE.a2ml — bump last-updated → 2026-06-05; add dogfood-proofs-ci session entry.
  • docs/ROADMAP.md + .machine_readable/ROADMAP.a2ml — record proof-corpus CI as a Stage-1 gate.
  • .machine_readable/6a2/{META,AGENTIC,NEUROSYM,PLAYBOOK,ECOSYSTEM}.a2ml — reference the proof-CI gate.
  • docs/wiki/* — add proof-CI + just proofs* local-run docs (must be bleeding-edge).
• File issue: --features verisim 22 compile errors (only genuinely-untracked TODO item; docs/handover/TODO.md P2).
• (minor) document why two ANCHOR.a2ml exist (anchors/ repo-identity vs 6a2/ SSG-build); note contractile-trident asymmetry (adjust/+bust/ carry full Nickel tridents; dust/intend/must/trust carry only the .a2ml).

echidnabot (branch already == main → new claude/checkpoint-2026-06-05 + draft PR)

• README.adoc — fix stale "129 tests / ~90%" → 184 and "12-prover enumeration" → ProverSlug dynamic (EXPLAINME.adoc already holds the truth).
• Archive SESSION_SUMMARY_2026-01-29.md (stale, pre-hardening).
• (minor) move contractiles/dust + contractiles/trust under .machine_readable/contractiles/ for alignment; root Mustfile is a stub.
• .machine_readable/6a2/STATE.a2ml — bump last-updated → 2026-06-05.

rsr-template

• WebFetch hyperpolymath/rsr-template + standards repo; report any divergence vs the RSR rules echidna/echidnabot embed.

Already-good — do NOT touch

• echidna Dustfile.a2ml + Bustfile.a2ml fully written; k9 svc/ templates real; README/EXPLAINME/wiki have no stale proof claims.
• Both repos: A2ML migration complete (no stale .scm), SHA-pins current — no alarming standards drift found within scope.
• Out-of-checkpoint-scope branches (leave alone): dependabot/* (4), pr-183, chore/training-infrastructure-cleanups.

Squash message for #234

title: fix(proofs): repair proof corpus + gate it in CI (Coq, Lean, Agda, Idris2)
body: Repairs proofs/{coq,lean,agda} + src/idris so all type-check; adds .github/workflows/dogfood-proofs-ci.yml (Coq/Lean/Agda); extends idris2-abi-ci.yml to type-check the src/idris validator; adds just proofs* recipes. Fixes two latent bugs: proofs/lean/lakefile.lean now roots every module (lake build was silently broken) and src/idris/Validator.idr gained a main. CI uses plain run: installs (works around a taiki-e/install-action startup_failure) + GitHub-pinned agda-stdlib v1.7.3 (apt --fix-missing was silently dropping it).