# SilverSight Theorem Triage Report

**Generated**: 2026-06-22T17:47:46Z
**Source**: `extraction/lean_concepts.json` + `ene.prover_state` (neon-64gb)
**Total theorems**: 3057

## Summary

| Tier | Theorems | Modules | Portability |
|------|----------|---------|-------------|
| Core (SilverSight import path) | 118 | 6 | direct |
| Verified foundations | 1591 | 121 | direct |
| Extension modules | 1084 | 291 | needs_work |
| Quarantined (needs review) | 137 | 15 | needs_work |
| Test/demo/deprecated | 127 | 18 | excluded |
| **TOTAL** | **3057** | | |

## Sorry Theorems (10)

These theorems contain `sorry` and must be proved before porting:

| Theorem | Tier | Module |
|---------|------|--------|
| `Semantics.UniversalField.phiUniversalNonNeg` | TIER_4_QUARANTINE | UniversalField |
| `Semantics.UniversalField.phiUniversalBounded` | TIER_4_QUARANTINE | UniversalField |
| `Semantics.HachimojiManifoldAxiom.bms_from_manifold` | TIER_4_QUARANTINE | HachimojiManifoldAxiom |
| `Semantics.GraphRank.cleanMerge_preservesGap` | TIER_1_CORE | GraphRank |
| `Semantics.ErdosRenyiPipeline.collisionEnergy_zero_iff` | TIER_4_QUARANTINE | ErdosRenyiPipeline |
| `Semantics.ErdosRenyiPipeline.erdos_renyi_bridge` | TIER_4_QUARANTINE | ErdosRenyiPipeline |
| `Semantics.ErdosRenyiPipeline.mott_threshold` | TIER_4_QUARANTINE | ErdosRenyiPipeline |
| `Semantics.EquationFractalEncoding.integrity_correct` | TIER_4_QUARANTINE | EquationFractalEncoding |
| `Semantics.EquationFractalEncoding.subtree_fold_empty` | TIER_4_QUARANTINE | EquationFractalEncoding |
| `Semantics.CompleteInteractionGraph.walkMatrix_off_diag` | TIER_4_QUARANTINE | CompleteInteractionGraph |

## TIER_1_CORE: SilverSight Import Path (118 theorems)

These theorems are in the canonical SilverSight import chain and should be ported first.

### `FixedPoint` (50 theorems)

| Theorem | Status | Portability |
|---------|--------|-------------|
| `ext` | ok | direct |
| `q16Clamp_monotone` | ok | direct |
| `q16Clamp_id_of_inRange` | ok | direct |
| `ext` | ok | direct |
| `epsilon_toInt_pos` | ok | direct |
| `maxVal_toInt` | ok | direct |
| `minVal_toInt` | ok | direct |
| `ofRawInt_toInt_ge` | ok | direct |
| `ofRawInt_toInt_nonneg` | ok | direct |
| `ofRawInt_toInt` | ok | direct |
| `ofRawInt_toInt_eq_nonneg` | ok | direct |
| `ofRawInt_toInt_eq_general` | ok | direct |
| `ofRawInt_toInt_eq_clamp` | ok | direct |
| `ofRawInt_monotone` | ok | direct |
| `add_nonneg_monotone` | ok | direct |
| `zero_mul` | ok | direct |
| `mul_zero` | ok | direct |
| `sub_self` | ok | direct |
| `add_zero` | ok | direct |
| `zero_add` | ok | direct |
| `sqrt_zero` | ok | direct |
| `sqrt_one` | ok | direct |
| `one_mul` | ok | direct |
| `mul_one` | ok | direct |
| `toInt_eq_zero_iff` | ok | direct |
| `zero_div` | ok | direct |
| `mul_self_nonneg` | ok | direct |
| `mul_toInt_nonneg` | ok | direct |
| `ofRaw_toInt_nonneg` | ok | direct |
| `mk_lt_half_nonneg` | ok | direct |
| `add_pos_of_pos` | ok | direct |
| `add_one_omega_ge_one` | ok | direct |
| `toInt_nonneg_le_maxVal` | ok | direct |
| `epsilon_add_pos` | ok | direct |
| `abs_sub_comm` | ok | direct |
| `sub_eq_add_neg` | ok | direct |
| `mul_mono_left` | ok | direct |
| `mul_mono_right` | ok | direct |
| `add_le_add` | ok | direct |
| `abs_nonneg` | ok | direct |
| `add_toInt_of_no_sat` | ok | direct |
| `sub_toInt_of_no_sat` | ok | direct |
| `mul_floor_le` | ok | direct |
| `mul_floor_ge` | ok | direct |
| `mul_floor_error` | ok | direct |
| `ofNat_le` | ok | direct |
| `ofNat_nonneg` | ok | direct |
| `add_le_add` | ok | direct |
| `ext` | ok | direct |
| `piPandigitalCorrect` | ok | direct |

