Audit Dedekind answer gap and moving-sofa misformalization - #265

Draft

DomTheDeveloper wants to merge 10 commits into

mainfrom

agent/low-hanging-fruit-audit

Commits on Jul 26, 2026

Audit low-hanging Dedekind and moving-sofa targets
DomTheDeveloper
committed
fbdf85f
Build low-hanging fruit audit in main Lean library
DomTheDeveloper
committed
e3f3b94
Separate clean Dedekind answer from admitted formula
DomTheDeveloper
committed
1964225
Add focused low-hanging fruit Lean audit
DomTheDeveloper
committed
0f765b5
Build exact audit module through Lake
DomTheDeveloper
committed
56af5b9
Use pinned Mathlib measure lemma
DomTheDeveloper
committed
f348928
Generalize moving-sofa uniqueness refutation
DomTheDeveloper
committed
3a27725
Audit generalized moving-sofa refutation
DomTheDeveloper
committed
609db2e
Remove obsolete duplicate audit module
DomTheDeveloper
committed
e24f08e
Keep only axiom-clean audit results
DomTheDeveloper
committed
ea37fdb