Disprove literal moving-sofa uniqueness statement - #264

Draft

DomTheDeveloper wants to merge 10 commits into

mainfrom

openai/disprove-moving-sofa-uniqueness-literal

Commits on Jul 26, 2026

Disprove literal moving-sofa uniqueness statement
DomTheDeveloper
committed
5eec6e0
Add focused moving-sofa Lean audit
DomTheDeveloper
committed
fdd85e6
Expose moving-sofa Lean diagnostics
DomTheDeveloper
committed
76b573e
Upload moving-sofa compiler diagnostics
DomTheDeveloper
committed
df5a15f
Build moving-sofa module through Lake
DomTheDeveloper
committed
10e3997
Remove moving-sofa sorry dependency and fix notation scope
DomTheDeveloper
committed
a1991e6
Run moving-sofa axiom audit after successful build
DomTheDeveloper
committed
e874ded
Prove generic null-set counterexample and specialize to moving sofa
DomTheDeveloper
committed
9d75817
Audit generic moving-sofa counterexample independently
DomTheDeveloper
committed
3ded335
Resolve moving-sofa generic counterexample elaboration
DomTheDeveloper
committed
e86cc62