allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-08-09 08:55:46 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
Research-Stack/6-Documentation/docs/plans/SilverSight_theorem_triage.md
allaun 73db623848 feat(silversight): Phase 1 core + claim promotions + theorem triage 
Phase 1 core (7 new Lean files, 3307 jobs, 0 errors):
- Schema.lean: Schema class with 6 type instances
- WireFormat.lean: WireFormat structure + Layout enum
- ProductSchema.lean: Schema (α × β) instance
- ProductWireFormat.lean: Row-major pair encoders with roundTrip proofs
- Receipt.lean: Receipt structure + GateType enum
- Bind.lean: bindReceipt composition + 8 theorems
- SilverSight.lean: root import module

Claim promotions (3 claims → VERIFIED):
- silversight_claim_q16_unified: FixedPoint.lean 12 theorems, 0 sorry
- silversight_claim_eigensolid_convergence: BraidEigensolid.lean:175
- silversight_claim_receipt_invertible: BraidEigensolid.lean:249

Theorem triage (3,057 theorems classified):
- TIER_1_CORE: 118 theorems (6 modules, direct port)
- TIER_2_FOUNDATION: 1,591 theorems (121 modules)
- TIER_3_EXTENSION: 1,084 theorems (291 modules)
- TIER_4_QUARANTINE: 137 theorems (15 modules)
- TIER_5_EXCLUDED: 127 theorems (18 modules)

Build: SilverSight 3307 jobs, 0 errors, 0 sorries
2026-06-22 13:00:29 -05:00

404 lines
14 KiB
Markdown
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

# 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
Reference in a new issue View git blame Copy permalink