For coding agents

Start with the scope boundary, then read the source declaration you will use. The Lean declaration is authoritative about hypotheses and quantifiers; the receipt is authoritative only for the exact content it names.

Required context

• Repository contract
• README and mathematical capsule
• Status and exclusions
• Claim ledger and public theorem inventory
• Trust and reproducibility

Working rules

• Use the pinned compiler and dependencies. Preserve foreign work and compile changed modules locally before any costly gate.
• Keep source, claims, examples, type checks and axiom inventory aligned. Never fabricate receipts or strengthen a theorem in prose.
• Read complete statement hypotheses. Preserve the domain and totalization conventions.
• Retain positive witnesses and strict negative fixtures. Get private/generated ownership counts from the compiled environment.

Compact machine entrance: llms.txt.