### `SidonSets` (48 theorems)

| Theorem | Status | Portability |
|---------|--------|-------------|
| `IsSidonMod` | ok | direct |
| `IsIntervalSidon` | ok | direct |
| `IsSidon` | ok | direct |
| `sidonMaximum_isSidonMaximum` | ok | direct |
| `isSidonMaximum_unique` | ok | direct |
| `IsIntervalSidon` | ok | direct |
| `sidonMaximum_le_sqrt_two` | ok | direct |
| `IsSidon` | ok | direct |
| `IsIntervalSidon` | ok | direct |
| `IsIntervalSidon` | ok | direct |
| `IsSidon` | ok | direct |
| `johnson_numerical` | ok | direct |
| `incidence_inequality` | ok | direct |
| `sidon_intersection_sum_bound` | ok | direct |
| `IsIntervalSidon` | ok | direct |
| `lindstrom_monotone` | ok | direct |
| `IsIntervalSidon` | ok | direct |
| `sidonMaximum_le_lindstrom` | ok | direct |
| `finrank_ext` | ok | direct |
| `trace_surjective` | ok | direct |
| `finrank_ker_trace` | ok | direct |
| `minpoly_degree_eq_three` | ok | direct |
| `linIndep_smul_v` | ok | direct |
| `no_proper_invariant_subspace` | ok | direct |
| `finrank_inf_of_distinct_twodim` | ok | direct |
| `finrank_inf_scaled_ker_trace` | ok | direct |
| `singer_quotient_sidon` | ok | direct |
| `singer_sidon_set_of` | ok | direct |
| `singer_sidon_set` | ok | direct |
| `singerFamilyHypothesis_holds` | ok | direct |
| `IsSidonMod` | ok | direct |
| `sidonMaximum_pos` | ok | direct |
| `sidonMaximum_mono` | ok | direct |
| `SidonChaosAddresses_isSidon` | ok | direct |
| `SidonChaosAddresses_card` | ok | direct |
| `addressOfStrand_strandOfAddress` | ok | direct |
| `strandOfAddress_some` | ok | direct |
| `sidon_chaos_address_mem` | ok | direct |
| `sidon_chaos_address_pow2` | ok | direct |
| `sidon_chaos_address_mod8_eq` | ok | direct |
| `sidon_chaos_address_surjective` | ok | direct |
| `chaos_trajectory_no_collision` | ok | direct |
| `sidon_guided_basin_unique` | ok | direct |
| `sidon_address_1` | ok | direct |
| `sidon_address_valid_chaos` | ok | direct |
| `sidon_address_unique_single` | ok | direct |
| `sidon_8strand_sum_count` | ok | direct |
| `sidon_8strand_full_capacity` | ok | direct |

### `BraidEigensolid` (9 theorems)

| Theorem | Status | Portability |
|---------|--------|-------------|
| `eigensolid_convergence` | ok | direct |
| `receipt_invertible` | ok | direct |
| `IsTopologicallyTrivial_iff` | ok | direct |
| `eigensolid_trivial` | ok | direct |
| `inZeroGenusLayer_iff` | ok | direct |
| `jsrr_residue_fixed` | ok | direct |
| `jsrr_profile_fixed` | ok | direct |
| `kkt_block_bounded` | ok | direct |
| `zero_genus_kkt_bounded` | ok | direct |

### `GraphRank` (4 theorems)

| Theorem | Status | Portability |
|---------|--------|-------------|
| `badLink_decidable` | ok | direct |
| `isClean_decidable` | ok | direct |
| `activeBins_empty` | ok | direct |
| `cleanMerge_preservesGap` | !! | blocked |

### `FixedPointBridge` (4 theorems)

| Theorem | Status | Portability |
|---------|--------|-------------|
| `roundTripQ0_zero` | ok | direct |
| `roundTripQ16_zero` | ok | direct |
| `q0ToQ16_zero` | ok | direct |
| `q16ToQ0_zero` | ok | direct |

### `RRC.PolyFactorIdentity` (3 theorems)

| Theorem | Status | Portability |
|---------|--------|-------------|
| `limbDecompose_polyEval_roundtrip` | ok | direct |
| `zeroLimbs_bound_terms` | ok | direct |
| `shortSleeve_mono_zero_prepend` | ok | direct |

## TIER_4_QUARANTINE: Needs Human Review (137 theorems)

These modules are quarantined — they may contain sorries, unverified claims, or
logic that doesn't belong in SilverSight. Each needs a human decision: revive,
rewrite, or permanently exclude.

### `ErdosRenyiPipeline` (21 theorems) ⚠️ HAS SORRY

