Disprove literal moving-sofa uniqueness statement

.github/workflows/openai-moving-sofa-literal-audit.yml

@@ -0,0 +1,78 @@
+name: OpenAI moving-sofa literal counterexample audit
+
+on:
+  push:
+    branches:
+      - openai/disprove-moving-sofa-uniqueness-literal
+    paths:
+      - 'FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean'
+      - '.github/workflows/openai-moving-sofa-literal-audit.yml'
+  pull_request:
+    paths:
+      - 'FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean'
+      - '.github/workflows/openai-moving-sofa-literal-audit.yml'
+  workflow_dispatch:
+
+jobs:
+  audit:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install pinned Lean toolchain
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Restore Lake cache
+        uses: actions/cache@v4
+        with:
+          path: .lake
+          key: ${{ runner.os }}-lake-${{ hashFiles('lake-manifest.json', 'lean-toolchain') }}
+          restore-keys: |
+            ${{ runner.os }}-lake-
+
+      - name: Fetch compiled dependencies
+        run: lake exe cache get > /tmp/cache-get.log
+
+      - name: Reject proof holes and trust escapes
+        run: |
+          set -euo pipefail
+          file='FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean'
+          if grep -nE '\b(sorry|admit|unsafe|axiom)\b|native_decide|Lean\.(ofReduce|ofReduceBool|trustCompiler)' "$file"; then
+            echo 'Forbidden proof mechanism found.'
+            exit 1
+          fi
+
+      - name: Compile exact counterexample module
+        run: |
+          lake build FormalConjectures.Wikipedia.MovingSofaLiteralCounterexample \
+            > /tmp/moving-sofa-lean.log 2>&1
+          cat /tmp/moving-sofa-lean.log
+
+      - name: Upload compiler diagnostic
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: moving-sofa-lean-log
+          path: /tmp/moving-sofa-lean.log
+
+      - name: Audit axiom-clean generic theorem
+        run: |
+          cat > /tmp/MovingSofaGenericAxioms.lean <<'EOF'
+          import FormalConjectures.Wikipedia.MovingSofaLiteralCounterexample
+          #print axioms MovingSofa.volume_does_not_characterize_exact_set
+          EOF
+          lake env lean /tmp/MovingSofaGenericAxioms.lean | tee /tmp/generic-axioms.log
+          if grep -E 'sorryAx|Lean\.(ofReduce|ofReduceBool|trustCompiler)' /tmp/generic-axioms.log; then
+            echo 'Forbidden axiom dependency found in generic theorem.'
+            exit 1
+          fi
+
+      - name: Record exact-wrapper axioms
+        run: |
+          cat > /tmp/MovingSofaExactAxioms.lean <<'EOF'
+          import FormalConjectures.Wikipedia.MovingSofaLiteralCounterexample
+          #print axioms MovingSofa.sofaConstant_eq_volume_iff_eq_gerversSofa_false
+          EOF
+          lake env lean /tmp/MovingSofaExactAxioms.lean | tee /tmp/exact-axioms.log

FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean

@@ -0,0 +1,90 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Wikipedia.MovingSofa
+
+/-!
+# Literal counterexample to moving-sofa uniqueness
+
+The catalog's uniqueness declaration quantifies over every set and uses literal
+set equality. Lebesgue volume is unchanged by inserting or deleting a singleton,
+so no set can be uniquely characterized among all sets by its volume alone.
+
+This only disproves the declaration as written. A corrected uniqueness theorem
+must restrict to valid moving sofas and should likely identify sets modulo null
+sets or impose suitable regularity.
+-/
+
+namespace MovingSofa
+
+open MeasureTheory
+open scoped ENNReal Real unitInterval EuclideanGeometry
+
+private abbrev Plane := ℝ²
+
+/-- Under atomless planar volume, no fixed number can characterize one exact set by volume alone. -/
+@[category research solved, AMS 28 49]
+theorem volume_does_not_characterize_exact_set (c : ℝ≥0∞) (g : Set Plane) :
+    ¬ (∀ s : Set Plane, c = volume s ↔ s = g) := by
+  intro h
+  have hconst : c = volume g := (h g).2 rfl
+  by_cases hg : g = Set.univ
+  · let p : Plane := 0
+    let s : Set Plane := ({p}ᶜ)
+    have huniv : (Set.univ : Set Plane) = insert p ({p}ᶜ) := by
+      ext x
+      by_cases hx : x = p <;> simp [hx]
+    have hae : (Set.univ : Set Plane) =ᵐ[volume] s := by
+      rw [huniv]
+      simpa [s] using (insert_ae_eq_self (μ := volume) p ({p}ᶜ))
+    have hvol : volume s = volume g := by
+      rw [hg]
+      exact (measure_congr hae).symm
+    have hsconst : c = volume s := hconst.trans hvol.symm
+    have hseq : s = g := (h s).1 hsconst
+    have hpg : p ∈ g := by
+      rw [hg]
+      simp
+    have hps : p ∈ s := by
+      rw [hseq]
+      exact hpg
+    simpa [s] using hps
+  · obtain ⟨p, hp⟩ : ∃ p : Plane, p ∉ g := by
+      by_contra hn
+      push_neg at hn
+      exact hg (Set.eq_univ_of_forall hn)
+    let s : Set Plane := insert p g
+    have hae : s =ᵐ[volume] g := by
+      simpa [s] using (insert_ae_eq_self (μ := volume) p g)
+    have hvol : volume s = volume g := measure_congr hae
+    have hsconst : c = volume s := hconst.trans hvol.symm
+    have hseq : s = g := (h s).1 hsconst
+    have hps : p ∈ s := by simp [s]
+    have hpg : p ∈ g := by
+      rw [← hseq]
+      exact hps
+    exact hp hpg
+
+/-- The moving-sofa uniqueness declaration is false as literally quantified over all sets. -/
+@[category research solved, AMS 49]
+theorem sofaConstant_eq_volume_iff_eq_gerversSofa_false :
+    ¬ (∀ s : Set ℝ², sofaConstant = volume s ↔ s = gerversSofa) :=
+  volume_does_not_characterize_exact_set sofaConstant gerversSofa
+
+#print axioms volume_does_not_characterize_exact_set
+#print axioms sofaConstant_eq_volume_iff_eq_gerversSofa_false
+
+end MovingSofa