allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(e8sidon): levelset axioms → proven theorems, N=32/64 are NOT Sidon

Browse source 
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
This commit is contained in:
allaun 2026-06-30 21:16:29 -05:00
parent c5e23a0b46
commit b280d6b8e4
2 changed files with 153 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

136
ERROR_INVENTORY.md Normal file
View file

@ -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 |

27
formal/CoreFormalism/E8Sidon.lean
View file

@ -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