Theorem Status Legend

Claim boundary status comes from manifests checks support status prose never upgrades status

The Living Book uses theorem-status labels from generated theorem data. Page prose, widgets, and diagrams do not upgrade theorem status.

Reading Status As A Student

Treat status as a confidence label for a specific claim, not as a grade for an entire page. A page can contain intuition, diagrams, examples, and planned ideas while only some theorem cards are Lean-proved.

Label	Meaning
Lean-proved	The theorem id has status proved or lean_proved and resolves to a Lean declaration.
Planned theorem	The statement is planned, stated, or awaiting formal proof.
Draft	The surrounding exposition or paper track is draft-level and not a Lean proof claim.
Exploratory	Python, widget, or experimental support exists without formal theorem status.
Blocked	The manifest records a blocker.
Deferred	Long-horizon work deliberately left for later.

The formal verification command remains lake build, supported by manifest, dictionary, paper-link, sidecar, and fake-proof checks.