Purge regenerable ignored cache/worktree residue under recovery rules

[metaphorics]

Question

Which regenerable ignored caches can be purged from the working checkout such that authority sources, manifests, recovery commands, and ignore rules still fully identify regeneration?

Evidence base: .outline/research/docs-rules-build-audit.md DRB-6 row, executive finding 6, the deletion-blockers table, and the rule-table row "Generated formal/fixture caches are not authority".

Exact scope (working checkout only; all ignored and untracked today - verified: .gitignore:4 **/compiled/, :5 **/.lake/, :8 perf/fixtures/boundary/; git ls-files over these families returns only Redex .rkt authorities)

1. formal/lean/.lake/ (~7.1 MB today) - Lean/Lake build cache. Recovery: cd formal/lean && lake build under pinned lean-toolchain 4.32.1, lakefile.toml, lake-manifest.json.
2. formal/redex/compiled/, formal/redex/bytecode/compiled/, formal/redex/ecmascript/compiled/ (~925 KB today; exactly these three dirs) - Racket bytecode caches. Recovery: rebuild from the sibling .rkt sources with Racket 9.2 per formal/toolchains.toml.
3. perf/fixtures/boundary/ (~1.7 MB, 11 files today) - materialized boundary benchmark inputs. Recovery: perf_budget materialize-fixtures --manifest perf/benchmarks.toml, then perf_budget verify-fixtures --manifest perf/benchmarks.toml (command names verified at crates/bamts-verification/src/bin/perf_budget.rs:88-96,158-167).

Execution contract (order matters)

1. Pre-purge gates: (a) workspace-owner consent recorded - these paths are untracked machine-local state; (b) no running formal/verification/perf process holds these paths; coordinate with the formal cluster integrator and perf evidence owners; (c) git status --porcelain over the three families shows no tracked entries - the purge must produce zero tracked diffs.
2. Prove recovery per family, before or immediately after deletion: run the family's recovery command, observe the path regenerate (boundary fixtures must pass the verify-fixtures hash check), then purge again. A family's proof may be skipped only if its pinned toolchain or the materializer is unavailable in this environment; record which proofs ran.
3. Deletion covers exactly the five named paths. Nothing else.

Protected surfaces (do not touch)

• Tracked authorities: formal/redex/**/*.rkt, formal/lean/** sources plus lean-toolchain/lakefile.toml/lake-manifest.json, formal/toolchains.toml, perf/benchmarks.toml, perf/fixtures/upstream/* (tracked generated/authority-owned evidence inputs), perf/baselines/, perf/scorecard/, .gitignore.
• Untracked user-owned scratch with an explicit deletion gate elsewhere: root src/main.rs, grounding/, /out/, verification/ts-suite* - owned by the root-ownership ticket (DRB-7); this issue leaves them alone.

Blockers

• Concurrent formal/perf regeneration (audit unresolved question 6): purge in an idle window for those paths, never mid-build.
• If any recovery command fails after purge, rerun it to restore (that is the recovery rule); if a family cannot regenerate, stop and report before touching the next family.

Zero-residue checks

• test ! -e formal/lean/.lake && test ! -e formal/redex/compiled && test ! -e formal/redex/bytecode/compiled && test ! -e formal/redex/ecmascript/compiled && test ! -e perf/fixtures/boundary - all pass.
• git status --porcelain empty for the three families; .gitignore unmodified.
• git ls-files formal/lean/.lake perf/fixtures/boundary still empty; git ls-files formal/redex unchanged (.rkt authorities intact).
• Each family's recovery proof (or documented toolchain unavailability) recorded in the issue with command output.

No destructive action beyond the five named regenerable ignored paths

Nothing tracked, nothing user-owned, no untracked scratch, no generated authority is deleted; all five paths regenerate from named pinned commands.

[metaphorics]

Dependencies

This issue is blocked by:

• Workspace-owner consent for deleting untracked machine-local paths
• Idle window for formal/perf processes holding these paths — formal cluster and perf evidence work is concurrently in flight and regenerates these caches

Parent: #156. Feeds: #185 (keeps generated cache noise out of the surfaces the sync pass reads).

[metaphorics]

Evidence update (2026-08-31)

Source: agent://ResidueRecoveryScout — crash-residue file investigation.

Corrected crash-residue inventory

The actual crash-residue files are:

• 0.jsonl.tmp-3642429
• 1.jsonl.tmp-3642539
• 2.jsonl.tmp-3642662
• 3.jsonl.tmp-3642804

The six named .ts paths listed in the original issue body are absent from the working tree — they were in-memory fixture names, not on-disk files. No active writer exists for any of these paths.

Removal procedure

• Removal still awaits explicit workspace-owner consent (unchanged blocker).
• Removal must use rip -f (not rm) for the crash-residue files.
• No tracked files are affected; git status --porcelain will show zero tracked diffs after removal.

The original issue body's scope (five named regenerable ignored paths) stands unchanged; this update corrects only the crash-residue file inventory and removal tool.