docs: honesty sweep — correct overclaimed dependency/feature/status docs (G09–G12) (#56)

## What

Docs-only honesty sweep — four doc-vs-reality overclaims in the
flagship, each corrected to the ground-truth (verified against the
actual `Project.toml` / filesystem so no fix smuggles in a *new* wrong
claim).

| Gap | File | Was (false) | Now (true) |
|---|---|---|---|
| **G11** | `EXPLAINME.adoc` | `AcceleratorGate` + `JSON3` listed as
hard deps; "13 weak dependencies" | AcceleratorGate is **vendored**
(`src/vendored/`); JSON3 was **removed**. Real: **10** hard deps / **6**
weakdeps / **5** extensions |
| **G12** | `README.md` | "Coprocessor Targets" implied accelerated
execution | Qualifier: detection+dispatch **skeleton**, falls back to
the Julia backend (test log confirms TPU→Julia fallback) |
| **G10** | `REGISTRY-READINESS.md` | "LLM-tell files … ✅ Removed" |
**False** — `0-AI-MANIFEST.a2ml` (a *required* RSR manifest) and
`llm-warmup-*.md` are still present; row corrected to reality |
| **G09** | `EXPLAINME.adoc` | SMT skip unexplained | Documented:
`packages/SMTLib.jl` is monorepo-only/unregistered → `AxiomSMTExt`
doesn't load outside the monorepo → `@prove` degrades to `:unknown` (a
**logged** fallback, not a silent skip) |

Plus design-diary **Entry 0008** (covers the merged G06 HuggingFace
wiring + this sweep).

## Verification

Every corrected number was ground-truthed:
- `[deps]` = 10, `[weakdeps]` =
`AMDGPU/CUDA/KernelAbstractions/Metal/PyCall/SMTLib` (6), `[extensions]`
= 5 — matches the new EXPLAINME text.
- `AcceleratorGate` absent from `Project.toml` +
`src/vendored/AcceleratorGateVendored.jl` present.
- `JSON3` absent from `Project.toml`.
- `0-AI-MANIFEST.a2ml`, `llm-warmup-dev.md`, `llm-warmup-user.md` all
present on disk.

No code changes. All edits are at repo root or
`docs/design-diary/*.adoc` (not `docs/*.md`), so the AsciiDoc-by-default
gate is unaffected; no V-lang tokens.

## Flagged for owner (not touched — rename/delete/policy calls)

- README is `README.md` where the estate rule wants `README.adoc`
(several tooling refs to `README.adoc` currently dangle).
- Whether `llm-warmup-*.md` belong in a *registered* package's root.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---
_Generated by [Claude
Code](https://claude.ai/code/session_01UPFC9YQ7g9gc3VnRox42Q1)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

EXPLAINME.adoc

@@ -122,8 +122,9 @@ requiring `PyCall`).
   `CpuFeatures` struct for backend capability assessment at startup.
 
 | `AcceleratorGate.jl`
-| Direct dependency; Axiom's 15-backend dispatch architecture extends
-  AcceleratorGate's type hierarchy with ML-specific operations.
+| Vendored (`src/vendored/AcceleratorGateVendored.jl`; upstream is unregistered)
+  — NOT a `Project.toml` dependency. Axiom's 15-backend dispatch architecture
+  extends AcceleratorGate's type hierarchy with ML-specific operations.
 
 | `QuantumCircuit.jl`
 | Shares the backend dispatch pattern (JuliaBackend → hardware fallthrough).
@@ -225,12 +226,23 @@ requiring `PyCall`).
   interop, serving endpoints, model packaging, proof export, backend detection.
 
 | `packages/SMTLib.jl`
-| Internal Julia-native SMT library consumed by the `@prove` default backend.
+| Internal Julia-native SMT library consumed by the `@prove` SMT backend. It is
+  a monorepo-only, *unregistered* package (resolvable only via the workspace/dev
+  path inside this repo), and it is wired as the `AxiomSMTExt` weak-dependency
+  extension. Consequence: outside the monorepo the extension does not load, so
+  the SMT path is unavailable — `@prove` then degrades gracefully (returns
+  `:unknown` rather than proving) and the SMT-runner tests log
+  `Skipping SMT runner test; no solver available` instead of failing. This is a
+  deliberate, logged fallback, NOT a silent skip. Registering SMTLib in General
+  would remove the monorepo restriction (tracked; out of scope here).
 
 | `Project.toml`
-| Package identity (uuid `bbd403f8...`), v1.0.0, `AcceleratorGate`/`HTTP`/`SHA`/
-  `JSON`/`JSON3`/`Zygote`/`Libdl` hard dependencies, 13 weak dependencies for
-  GPU and coprocessor extensions.
+| Package identity (uuid `bbd403f8...`), v1.0.0. Hard dependencies (10):
+  `Dates`/`HTTP`/`JSON`/`Libdl`/`LinearAlgebra`/`Random`/`SHA`/`Serialization`/
+  `Statistics`/`Zygote` — AcceleratorGate is vendored (not a dependency) and
+  JSON3 was removed. 6 weak dependencies
+  (`AMDGPU`/`CUDA`/`Metal`/`KernelAbstractions`/`PyCall`/`SMTLib`) driving 5
+  extensions for GPU / PyTorch / SMT.
 
 | `docs/wiki/`
 | Markdown wiki: Home, User-Guide, Developer-Guide, Vision, Axiom-DSL,

README.md

