proven: postulate cure is NOT on origin/main — 42 .idr files/360 sites still unparseable there; the full cure exists only as ~77 UNCOMMITTED working-tree files on a local branch

[hyperpolymath]

Claim

hyperpolymath/proven remote main (@ aa6dbd23, 2026-08-31) still carries 42 unparseable .idr files / 360 postulate sites. The cure exists — but on the local branch fix/idris2-totality-and-elaboration-cures, whose committed HEAD (2ce64f03) still has 39 postulate files; the full cure exists only as ~77 uncommitted working-tree files in hyper-repos/proven. Unpushed, unmerged, uncommitted.

Why this is urgent

Uncommitted working-tree changes are the most fragile state in the estate — one git checkout/clean/sweep away from gone (this exact class of loss has happened before: purge sweeps have destroyed uncommitted work). The repair effort that fixed 11 defect classes in proven is currently not durably recorded anywhere.

First step

In hyper-repos/proven: commit the working tree to fix/idris2-totality-and-elaboration-cures, push the branch, open the PR. (Verify the 77 files first — this measurement is from the #675 verification pass, 2026-08-31; commands: git grep -lE '^\s*postulate' 2ce64f03 -- 'src/**/*.idr' | wc -l → 39; working tree → 0.)

Found while re-verifying #675; filed per the discoveries-become-issues rule. Related: #675 (the estate-confinement register), #677 (repos whose damage hides uncommitted state).

[hyperpolymath]

Preservation executed 2026-08-31. The cure is now durable: 81 .idr files (the 77 modified + 4 new modules: SafeRegex/Matcher, SafeSQL/Builder, SafeXML/Parser, SafeYAML/Parser) committed as d2d57a0d and pushed — origin/fix/idris2-totality-and-elaboration-cures now exists remotely.

What was deliberately NOT committed (the working tree held 246 changes, not 77): 72 .ts binding files that are pure deletions to zero — the deno/tsc blanking-sweep signature, previously known in project-ovine's tree, now confirmed in proven's. HEAD holds the real content, so the blanking lives only in the working tree; do not commit those paths. The remaining ~90 changes (.afs one-liners, workflow/docs edits, a FUNDING.yml rename) are of unaudited provenance and were left uncommitted for a deliberate pass.

Remaining for this issue: audit the leftover working-tree changes, discard the blanked .ts files, then PR the cure branch onto main (which still carries 42 unparseable files / 360 sites).

[hyperpolymath]

One attribution correction to the note above: proven's 72 .ts deletions are whole-file deletions of the deno/assemblyscript binding trees — consistent with an in-flight deliberate banned-language purge (TypeScript/Deno are banned estate-wide) as much as with the token-blanking corruption class. The tree also carries the FUNDING.yml → funding.yml case-rename rider seen in project-ovine's sweep, so the two trees likely share one origin event. Either way the operational rule is unchanged: those paths stay uncommitted until ruled on — if it was a purge, it should land as its own audited commit; if it was damage, HEAD already holds the content.