62 of 67 DISCHARGED proof claims have never been verified; 4 confirmed false

[hyperpolymath]

src/**/*.idr carries 67 DISCHARGED docstring claims across 23 files. A DISCHARGED marker
asserts that a proof obligation has been met. Nothing checks it.

	Count
Total DISCHARGED claims	67, in 23 files
Written during this campaign, each verified rc=0 at the time of writing	5
Pre-existing and never verified	62
Confirmed false so far	4

The four confirmed-false claims were found incidentally — they surfaced while the build was being
driven forward, not by any search for them. The 62 have not been audited, so 4 is a floor, not
an estimate.

Why this is the highest-severity item on the list

A false DISCHARGED is strictly worse than an OWED marker. OWED is honest debt and shows up in
the debt register. DISCHARGED is a claim of completion that silences the register — it removes
the obligation from view while leaving it undischarged. The same shape as this repo's
believe_me = 0 badge: literally true, and the debt was relocated rather than met.

The audit instrument already exists

The build is the audit. Every module that compiles rc=0 with --total has had its
DISCHARGED claims mechanically checked, because a false claim in a proof body cannot typecheck.
So this issue is largely discharged as a side effect of finishing the build — which is a strong
additional reason to finish it.

What is needed beyond that:

1. Enumerate all 67 with file:line.
2. Mark the 62 unverified ones DISCHARGED (UNVERIFIED) until their module compiles clean.
3. Add a gate: a DISCHARGED claim in a module that does not compile --total is a build failure.

Context: docs/IDRIS2-BUILD-WORK-PACKAGE.adoc §5.2.