Write down the method as practiced

[1zeroone0]

The method in AGENTS.md and CODE.md, as practiced in #11, with nothing left that ages.

What this PR does

• AGENTS.md: evidence outranks every artifact. When code or a measurement disagrees with a spec, doc or decision, it changes in that PR; it is never defended.
• AGENTS.md: a PR that changes what the spec says opens with that change, TLC green, before any code (replaces the "seed's shape" rule, which CODE.md never defined).
• CODE.md: removes the "unpracticed" note, the "green before any Rust exists" lines, and the pointer to "the first Lean PR"; each aged or pointed outside the file.
• CODE.md TLA+: two practices from Specify cead as a system in TLA+ #11. Every property has a mutation TLC catches. Committed cfgs run in about a minute; larger bounds are one-off runs recorded in the PR.
• CODE.md Lean: green before the Rust it specifies, per function.

What this PR does not do

• Change the pipeline, the vocabulary, or the Rust rules.
• Decide how Lean outputs reach cargo test (open in Horizon Horizon #7: agent and meters).

Merge requirements

• No statement in AGENTS.md or CODE.md depends on the state of a PR or on time.
• Each removed rule is either said once elsewhere or no longer true.

🤖 Generated with Claude Code

[1zeroone0]

3512a45

1. Built — AGENTS.md: one rule added to the wall paragraph (evidence outranks every artifact); the first-commit rule restated for a spec that exists. CODE.md: three aged lines removed, two TLA+ practices added, Lean's gate made per function.
2. Why — Specify cead as a system in TLA+ #11 was the method's first practice. Lines that described the method's state ("unpracticed", "before any Rust exists", "the first Lean PR") would drift; practices it proved (a mutation per property, fast committed cfgs, receipt runs in the PR) were written nowhere.
3. Bloat — CODE.md's "when code disagrees with it, the spec changes in that PR" folded into the general rule in AGENTS.md: said once.
4. Drift — Three time-bound statements removed; nothing points outside its file.
5. Trust surface — Prose.
6. How it breaks — "Evidence outranks every artifact" can be read as licence to change a spec whenever code is inconvenient; the wall paragraph above it (re-derive, never patch) is what bounds it.
7. Not confident — "about a minute" for committed cfgs is a number from one PR.
8. Verify yourself — The two AGENTS.md lines.
9. Next steps — Finished: all merge requirements met, ready for review.