Disprove literal moving-sofa uniqueness statement

[DomTheDeveloper]

Result

The literal declaration

∀ s : Set ℝ², sofaConstant = volume s ↔ s = gerversSofa

is false. Lebesgue volume is unchanged by inserting or deleting a singleton, so no exact set can be characterized among all sets solely by its volume.

The branch proves the stronger generic theorem:

volume_does_not_characterize_exact_set
  (c : ℝ≥0∞) (g : Set ℝ²) :
  ¬ (∀ s : Set ℝ², c = volume s ↔ s = g)

and specializes it to sofaConstant and gerversSofa.

Verification

Focused audit run 30206088582 passed:

• no sorry, admit, native_decide, custom axiom, unsafe declaration, or compiler-trust escape in the new source;
• exact module compilation;
• axiom audit of the generic theorem, depending only on propext, Classical.choice, and Quot.sound;
• successful compilation and recorded axiom footprint of the exact moving-sofa wrapper.

Existing catalog limitation

The exact wrapper inherits sorryAx from the pre-existing definition of gerversSofa, because that object is built using the catalog theorem ABφθSpec.existsUnique, whose body is still sorry. The counterexample proof itself is hole-free and the generic theorem is axiom-clean, but the exact wrapper cannot pass a no-sorryAx transitive audit until that underlying definition is completed or refactored.

Qualification

This does not refute a corrected geometric uniqueness theorem. Such a theorem must restrict s to valid moving sofas and likely use equality modulo null sets or impose regularity assumptions.

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.