Audit Dedekind answer gap and moving-sofa misformalization

[DomTheDeveloper]

Findings

• DedekindNumber.M_eq_via_antichains gives a clean formal answer M = answer(M') from the existing theorem M_eq_M'.
• This is not a new mathematical solution of the Dedekind-number formula problem. The intended Kisielewicz formula still depends on the admitted M_eq_kisielewiczFormula and therefore exposes sorryAx.
• MovingSofa.no_literal_volume_unique proves a stronger general fact: no set can be the literal unique set having maximal volume, because deleting a singleton preserves volume while changing the set.
• Therefore the repository's current moving-sofa uniqueness statement is false as written. It omits a moving-sofa admissibility condition and uses literal set equality.
• The exact specialization mentioning gerversSofa currently inherits sorryAx through the admitted existence theorem used to define Gerver's constants; the generalized refutation is the clean audited theorem.

Validation

The focused audit builds FormalConjectures.Other.LowHangingFruitAudit and separately prints the axioms of only the two clean results. The gate rejects sorryAx, Lean.ofReduceBool, and Lean.trustCompiler.

Final focused run: green.

'DedekindNumber.M_eq_via_antichains' depends on axioms:
[propext, Classical.choice, Quot.sound]

'MovingSofa.no_literal_volume_unique' depends on axioms:
[propext, Classical.choice, Quot.sound]

Status

Draft audit/correction work only. This should not be described upstream as solving the mathematical Dedekind formula or moving-sofa uniqueness problem. The draft is labeled ci:full so the repository-wide build also runs.

[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.