- `sidon_iff_no_collision` — DEFINED
- `collisionEnergy_nonneg` — DEFINED
- `collisionEnergy_zero_iff` — SORRY
- `erdos_renyi_bridge` — SORRY
- `mott_threshold` — SORRY
- `sidon_zero_quadruplons` — DEFINED
- `quadruplon_supercritical` — DEFINED
- `c36_preserves_collisions` — DEFINED
- `c36_gap_preservation` — DEFINED
- `c36_sidon_consequence` — DEFINED
- `unified_phase_transition` — DEFINED
- `structure_bonus` — DEFINED
- `crt_sieve_iff_not_prime_pow` — DEFINED
- `prime_barrier_k10` — DEFINED
- `pipeline_with_erdos_renyi` — DEFINED
- `rcp_pipeline_ordering` — DEFINED
- `pipeline_kissing_ratio` — DEFINED
- `sidon_regime_below_φ_LT` — DEFINED
- `mott_regime_bounded_by_φ_RCP` — DEFINED
- `lattice_ordering_gap` — DEFINED
- `rcp_phases_partition` — DEFINED

### `UnifiedConvictionFlow` (17 theorems)

- `multiplicationDistributesNat` — DEFINED
- `degeneracyPenaltyBounded` — DEFINED
- `productBoundedNat` — DEFINED
- `weightedCombinationBoundedReal` — DEFINED
- `informationDensityBoundedReal` — DEFINED
- `informationDensityNonneg` — DEFINED
- `fullRegistry_nonempty` — DEFINED
- `numerator_nonneg` — DEFINED
- `geometry_pos` — DEFINED
- `energy_pos` — DEFINED
- `phi_nonneg` — DEFINED
- `lawWeighted_nonneg` — DEFINED
- `lawWeighted_bounded` — DEFINED
- `phiAugmented_ge_phi` — DEFINED
- `phiAugmented_nonneg` — DEFINED
- `flowAugmented_differs_on_rho` — DEFINED
- `unifiedRegistry_size` — DEFINED

### `ImaginarySemanticTime` (17 theorems)

- `iUnitSemanticOne` — DEFINED
- `mengerSemanticTimeK0` — DEFINED
- `p04SemanticTimeCorrect` — DEFINED
- `p04SemanticTimeMagnitude` — DEFINED
- `semanticPeriodRatioIs3_k0` — DEFINED
- `semanticPeriodRatioIs3_k1` — DEFINED
- `semanticPeriodRatioIs3_k2` — DEFINED
- `semanticPeriodRatioIs3_k5` — DEFINED
- `semanticPeriodRatioIs3_k10` — DEFINED
- `observerProjectionPreservesSemantic` — DEFINED
- `p04ProjectedPhysicalMagnitude` — DEFINED
- `p04ProjectedPhysicalGreaterThan60` — DEFINED
- `trivial_observer_sees_zero` — DEFINED
- `sieve_independent_of_P0` — DEFINED
- `reconcileObservers_correct_mod_ℓ1` — DEFINED
- `reconcileObservers_correct_mod_ℓ2` — DEFINED
- `reconcileObservers_recovers_coordinate` — DEFINED

### `HumanNeuralCompression` (15 theorems)

- `topologicalPreservationWithinBudget` — DEFINED
- `layer1ErrorWithinBudget` — DEFINED
- `layer2ErrorWithinBudget` — DEFINED
- `layer3ErrorWithinBudget` — DEFINED
- `layer4ErrorWithinBudget` — DEFINED
- `totalRatioAchievesTarget` — DEFINED
- `totalErrorBelowOnePercent` — DEFINED
- `pumpPhaseWindowsWithinBounds` — DEFINED
- `snowballGrowthWithinBounds` — DEFINED
- `electronOrbitalLoadsWithinBounds` — DEFINED
- `sigma65ConfidenceAchievedWithPumpPhase` — DEFINED
- `effectiveCompressionAchievesTarget` — DEFINED
- `compressedSizeWithinTarget` — DEFINED
- `temporalSamplingPreservesInvariant` — DEFINED
- `pumpPhaseExtendsSafeWindow` — DEFINED

### `NetworkedSelfSolvingSpace` (10 theorems)

- `solitonConvergence` — DEFINED
- `boundedPropagationTime` — DEFINED
- `asyncSelfSolvingPreservation` — DEFINED
- `eventualConsistency` — DEFINED
- `globalConsistency` — DEFINED
- `communicationCostMonotonicity` — DEFINED
- `networkedDescentConvergence` — DEFINED
- `mengerSpongeErasureBasin` — DEFINED
- `holographicQuantumEraser` — DEFINED
- `topologicalPruningRestoresInterference` — DEFINED

### `HumanNeuralCompressionVerification` (10 theorems)

