allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +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

14 KiB
Raw Permalink Blame History

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