docs: lead the README with the problem, not the machinery

[shitianfang]

Companion to #1 — the same treatment applied to the English README, so the two files now mirror each other section for section.

The README opened on immutable contracts, a ranked frontier, a verifier and cascade: four terms before a reader knew what any of it was for. The two failures that motivate the whole protocol — agents collide on files, PRs stall on human review — were a subordinate clause two thirds of the way down the Prove2Me paragraph.

New ## Why this exists

Puts them first, then the Prove2Me answer (move trust from review to immutable statements plus a checker), then the bridge the README never spelled out:

In Lean that checker is free: the compiler says it type-checks, and it is proved. […] build2me asks the obvious follow-up: in software, what plays the part of the compiler? The answer it commits to: every unit of work carries its own acceptance command.

Stale count fixed

all twelve contracts are Done / 12 done / 0 open predated declared-laws, which was published after root closed and is imported by no decomposition. verify.mjs derives 13 done / 0 open; the badge was already right.

The seven-session cost paragraph keeps its twelve — that run genuinely covered twelve contracts, so changing it would introduce a new error rather than fix one.

Structure

• Race 001 and the self-reference lesson become ### subsections. They are the receipts for the kernel judges admissibility, not quality and run a gate red before publishing it, and were easy to skim past as prose.
• ## Architecture renamed ## How it runs and moved next to the agent loop it describes; the lock-free consequences are now a list.
• Security and Known limits moved below the sections a new reader needs first.

Checks

No links dropped and no sections dropped (diffed the heading and link sets against HEAD). Locally verify.mjs exits 0 at 13 done / 0 open, and l4-english, l5-tool-size, l6-status-honest all exit 0.

🤖 Generated with Claude Code