- `minimumCompressionRatio_eq` — DEFINED
- `idealCompressionRatio_eq` — DEFINED
- `effectiveUncompressedGb_eq` — DEFINED
- `effectiveMinimumRatio_eq` — DEFINED
- `byte_budget_strictly_smaller` — DEFINED
- `lossless_witness_requires_capacity` — DEFINED
- `no_injective_compression_to_smaller_fintype` — DEFINED
- `no_lossless_universal_compression` — DEFINED
- `arbitrary_lossless_compression_impossible` — DEFINED
- `onePbTo800Gb_needs_extra_model_structure` — DEFINED

### `EntropyPhaseEngine` (10 theorems)

- `complexity_penalty_monotone` — DEFINED
- `modelType_exhaustive` — DEFINED
- `complexity_ordering_monotone` — DEFINED
- `allCandidates_length` — DEFINED
- `noiseCandidate_complexity_zero` — DEFINED
- `minCandidate_singleton` — DEFINED
- `anti_puppy_box_theorem` — DEFINED
- `nanokernel_isolation` — DEFINED
- `fpga_extraction_correctness` — DEFINED
- `universal_electron_verification` — DEFINED

### `EquationFractalEncoding` (9 theorems) ⚠️ HAS SORRY

- `manifold_distance_symmetric` — DEFINED
- `merkle_root_empty` — DEFINED
- `merkle_root_singleton` — DEFINED
- `mixHash_non_comm` — DEFINED
- `integrity_correct` — SORRY
- `sidon_address_valid` — DEFINED
- `chaos_game_bounded` — DEFINED
- `subtree_fold_empty` — SORRY
- `integrity_reflexive` — DEFINED

### `CompleteInteractionGraph` (7 theorems) ⚠️ HAS SORRY

- `completeAdj_edge_count` — DEFINED
- `completeAdj_max_edges` — DEFINED
- `completeAdj_step_exists` — DEFINED
- `completeAdj_diameter_one` — DEFINED
- `completeAdj_not_sidon_witness` — DEFINED
- `completeAdj_contains_all` — DEFINED
- `walkMatrix_off_diag` — SORRY

### `AgenticTheorems` (6 theorems)

- `assignmentRespectsCapabilities` — DEFINED
- `dependenciesRespected` — DEFINED
- `orchestrationTermination` — DEFINED
- `synergyImprovesPerformance` — DEFINED
- `agentFieldBounded` — DEFINED
- `loadPenaltyDecreasesField` — DEFINED

### `AgentSwarmTemplateAlignment` (5 theorems)

- `classifyTemplateNeverReviewed` — DEFINED
- `noReceiptsHold` — DEFINED
- `invalidReceiptBlocks` — DEFINED
- `codeReviewGraphCandidate` — DEFINED
- `unsafeSupportGraphHeld` — DEFINED

### `EntropyMeasures` (4 theorems)

- `defaultThresholdsValid` — DEFINED
- `adaptiveEntropySelectsShannon` — DEFINED
- `adaptiveEntropySelectsCollision` — DEFINED
- `adaptiveEntropySelectsMin` — DEFINED

### `HachimojiManifoldAxiom` (3 theorems) ⚠️ HAS SORRY

- `HachimojiBase` — DEFINED
- `bms_from_manifold` — SORRY
- `goormaghtigh_from_manifold` — DEFINED

### `UniversalField` (2 theorems) ⚠️ HAS SORRY

- `phiUniversalNonNeg` — SORRY
- `phiUniversalBounded` — SORRY

### `AgenticOrchestration` (1 theorems)

- `researchPipelineIsAcyclic` — DEFINED

## TIER_2_FOUNDATION: Top Modules (1591 theorems total)

| Module | Theorems |
|--------|----------|
| `HamiltonianVerification` | 324 |
| `DeltaGCLCompression` | 62 |
| `HamiltonianFormal` | 61 |
| `E8Sidon` | 51 |
| `SpatialHashCodec` | 36 |
| `DomainDetector` | 30 |
| `CouchFilterNormalization` | 28 |
| `HCMMR.Laws.Law15_Field` | 27 |
| `Physics.UniversalBridge` | 26 |
| `Q16InverseProof` | 25 |
| `Functions.WSM_WR_EGS_WC_Mathlib` | 25 |
| `ExtendedManifoldEncoding` | 22 |
| `Core.FoldedPointManifold` | 21 |
| `SpherionTwinPrime` | 20 |
| `Physics.PreRegisteredPredictions` | 20 |
| `N3L_Energy` | 20 |
| `AdjugateMatrix` | 20 |
| `BurgersPDE` | 19 |
| `TreeDIATKruskal` | 16 |
| `FractionScan` | 16 |

## Prover State Cross-Reference

- Verified in prover_state: 2987
- Raw in prover_state: 9
- Not in prover_state: 61