From b280d6b8e44caaa70c68df9bafd4ebec2a90a697 Mon Sep 17 00:00:00 2001 From: allaun Date: Tue, 30 Jun 2026 21:16:29 -0500 Subject: [PATCH] =?UTF-8?q?fix(e8sidon):=20levelset=20axioms=20=E2=86=92?= =?UTF-8?q?=20proven=20theorems,=20N=3D32/64=20are=20NOT=20Sidon?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Critical finding: E8LevelSet(N) is Sidon only for N≤16. N=8: {1} — 1 element, trivially Sidon ✅ (dec_trivial) N=16: {1,2} — 2 elements, all sums distinct ✅ N=32: {1,2,3} — NOT Sidon ❌ 1+3 = 2+2 (counterexample) N=64: {1,2,3} — NOT Sidon ❌ same violation This means the erdos30_e8_conditional proof (which assumed all level sets are Sidon) is vacuously true — its premise is false. Renamed: axiom levelset_{32,64}_is_sidon → theorem levelset_{32,64}_NOT_sidon axiom levelset_{8,16}_is_sidon → theorem levelset_{8,16}_is_sidon --- ERROR_INVENTORY.md | 136 ++++++++++++++++++++++++++++++ formal/CoreFormalism/E8Sidon.lean | 27 +++--- 2 files changed, 153 insertions(+), 10 deletions(-) create mode 100644 ERROR_INVENTORY.md diff --git a/ERROR_INVENTORY.md b/ERROR_INVENTORY.md new file mode 100644 index 00000000..cf58e484 --- /dev/null +++ b/ERROR_INVENTORY.md @@ -0,0 +1,136 @@ +# Error Inventory + +Both repositories build with **0 compilation errors** but have unproven theorems (sorries), vacuous proofs (`True` theorems), and trivial proofs (`by trivial`). + +## Research Stack — Semantics (8604 jobs, 0 errors) + +### Sorries (unproven theorems) — 16 total + +| File | Line | Def | +|------|------|-----| +| `Semantics/Core/T1_Coherence.lean` | 115 | `sorry` | +| | 147 | `sorry` | +| | 217 | `sorry` | +| | 233 | `sorry` | +| | 277 | `sorry` | +| | 321 | `sorry` | +| | 376 | `sorry` | +| `Semantics/Core/InformationManifold.lean` | 102 | `sorry` | +| | 130 | `sorry` | +| | 184 | `sorry` | +| | 380 | `sorry` | +| | 395 | `sorry` | +| `Semantics/EquationFractalEncoding.lean` | 598 | `sorry` | +| | 627 | `sorry` | +| | 629 | `sorry` | +| `ExtensionScaffold/Physics/NBody.lean` | 1394 | `sorry` | +| `Semantics/EquationFractalEncoding.lean` | 598 | `sorry` | +| `Semantics/PutinarBackbone.lean` | 335 | `sorry` (gap closed by SDP pipeline per comment) | +| `Semantics/UniversalField.lean` | 225 | `sorry` (pending Q16_16 lemma) | +| | 234 | `sorry` (pending finSum lemma) | +| `Semantics/HachimojiManifoldAxiom.lean` | 225 | `sorry` (geometric-series bound) | +| `Semantics/CompleteInteractionGraph.lean` | 186 | `sorry` (TODO lean-port) | +| `Semantics/GraphRank.lean` | 76 | `by sorry` (TODO lean-port) | + +### `: True` theorems — 13 total + +| File | Line | Theorem | +|------|------|---------| +| `Core/T1_Coherence.lean` | 8 | `T1_SIM_reduces_to_Fisher : True` | +| | 9 | `T2_Alcubierre_chart_consistency : True` | +| | 10 | `T3_MOIM_approximates_SIM : True` | +| | 11 | `T4_genus3_forced : True` | +| `Semantics/Biology/QuaternionGenomic.lean` | 199 | `chiralIncompatibleBoolean : True` | +| | 203 | `watsonCrickClassificationGate : True` | +| | 207 | `distanceMetricReceipt : True` | +| `Semantics/BraidSpherionBridge.lean` | 101 | `strandPair_distinct : True` | +| `Semantics/PrimitiveMatrix.lean` | 71 | `prim_adj_identity_exact : True` | +| `Semantics/RRC/Emit.lean` | 132 | `ncDerived_independence_justification : True` | +| `Semantics/TestCopyIf.lean` | 11 | `test_rfl2 : True` | +| `Semantics/Adapters/ErgodicAdditive.lean` | 101 | `polynomial_method_adapter : True` | +| `Semantics/Adapters/AlphaProofNexus/Bridge.lean` | 45 | `apn_bridge_reference : True` | + +### `by trivial` — ~200 total + +| File | Count | +|------|-------| +| `Semantics/HamiltonianVerification.lean` | ~184 (`DocumentedAuditClaim` instances) | +| `Semantics/CompressionLossComparison.lean` | 6 (`UnifiedField` well-formedness) | +| `Semantics/HamiltonianFormal.lean` | 2 (`FormalSketchClaim`) | +| `Semantics/NIICore/MorphicFieldCategory.lean` | 1 (`naturality_placeholder`) | +| `Semantics/NIICore/SheafPersistentRGHybrid.lean` | 3 (sheaf/topological/scale invariance) | +| `Semantics/NIICore/SemanticRGFlow.lean` | 1 (`continuity`) | +| `Semantics/NIICore/MereotopologicalSheafHypergraph.lean` | 1 (`gluing`) | +| `Semantics/WSM_WR_EGS_WC.lean` | 1 (domain assertion) | +| `Core/T1_Coherence.lean` | 4 (T1–T4) | +| `Semantics/Core/UnderversePacket.lean` | 1 | + +## SilverSight (3307 jobs, 0 errors) + +### Sorries (unproven theorems) — 17 total + +| File | Line | Def | +|------|------|-----| +| `formal/CoreFormalism/E8Sidon.lean` | 45 | `sigma3_multiplicative` | +| | 55-56 | `sidon_iff_no_collision` (2 sorries) | +| | 83 | `e8_conv_identity_200 : True := sorry` | +| | 106 | `e8_convolution_identity` | +| | 124 | `e8_levelset_sidon` | +| `formal/SilverSight/PIST/UnifiedCovariant.lean` | 204 | `is_Kaehler : Prop := sorry` | +| | 205 | `admits_Cartan_connection : Prop := sorry` | +| | 206 | `has_SO_1_6_holonomy : Prop := sorry` | +| | 230 | `goldenCP7 : Type := sorry` | +| | 240 | `sorry` | +| | 244 | `sorry` | +| | 248 | `sorry` | +| `formal/SilverSight/AdjugateMatrix.lean` | 60 | `sorry` | +| `formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean` | 1057 | `sorry` | +| `formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean` | 384 | `sorry` | +| | 386 | `sorry` | +| | 405 | `sorry` | +| | 407 | `sorry` | + +### `: True` axioms/theorems — 6 total + +| File | Line | Theorem | +|------|------|---------| +| `formal/CoreFormalism/HopfFibration.lean` | 97 | `duran_is_braid_crossing : True := sorry` | +| | 114 | `corkscrew_duran_correspondence : True := sorry` | +| `formal/CoreFormalism/BraidStateN.lean` | 304 | `regime_classification : True := sorry` | +| `formal/CoreFormalism/E8Sidon.lean` | 83 | `e8_conv_identity_200 : True := sorry` | +| `formal/SilverSight/RRC/Emit.lean` | 131 | `ncDerived_independence_justification : True := trivial` | +| `formal/CoreFormalism/BraidSpherionBridge.lean` | 102 | `strandPair_distinct : True` | + +### `by trivial` — 0 + +## Warnings (both repos) + +### Unused variables +- `Semantics/AVM.lean:120` — `method` +- `Semantics/SSMS.lean:588` — `hB` +- `Semantics/KdVBurgersPDE.lean:40-41` — `h1`, `h2` +- `Semantics/Burgers2DPDE.lean:44-46` — `h1`, `h2` +- `Semantics/Burgers2DPDE.lean:187` — `maxVal` +- `Semantics/FAMM.lean:110-132` — `newBank`, `currentCell` +- `formal/CoreFormalism/E8Sidon.lean:131` — `h_sidon` + +### Unused simp arguments +- `Semantics/SDPVerify.lean:350,375` — `ih` +- `Semantics/TreeDIATKruskal.lean:56,106,121` — `ihL`, `ihR`, `treeNodeCountExact`, `treeLeafCountExact` +- `Semantics/N3L_Energy.lean:456-478` — `integrand_simp` + +### Deprecated API (in Sparkle dependency, not project code) +- `String.trimLeft` → `String.trimAsciiStart` in `Sparkle/Backend/CppSim.lean` +- `String.trim` → `String.trimAscii` in `Sparkle/Backend/CppSim.lean` +- `String.dropRight` → `String.dropEnd` in `Sparkle/Backend/CppSim.lean` +- `String.mk` → `String.ofList` in `Sparkle/Verification/Equivalence.lean` + +## Summary + +| Metric | Research Stack | SilverSight | +|--------|---------------|-------------| +| Build jobs | 8604 | 3307 | +| Compilation errors | **0** | **0** | +| Sorries (total) | 16 | 17 | +| `: True` theorems | 13 | 6 | +| `by trivial` proofs | ~200 | 0 | diff --git a/formal/CoreFormalism/E8Sidon.lean b/formal/CoreFormalism/E8Sidon.lean index b1c086ee..ecab7b61 100644 --- a/formal/CoreFormalism/E8Sidon.lean +++ b/formal/CoreFormalism/E8Sidon.lean @@ -146,18 +146,25 @@ theorem erdos30_e8_conditional (h_sidon : ∀ N, 1 ≤ N → IsSidon (E8LevelSet -- let rhs := sigma3 n + 120 * ((List.range n).map (λ j => sigma3 j * sigma3 (n - j))).sum -- sigma7 n ≠ rhs) -/-- The Sidon property for the E8 level set at N=8. - TODO(E8Sidon): structural proof blocked on sigma3_multiplicative. - This is a computational receipt — verified externally. -/ -axiom levelset_8_is_sidon : IsSidon (E8LevelSet 8) +/-- E8LevelSet 8 = {1} is trivially Sidon (1 element, no pairs to collide). -/ +theorem levelset_8_is_sidon : IsSidon (E8LevelSet 8) := by + unfold E8LevelSet IsSidon + decide -/-- The Sidon property for the E8 level set at N=16. -/ -axiom levelset_16_is_sidon : IsSidon (E8LevelSet 16) +/-- E8LevelSet 16 = {1, 2} has all sums distinct (1+1=2, 1+2=3, 2+2=4). -/ +theorem levelset_16_is_sidon : IsSidon (E8LevelSet 16) := by + unfold E8LevelSet IsSidon + decide -/-- The Sidon property for the E8 level set at N=32. -/ -axiom levelset_32_is_sidon : IsSidon (E8LevelSet 32) +/-- E8LevelSet 32 = {1, 2, 3} is NOT Sidon: 1+3 = 2+2 = 4. + This is the first violation — the Sidon property breaks at N=32. -/ +theorem levelset_32_NOT_sidon : ¬ IsSidon (E8LevelSet 32) := by + unfold E8LevelSet IsSidon + decide -/-- The Sidon property for the E8 level set at N=64. -/ -axiom levelset_64_is_sidon : IsSidon (E8LevelSet 64) +/-- E8LevelSet 64 = {1, 2, 3} is also NOT Sidon (same set as N=32, same violation). -/ +theorem levelset_64_NOT_sidon : ¬ IsSidon (E8LevelSet 64) := by + unfold E8LevelSet IsSidon + decide end SilverSight.E8Sidon