docs(agents): bank elaboration, vacuity-certificate, and restacking gotchas

[alik-eth]

Five field-tested additions to docs/agents/gotchas.md, distilled from recent proof campaigns and written as timeless guidance:

• Type System port: make indexing sets a parameter rather than a field #8 — structure values closing over Fintype.ofFinite/SampleableType.ofFintype are whnf-hostile: the mechanism, the where-syntax symptom, and the fixes (anonymous constructors; abstract-value + pinning-equality statement architecture; explicit Classical.propDecidable).
• Proof Patterns feat: Better constructions for uniform selection and various @[simp] proofs #14 — hypothesis satisfiability is a proof obligation: vacuous conditional theorems are invisible to #print axioms; the two common failure classes (relation-pinning pairs vs gen_sound; deterministic small-seed-image cardinality), and the rule of shipping a kernel-checked inhabitance certificate in the same commit.
• Build/Tooling feat: more useful API for tracking, swap to concrete bound focus #21 — warm-starting worktrees from a built donor's .lake/build (placed as a cluster with the existing cache entry).
• Build/Tooling feat: major overhaul to add Alternative instance for OracleComp #22 — lake env lean/LSP don't check olean staleness: phantom whnf timeouts and unknown-identifier errors that mimic real elaboration pathologies (including a section-dependence illusion via shared instance fvars); rule: no-op lake build before diagnosing, trust only symptoms that reproduce after.
• Build/Tooling feat: Overhaul foundations to be more idomatic #29 — restacking with git rebase --onto <new-base> <old-base-tip> after folding commits into a base, and the tree byte-identity gate before pushing.

Docs-only; entries renumbered into a clean sequence (verified nothing references gotchas by number).

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

[github-actions]

🤖 PR Summary

Failed to generate AI summary. Please check the per-file summaries and statistics below.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	117
❌ Lines Removed	17

---

Lean Declarations

• No declarations were added, removed, or affected.

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📄 **Per-File Summaries**

• docs/agents/gotchas.md: The diff adds four new gotchas (now numbered 14, 21, 22, and 29) and renumbers all subsequent entries due to insertions in the middle of the document.

• New gotcha 14 ("Hypothesis satisfiability is a proof obligation") is inserted under "Proof Patterns." It warns that conditional theorems with uninhabitable hypotheses are vacuously true and undetectable by #print axioms, then describes two failure classes: relation-pinning pairs (where GenerableRelation.gen_sound forces support into the relation, making a pair (hr : GenerableRelation _ _ r) (hGen : hr.gen = myGen) uninhabitable if support myGen ⊄ r) and cardinality mismatches (e.g., a small seed space cannot be uniformly distributed on a larger space). The fix requires shipping an explicit-witness inhabitance certificate with every new hypothesis pair.
• New gotcha 21 ("Warm-start new worktrees from a built donor worktree") is added under "Build and Tooling." It describes copying the entire .lake/build tree from a matching-branch worktree to make a new worktree's build a near-no-op, warns about toolchain mismatches, and advises a sanity check.
• New gotcha 22 ("lake env lean and the LSP do not check olean staleness") is added under "Build and Tooling." It explains that both tools elaborate against whatever import .oleans are on disk, producing deterministic phantom failures (whnf/heartbeat timeouts, unknown-identifier errors, apparent section-dependence) that mimic genuine pathologies. The fix is to run lake build <lib> before diagnosing any elaboration pathology.
• New gotcha 29 ("Restack with --onto after folding commits into a base branch") is added under "Build and Tooling." When a stacked branch's early commits are folded into its base, it warns that a plain rebase from the branch's own fork point silently drops mid-stack commits, and prescribes git rebase --onto <new-base> <old-base-tip> <branch> --empty=drop followed by a tree byte-identity gate via git diff.

---

Last updated: 2026-07-13 15:41 UTC.