Settle how cead is built: spec, skeleton, fill

[1zeroone0]

What this PR does

Settles how cead is built before the first code, from scoping the first PR (the old loop PR, whose intent is now a Horizon comment on #7).

• One method. CODE.md is reorganized as method, vocabulary, languages. TLA+ specifies the system, Lean a core function, Rust is the system: one pipeline of spec → slice → core → skeleton → fill. The system spec (spec/cead.tla) comes first and is revisable: when code disagrees, the spec changes in that PR. A moved signature is learning, stated in the commit comment; a new capability is drift.
• Spec, not model. The artifact before the skeleton is a spec; "model" collided with the LLM.
• Frontier and claim. Placeholders (todo!, unimplemented!, unwrap, expect, #[ignore]) are the frontier, zero at merge. unreachable!() and #[expect(lint, reason)] are claims review reads. #[allow] is denied. Frontier lints warn, so a draft compiles and cargo clippy --all-targets -- -D warnings fails until filled. Tests unwrap through clippy.toml, not attributes. The toolchain pins clippy.
• Types as schema. The five language-enforced invariants and the "does it still compile?" test for what is a choice, written down as priors.
• Probe, then wrap. Dependencies are probed while scoping, findings in a PR comment, probe never committed. A dependency's types stay inside its boundary module.
• Vocabulary as a table. Every noun has one home in code (type, module or crate, binary); a noun may precede its home; no home without a noun.
• AGENTS.md. End-to-end tests first, ending in a checkable, re-runnable artifact. Branches name the change, not the thing changed. Only Horizon and PRs in progress are open. The squash trade is stated; gh land now keeps each PR's comment thread as a git note in refs/notes/pr (backfilled for Refresh cead's assets: Irish accents, feathered Ogham mark, SVG lockups #3, Name cead's userspace and its three ways to fan out #4, Make PR comments state their next step and feed the description #6). The one-measurement-per-milestone line is removed: "a system that can disagree with us" already says it.
• done → finish. done is a POSIX shell keyword (bash -c 'done x' is a syntax error), so the call could never run. finish is process-shaped: like gdb's, it returns a frame's value to its caller.

What this PR does not do

• Write any spec or code; initial-spec is next (Horizon).
• Re-cut the rest of Horizon; that is a merge requirement of initial-spec.
• Change gh land itself in the repo; it lives outside it.

Merge requirements

• cargo clippy --all-targets -- -D warnings green on the empty crate with the new lints.
• Roone has read CODE.md end to end and it reads as one document.

🤖 Generated with Claude Code

[1zeroone0]

d86898f

1. Built — CODE.md reorganized as Method (sequence, frontier/claim, boundaries) → Vocabulary (table with a Home column) → Rust / TLA+ / Lean (environment and idioms only). AGENTS.md: five line edits, one deletion. Cargo.toml lints, clippy.toml, clippy in the toolchain; README done → finish.
2. Why — Languages were parallel sections; they are one pipeline, so method comes first and languages say only how they express it. clippy.toml over cfg_attr(test, allow(...)), because allow_attributes rejects the attribute form.
3. Bloat — CODE.md is 24 bytes smaller despite adding the invariants, the method sequence and the table: the lint block that duplicated Cargo.toml is gone (Cargo.toml is the rule), and "every noun is a struct or enum" is absorbed by the Home rule.
4. Drift — Moved out, to Horizon, not deleted: TLA+ candidates (fork–exec gap, log/snapshot/fork, budget tree) and Lean candidates (Budget::split, eviction, export round-trip, pinned-prompt renderer) go to the initial-spec comment; "first Lean spec is Budget" goes to the rlm-and-budget comment. The Lean project moves from model/ to spec/.
5. Trust surface — Checked on 1.98 in a scratch crate: todo!() warns; bare #[allow] and a reason-less #[expect] are errors; #[expect(clippy::unreachable, reason)] passes; unwrap in #[cfg(test)] passes with clippy.toml. Not checked: allow-expect-in-tests, by symmetry only.
6. How it breaks — A lake project and TLA+ modules sharing spec/ may collide once both exist. #[ignore] is still counted as frontier but no lint counts it; that is grep, not a checker.
7. Not confident — The Home column's form (one column, free text) before any home exists. Whether "a fill commit names the action it implements" is practical when one body serves two actions.
8. Verify yourself — CODE.md Method section as a whole; the frontier/claim lists in Rust › Idioms; AGENTS.md line on Horizon.
9. Next steps — Finished pending your read; Horizon updates and initial-spec scoping continue on Horizon #7.