@@ -112,6 +112,13 @@ prod_model = compile(model, backend=ZigBackend("/path/to/libaxiom_zig.so"), opti
 
 ## Coprocessor Targets
 
+> **Status — skeleton, not accelerated execution.** Coprocessor support today is
+> a *detection + dispatch* surface: `detect_coprocessor()` probes for devices and
+> `compile(…, backend=cop)` routes through the backend interface, but the
+> per-device compute kernels are not yet implemented, so execution gracefully
+> falls back to the Julia backend. Treat this as a forward-looking API, not
+> hardware-accelerated inference.
+
 ```julia
 # Non-GPU accelerator targets with self-healing fallback
 cop = detect_coprocessor()  # TPU/NPU/VPU/QPU/PPU/MATH/CRYPTO/FPGA/DSP or nothing

REGISTRY-READINESS.md

@@ -19,7 +19,7 @@ package submissions. The only thing that rebuilds that trust is honesty.
 | `generate_certificate` threw `FieldError` (`result.mode` nonexistent) — broke the shipped example | ✅ Fixed (`verification_mode` kwarg) |
 | `sum(::Tensor; dims)` undefined — documented usage failed | ✅ Fixed |
 | Licensing self-contradictory: `Project.toml` MPL-2.0 vs source headers PMPL-1.0 (non-OSI) | ✅ Relicensed consistently to **MPL-2.0** (OSI), REUSE.toml added |
-| LLM-tell files in package root (`0-AI-MANIFEST.a2ml`, `llm-warmup-*.md`) | ✅ Removed |
+| LLM-tell files in package root | ⚠ Corrected (were NOT removed): `0-AI-MANIFEST.a2ml` is a **required** RSR machine-readable manifest — kept, not an LLM-tell to remove. `llm-warmup-*.md` remain in root as the estate LLM-warmup convention (same as sibling repos, e.g. `julia-professional-registry`). |
 
 ## Honest current limitations (NOT hidden)
 

docs/design-diary/PEPYS-DESIGN-DIARY.adoc

@@ -325,3 +325,50 @@ caps the whole score).
 *Method held:* ran tools not docs (and ran them on my OWN deliverable);
 fixed the A2ML collision at source; no self-grade; faithful reporting of the
 BLOCKED push and the 3 template bugs I had to fix.
+
+== Entry 0008 — 2026-07-01 — Shipped a planned feature honestly, then swept the overclaims
+
+*Main-route directive:* "concentrate on concerns on our main route" — i.e. the
+flagship's holes, holes-first. Two slices, both ground-truthed by running tools.
+
+*G06 — HuggingFace, wired not deleted (#55, merged).* `huggingface.jl` was 825
+lines of dead code: not `include`d from `src/Axiom.jl`, `using JSON3` (a dep
+that had been removed from Project.toml), and a `✓ Current Status` header
+claiming features that could not run. Rather than delete cold code (doctrine #7)
+I WIRED it: ported JSON3→JSON (already a dep, no new dependency), fixed the two
+bugs wiring exposed (unexported internals `Pipeline`/`AbstractLayer`/`parameters`
+needed explicit import; `verify_model` was an *undefined export* Aqua flags),
+and added `test/integrations/huggingface_tests.jl` exercising the network-free
+core (architecture detection, model building into an Axiom Pipeline, SafeTensors
+dtype). The `✓` header became honest capability tiers (wired+tested / needs-
+network / not-implemented) and the wiki's contradictory "⚠ Beta / not shipped"
+was reconciled. Verified: Pkg.test 732/732 green (Aqua+JET+new HF tests). The
+network hub-fetch is present and honestly gated as network-required, not CI-run.
+Measurement drove the wire-vs-park call: I didn't guess JET would tolerate 825
+new lines — I ran it.
+
+*G09–G12 — the overclaim sweep (this entry's commit).* Four doc-vs-reality
+holes, each corrected to the ground-truth:
+- G11: EXPLAINME listed `AcceleratorGate` and `JSON3` as hard dependencies —
+  AcceleratorGate is VENDORED (`src/vendored/`), JSON3 was removed. Corrected to
+  the real 10 hard deps / 6 weakdeps / 5 extensions (counts verified against
+  Project.toml, so the fix doesn't introduce a new wrong number).
+- G12: README's "Coprocessor Targets" presented `compile(…, backend=cop)` as
+  working; the test log shows TPU falling back to the Julia backend. Added a
+  "skeleton, not accelerated execution" qualifier.
+- G10: REGISTRY-READINESS claimed LLM-tell files "✅ Removed" — false;
+  `0-AI-MANIFEST.a2ml` (a REQUIRED RSR manifest, must stay) and `llm-warmup-*.md`
+  are both still present. Corrected the row to the truth.
+- G09: documented that `packages/SMTLib.jl` is monorepo-only/unregistered, so
+  the `AxiomSMTExt` weakdep extension doesn't load outside the monorepo and
+  `@prove` degrades gracefully to `:unknown` — a deliberate, LOGGED fallback,
+  not a silent skip.
+
+*Flagged for owner (not touched):* README is `README.md` where the estate rule
+wants `README.adoc` (several tooling refs point at `README.adoc` and dangle);
+and whether `llm-warmup-*.md` belong in a registered package's root. Both are
+rename/delete/policy calls — surfaced, not decided unilaterally.
+
+*Method held:* wired-not-deleted; ran the tools (Pkg.test, grep-vs-Project.toml)
+not the status docs; verified my OWN corrected numbers so an honesty fix didn't
+smuggle in a fresh overclaim; no self-grade.