docs: bring the repo's account of itself in line with what is true

[hyperpolymath]

Documentation pass for humans and machines. Everything below was measured or
path-checked; nothing is asserted. No code touched — the diff is 5 files, all docs and
manifests.

The machine-readable side was the worse half

.machine_readable/6a2/STATE.a2ml was stale and partly corrupt:

• named the project "gql-dt", dated 2026-02-01, claimed 45% completion
• listed already-completed milestones as critical next actions — "Create
  bridge/lith_types.zig", "Begin Milestone 6 (GQL Parser)"
• its purpose field held a fragment of a build error rather than a purpose:
  "References to removed .tracked and .confidence constructors, missing API updates"

Rewritten with measured figures, plus four sections it didn't have: [verification]
(each gate and its result), [caveat] (a green proof gate ≠ nothing assumed),
[history-landmines] (the squash-extract, the sweep branches, the floating @main pins),
and [evidence] (the command reproducing every claim).

0-AI-MANIFEST.a2ml identified the repo as "GQL-DT — Dependently-Typed Glyph Query
Language". It is GNPL; GQLdt is the layer beneath. The purpose now states the two-layer
structure explicitly, so an agent doesn't conclude the GqlDt namespace is a mistake.

Its canonical-locations block was worse — all six paths were dead:

Claimed	Reality
.machine_readable/{STATE,META,ECOSYSTEM,ROADMAP}.scm	converted to .a2ml under 6a2/, never repointed
AI.a2ml	never existed
justfile	never existed

Replaced with 20 paths, each verified to exist (20/20 checked), plus an (evidence)
block and a (caveat-for-agents) warning against reporting this repo as "verified" on the
strength of a green build.

Human-readable

docs/STATE-OF-PLAY.adoc (new) — the human twin of STATE.a2ml, kept deliberately
parallel so drift between them is visible. What is established and by which command;
the gates and why they're trusted; what is known missing; the two open decisions; the
sequencing.

It also lists the four gates this repo has shipped and removed that could not fail — the
tautological naming check, the || echo on lake test, suites whose main : IO Unit
always exited 0 while printing "All tests passed!", and the Containerfile masking both
its steps. That history is why the standard is "a gate is not trusted until it has gone
red on a seeded fault".

docs/proof-debt.md §(b) claimed this repo has "no executable test coverage" and
that a @[test_driver] was "a prerequisite for moving any item into this section". That
prerequisite is now met (163 checks) — so the claim was stale in my own favour, which is
the direction that matters least and gets caught least.

Corrected while keeping the section empty: coverage existing is not the same as a given
axiom being covered, and the policy wants a citable refutation budget. D4's entry updated
likewise — its blocker is no longer "no coverage at all" but "this path is not
property-tested", which is materially different and now reachable.

Verification

• 20/20 manifest paths confirmed present
• diff touches no .lean, .zig or lakefile — git diff --name-only shown above
• main at 9de0713 independently verified green from a clean checkout earlier today:
  lake build exit 0, lake test exit 0, 163 checks

🤖 Generated with Claude Code

[gitar-bot]

Note

Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime.
Learn more

Code Review ✅ Approved

Updates documentation and machine-readable manifests to correct stale status claims, fix dead file paths, and align the repository description with actual state. No issues found.

Auto-approved and auto-merge armed: No blocking issues found.
Please see Auto-approve Docs for details on setting custom approval criteria. — merges when pipeline and required approvals pass.

Options

Display: compact → Showing less information.

Comment with these commands to change the behavior for this request:

Compact

gitar display:verbose

_{Was this helpful? React with 👍 / 👎 | Gitar}

[gitar-bot]

⚠️ Gitar auto-approved this PR but could not enable auto-merge: auto-merge is disabled for this repository — enable "Allow auto-merge" in the repository settings.

[gitar-bot]

Gitar has auto-approved this PR and enabled auto-merge (configure)