docs: proof review against PROOF-POLICY; proof ledger; plan correction (#787)

This follows the merged completion plan, #786.
I re-ran every prover that could be installed, and judged each proof
against `metadatastician/standards` `3-practice/PROOF-POLICY.adoc` at
commit `9bdf864`.

## What changed
- **Proof ledger**, in `docs/EXPLAINME.adoc`. The README-EXPLAINME
standard requires one whenever a repo claims proofs, and this repo had
none. It is keyed to the obligation IDs in `docs/PROOF-NEEDS.adoc` and
has 22 rows: 7 `proven`, all of them about models rather than the
shipped code; 13 `open`; and 2 `argued`. No theory theorem has a proof
witness grade, because none has an Agda source.
- **Solo core status.** `docs/SOUNDNESS.adoc` and
`docs/PROOF-NEEDS.adoc` still said the Solo core's progress and
preservation were `?todo`. Both now check under Idris2 0.7.0 and are
total. That was a local check; no CI job runs it yet.
- **PROOF-NEEDS caveats.** P-3, P-4 and the K-1 real-lift text now say
they hold for models only. F-5 records the real `render_ty`
counterexample and stays open.
- **Plan proof route.** The completion plan's proof route was Coq-first.
It is now aligned with the policy: theory goes in Agda with Rocq and
Lean rechecks, and engineering goes in Idris2 or under a recorded §4
exception. There is a new section 5.0 and corrected rungs.
- **Plan findings and rulings.** Workflow W7 is corrected. The plan also
gains the verified per-repo results, new cross-repo items, and owner
questions 16 to 19 with the owner's rulings of 2026-11-09.
- **Idris2 0.8.0 results and provisioning fix** (`19084c8`).
- typed-wasm passes `tools/check-kernel-proofs.sh` in full under its
pinned Idris2 0.8.0 (`15a3e4e`). The plan's `Region.idr` item is closed.
  - januskey and absolute-zero type-check under the 0.8.0 release.
- New estate item: the Idris2 repos check against three different
compilers. typed-wasm uses the v0.8.0 tag, januskey and absolute-zero
use a pack image built from Idris2 `main`, and anytype uses 0.7.0.
- The W0 recipe now passes `PREFIX` to `make bootstrap` as well as to
`make install`. Without that, Idris2 type-checks but cannot run
programs, and still exits 0.

## New holes
- **H20.** `Face.render_ty` is not injective. On the Js face,
`List[Option[Int]]` and `Option[List[Int]]` both render as `List[Int] |
null`; on Cafe both render as `List[Int]?`. I observed this by calling
the built library. The Coq F-5 theorem proves the opposite, but for a
model that differs from the code.
- **H21.** The Coq proof gate covers only 96 of the 137 assertions. A
planted `Admitted` false lemma and a planted `Axiom False` both passed a
replica of the gate.
- **H22.** The 23 staged Agda files under `proposals/` pass the
canonical flags, but nothing runs them. `tools/check-proofs.sh --agda`
reports SKIP when its environment variables are unset.

## Proof review results
- **Coq.** All 20 files build under Coq 8.18, and all 137 assertions are
closed under the global context. Several headline theorems hold by
definition: P3 borrow soundness, F3, F4, F1 `same_cube`, and
`QttTyping.usage_soundness`. The `Real*` models differ from
`lib/codegen.ml`.
- **Idris2 Solo core.** It checks, and `progress` and `preservation` are
total.
- **Lean, installed with the owner's approval from
`releases.lean-lang.org`.**
- tropical-types builds all 20 modules at its 4.13.0 pin. Its 334
theorems use no `sorry`, no Mathlib and no `Classical.choice`.
  - occupancy's `stackcert` does not compile at its 4.15.0 pin.
  - This repo's copy of the tropical file compiles at 4.13.0.
- **Not re-run.** CI's Coq 8.20.1 was not re-run.

## Checks
- `bash tools/check-doc-truthing.sh`: OK
- `bash tools/check-soundness-ledger.sh`: all 5 properties hold. It ran
on deepened history.
- `asciidoctor --failure-level=WARN` on all four files: clean

Companion change in mathesis: hyperpolymath/mathesis#24.

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

https://claude.ai/code/session_01J4QvDjbCwy9iYWY9vKgzGW

---------

Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath