# 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` → **FIXED**: replaced with `ncDerived_nonneg`, `ncDerived_zero_left`, `ncDerived_zero_right` (meaningful Q16_16 properties) |
| `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 |