v1.0: complete formalization of the 2D area law

Main theorem and every proposition of openai/math family 265a proved in Lean 4 with no sorry; statements frozen 2026-10-13 and audited against the paper (docs/StatementAudit.md); comparator pair included. Public since 2026-10-16.