mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
3504bca392
Implements the YaFF-inspired separation of schema, layout, and access pattern
in Core/SilverSight/Semantics/:
- Schema.lean: fixed-size Schema typeclass with byteSize and wellFormed.
- Layout.lean: Layout enum, AccessProfile cost model, and cost-based selector
with an ε-suboptimality theorem.
- WireFormat.lean: certified encode/decode/roundTrip/encode_size structure.
- View.lean: zero-copy View with address-arithmetic invariant.
- LayoutBridge.lean: certified layout-conversion structure and identity bridges.
- CanalLayout.lean: CanalRegime enum and regime-aware layout selection.
Also updates:
- lakefile.lean: adds SilverSight.Semantics.* roots to SilverSightCore.
- docs/ARCHITECTURE.md, RRC_REFACTOR_READINESS.md, PROJECT_MAP.{md,json},
build_logs/2026-06-21_session_build_baseline.md, and GLOSSARY.md.
- AGENTS.md: build baseline, blessed surfaces, and pending proof work.
Build: 2987 jobs, 0 errors (lake build)
Tests: Python 21/21, Lean/C 35/35
17 KiB
17 KiB
SilverSight Project Map
Generated: 2026-06-21T18:58:40.565557+00:00
Source repo: https://github.com/allaunthefox/SilverSight
Tooling: python3 docs/generate_project_map.py regenerates this file and docs/PROJECT_MAP.json.
1. Project Overview
- Total tracked files: 116
- Lean files: 62
- Python files: 23
- Active: 115 | Quarantined: 1 | Archived: 0
- Receipt-boundary files: 4
2. Layer Summary
| Layer | Path | Files | Lean | Python | Active | Quarantined | Archived | Description |
|---|---|---|---|---|---|---|---|---|
| Core | Core |
8 | 8 | 0 | 8 | 0 | 0 | Invariant core: no imports except Mathlib; defines Receipt and AVM. |
| CoreFormalism | formal/CoreFormalism |
18 | 18 | 0 | 18 | 0 | 0 | Canonical Q16_16, Sidon, braid, and Hachimoji foundations. |
| PVGS_DQ_Bridge | formal/PVGS_DQ_Bridge |
9 | 8 | 1 | 9 | 0 | 0 | Photon-varied Gaussian state dual-quaternion bridge. |
| UniversalEncoding | formal/UniversalEncoding |
2 | 2 | 0 | 2 | 0 | 0 | Universal math address space and chirality. |
| BindingSite | formal/BindingSite |
3 | 3 | 0 | 3 | 0 | 0 | Amino-acid / protein binding sketches. |
| PythonShims | python |
9 | 0 | 9 | 9 | 0 | 0 | I/O and feature extraction; no admissibility logic. |
| QUBOShims | qubo |
5 | 0 | 5 | 5 | 0 | 0 | QUBO/QAOA/Finsler optimization shims. |
| Tests | tests |
3 | 0 | 3 | 2 | 1 | 0 | Verification fixtures. |
| Infrastructure | .github |
6 | 0 | 2 | 6 | 0 | 0 | CI workflows and repo scripts. |
| Docs | docs |
19 | 0 | 3 | 19 | 0 | 0 | Architecture, contracts, and generated maps. |
3. File Inventory
Core (Core)
| File | Module | Build Target | Status | Receipt Boundary | Research-Stack Source | Role |
|---|---|---|---|---|---|---|
Core/SilverSight/FixedPoint.lean |
SilverSight.FixedPoint | SilverSight.FixedPoint | active | — | — | — |
Core/SilverSight/Semantics/CanalLayout.lean |
SilverSight.Semantics.CanalLayout | SilverSightFormal | active | — | — | — |
Core/SilverSight/Semantics/Layout.lean |
SilverSight.Semantics.Layout | SilverSight.Semantics.Layout | active | — | — | — |
Core/SilverSight/Semantics/LayoutBridge.lean |
SilverSight.Semantics.LayoutBridge | SilverSight.Semantics.LayoutBridge | active | — | — | — |
Core/SilverSight/Semantics/Schema.lean |
SilverSight.Semantics.Schema | SilverSight.Semantics.Schema | active | — | — | — |
Core/SilverSight/Semantics/View.lean |
SilverSight.Semantics.View | SilverSight.Semantics.View | active | — | — | — |
Core/SilverSight/Semantics/WireFormat.lean |
SilverSight.Semantics.WireFormat | SilverSight.Semantics.WireFormat | active | — | — | — |
Core/SilverSightCore.lean |
SilverSightCore | SilverSightCore | active | ✅ | — | Invariant core: Hachimoji states, Receipt, AVM δ, TIC axiom, library interface. |
CoreFormalism (formal/CoreFormalism)
| File | Module | Build Target | Status | Receipt Boundary | Research-Stack Source | Role |
|---|---|---|---|---|---|---|
formal/CoreFormalism/Bind.lean |
CoreFormalism.Bind | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/Bind.lean |
Bind/connective primitives used by braid modules. |
formal/CoreFormalism/BraidBracket.lean |
CoreFormalism.BraidBracket | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/BraidBracket.lean |
Braid bracket algebra. |
formal/CoreFormalism/BraidCross.lean |
CoreFormalism.BraidCross | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/BraidCross.lean |
Braid crossing representation and residuals. |
formal/CoreFormalism/BraidEigensolid.lean |
CoreFormalism.BraidEigensolid | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/BraidEigensolid.lean |
Eigensolid fixed-point theory for BraidStorm topology. |
formal/CoreFormalism/BraidField.lean |
CoreFormalism.BraidField | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/BraidField.lean |
Field operations on braid states. |
formal/CoreFormalism/BraidSpherionBridge.lean |
CoreFormalism.BraidSpherionBridge | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/BraidSpherionBridge.lean |
Braid-to-spherion bridge and topological mixing. |
formal/CoreFormalism/BraidStrand.lean |
CoreFormalism.BraidStrand | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/BraidStrand.lean |
8-strand braid model. |
formal/CoreFormalism/ChentsovFinite.lean |
CoreFormalism.ChentsovFinite | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/ChentsovBridge.lean |
Finite Chentsov theorem for the 8-state Hachimoji simplex. |
formal/CoreFormalism/DynamicCanal.lean |
CoreFormalism.DynamicCanal | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/DynamicCanal.lean |
Dynamic canal primitives for braid/spherion flow. |
formal/CoreFormalism/FixedPoint.lean |
CoreFormalism.FixedPoint | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean |
Canonical Q16_16 fixed-point type; source of truth for cross-language determinism. |
formal/CoreFormalism/HachimojiBase.lean |
CoreFormalism.HachimojiBase | SilverSightFormal | active | — | — | Base definitions for the 8-state Hachimoji alphabet. |
formal/CoreFormalism/HachimojiCodec.lean |
CoreFormalism.HachimojiCodec | SilverSightFormal | active | — | — | Hachimoji encode/decode for UTF-8 strings. |
formal/CoreFormalism/HachimojiManifoldAxiom.lean |
CoreFormalism.HachimojiManifoldAxiom | SilverSightFormal | active | — | — | Axioms tying Hachimoji states to statistical manifold structure. |
formal/CoreFormalism/InteractionGraphSidon.lean |
CoreFormalism.InteractionGraphSidon | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/InteractionGraphSidon.lean |
Typed interaction graphs, bounded Sidon witness, weak-axis CRT reconstruction. |
formal/CoreFormalism/Q16_16Numerics.lean |
CoreFormalism.Q16_16Numerics | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/Q16_16Numerics.lean |
Numeric helpers and bounds over canonical Q16_16. |
formal/CoreFormalism/SidonSets.lean |
CoreFormalism.SidonSets | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/SidonSets.lean |
Sidon-set definitions, extremal function, Johnson/Lindström bounds, Singer theorem. |
formal/CoreFormalism/SieveLemmas.lean |
CoreFormalism.SieveLemmas | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/SieveLemmas.lean |
Coprime-sieve observers and CRT reconstruction. |
formal/CoreFormalism/Tactics.lean |
CoreFormalism.Tactics | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/Tactics.lean |
Shared tactic macros used across CoreFormalism modules. |
PVGS_DQ_Bridge (formal/PVGS_DQ_Bridge)
| File | Module | Build Target | Status | Receipt Boundary | Research-Stack Source | Role |
|---|---|---|---|---|---|---|
formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean |
PVGS_DQ_Bridge.PVGS_DQ_Bridge_fixed | SilverSightFormal | active | ✅ | 0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean |
Master PVGS dual-quaternion bridge receipt. |
formal/PVGS_DQ_Bridge/pvgs_receipt_hash.py |
— | — | active | ✅ | 4-Infrastructure/shim/pvgs_receipt_hash.py |
Python helper to hash PVGS receipts. |
formal/PVGS_DQ_Bridge/section1_pvgs_params.lean |
PVGS_DQ_Bridge.section1_pvgs_params | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean |
Photon-varied Gaussian state parameters. |
formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean |
PVGS_DQ_Bridge.section2_hermite_sieve | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean |
Hermite-sieve construction for PVGS. |
formal/PVGS_DQ_Bridge/section3_variety_isomorphism.lean |
PVGS_DQ_Bridge.section3_variety_isomorphism | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean |
Variety isomorphism linking PVGS states. |
formal/PVGS_DQ_Bridge/section4_rrc_kernel.lean |
PVGS_DQ_Bridge.section4_rrc_kernel | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean |
RRC kernel embedded in PVGS bridge. |
formal/PVGS_DQ_Bridge/section5_quantum_sensing.lean |
PVGS_DQ_Bridge.section5_quantum_sensing | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean |
Quantum-sensing bounds within PVGS. |
formal/PVGS_DQ_Bridge/section6_effective_bounds.lean |
PVGS_DQ_Bridge.section6_effective_bounds | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean |
Effective bounds for dual-quaternion operations. |
formal/PVGS_DQ_Bridge/section7_master_receipt.lean |
PVGS_DQ_Bridge.section7_master_receipt | SilverSightFormal | active | ✅ | 0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean |
Top-level PVGS receipt assembly. |
UniversalEncoding (formal/UniversalEncoding)
| File | Module | Build Target | Status | Receipt Boundary | Research-Stack Source | Role |
|---|---|---|---|---|---|---|
formal/UniversalEncoding/ChiralitySpace.lean |
UniversalEncoding.ChiralitySpace | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/ChiralitySpace.lean |
Chirality classification space. |
formal/UniversalEncoding/UniversalMathEncoding.lean |
UniversalEncoding.UniversalMathEncoding | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/UniversalMathEncoding.lean |
50-token universal math address space. |
BindingSite (formal/BindingSite)
| File | Module | Build Target | Status | Receipt Boundary | Research-Stack Source | Role |
|---|---|---|---|---|---|---|
formal/BindingSite/BindingSiteCodec.lean |
BindingSite.BindingSiteCodec | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/BindingSite/BindingSiteCodec.lean |
Binding-site codec for amino-acid/protein sketches. |
formal/BindingSite/BindingSiteEntropy.lean |
BindingSite.BindingSiteEntropy | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/BindingSite/BindingSiteEntropy.lean |
Entropy calculations for binding sites. |
formal/BindingSite/BindingSiteHachimoji.lean |
BindingSite.BindingSiteHachimoji | SilverSightFormal | active | — | 0-Core-Formalism/lean/Semantics/Semantics/BindingSite/BindingSiteHachimoji.lean |
Binding-site classification into Hachimoji states. |
PythonShims (python)
| File | Module | Build Target | Status | Receipt Boundary | Research-Stack Source | Role |
|---|---|---|---|---|---|---|
python/build_corpus250.py |
— | — | active | — | — | — |
python/build_pist_matrices_250.py |
— | — | active | — | — | — |
python/chaos_game.py |
— | — | active | — | 4-Infrastructure/shim/chaos_game_16d.py |
16D chaos-game basin sampler. |
python/pist_matrix_builder.py |
— | — | active | — | — | — |
python/q16_canonical.py |
— | — | active | — | — | Canonical Q16_16 Python reference implementation. |
python/sidon_address.py |
— | — | active | — | 4-Infrastructure/shim/sidon_generation_kernel.py |
Sidon label generation for collision-free addressing. |
python/spectral_profile.py |
— | — | active | — | 4-Infrastructure/shim/geometric_entropy_explorer.py |
Spectral/entropy profile exploration. |
python/test_search.py |
— | — | active | — | — | Search-layer sanity tests. |
python/validate_rrc_predictions.py |
— | — | active | — | — | — |
QUBOShims (qubo)
| File | Module | Build Target | Status | Receipt Boundary | Research-Stack Source | Role |
|---|---|---|---|---|---|---|
qubo/classical_solver.py |
— | — | active | — | 4-Infrastructure/shim/qubo_highs.py |
HiGHS MIP bridge + TSP assignment relaxation. |
qubo/finsler_metric.py |
— | — | active | — | 4-Infrastructure/shim/qaoa_adapter.py |
Finsler-Randers metric and QUBO formulation. |
qubo/qaoa_circuit.py |
— | — | active | — | 4-Infrastructure/shim/qaoa_adapter.py |
QAOA circuit generation and classical simulation. |
qubo/qubo_builder.py |
— | — | active | — | 4-Infrastructure/shim/qaoa_adapter.py |
QUBO/Ising/Pauli problem builder. |
qubo/test_optimize.py |
— | — | active | — | — | Optimization-layer unit tests. |
Tests (tests)
| File | Module | Build Target | Status | Receipt Boundary | Research-Stack Source | Role |
|---|---|---|---|---|---|---|
tests/quarantine/q16_roundtrip_test.legacy.py |
— | — | quarantined | — | tests/q16_roundtrip_test.py |
Archived C <-> Python roundtrip test; waiting on C bridge. |
tests/test_q16_canonical.py |
— | — | active | — | — | Canonical Q16_16 unit tests. |
tests/test_q16_roundtrip.py |
— | — | active | — | — | — |
Infrastructure (.github)
| File | Module | Build Target | Status | Receipt Boundary | Research-Stack Source | Role |
|---|---|---|---|---|---|---|
.github/scripts/check_doc_sync.py |
— | — | active | — | — | — |
.github/scripts/glossary_lint.py |
— | — | active | — | — | — |
.github/workflows/doc-sync.yml |
— | — | active | — | — | — |
.github/workflows/lean-check.yml |
— | — | active | — | — | — |
.github/workflows/python-check.yml |
— | — | active | — | — | — |
.github/workflows/q16-roundtrip.yml |
— | — | active | — | — | — |
Docs (docs)
| File | Module | Build Target | Status | Receipt Boundary | Research-Stack Source | Role |
|---|---|---|---|---|---|---|
docs/ARCHITECTURE.md |
— | — | active | — | — | — |
docs/GLOSSARY.md |
— | — | active | — | — | — |
docs/GLOSSARY_ALLOWLIST.md |
— | — | active | — | — | — |
docs/LIBRARY_MANIFEST.md |
— | — | active | — | — | — |
docs/PROJECT_MAP.json |
— | — | active | — | — | — |
docs/PROJECT_MAP.md |
— | — | active | — | — | — |
docs/RRC_PLACEMENT.md |
— | — | active | — | — | — |
docs/RRC_REFACTOR_READINESS.md |
— | — | active | — | — | — |
docs/TESTING.md |
— | — | active | — | — | — |
docs/build_logs/2026-06-21_session_build_baseline.md |
— | — | active | — | — | — |
docs/generate_porting_candidates.py |
— | — | active | — | — | — |
docs/generate_project_map.py |
— | — | active | — | — | — |
docs/generate_research_stack_usage_map.py |
— | — | active | — | — | — |
docs/research_stack_porting_candidates.md |
— | — | active | — | — | — |
docs/research_stack_usage_graph.dot |
— | — | active | — | — | — |
docs/research_stack_usage_graph.json |
— | — | active | — | — | — |
docs/research_stack_usage_graph.md |
— | — | active | — | — | — |
docs/research_stack_usage_graph.svg |
— | — | active | — | — | — |
docs/research_stack_usage_graph_thumb.png |
— | — | active | — | — | — |
4. Key Build & Test Commands
# Lean
lake build
lake build SilverSightFormal
lake build CoreFormalism.SidonSets
# Python
python3 -m py_compile python/*.py qubo/*.py tests/*.py .github/scripts/*.py
pytest tests/ python/ qubo/ -v
# Docs
python3 .github/scripts/glossary_lint.py
python3 docs/generate_project_map.py
5. Dependency Rules
Core/SilverSightCore.leanimports nothing except Mathlib.- Every library may import
Core/and Mathlib, but no library may import another library. formal/CoreFormalism/is the canonical foundation; higherformal/directories may importCoreFormalism/but not each other.python/andqubo/are I/O shims; they may not contain admissibility logic.- The
Receiptis the only Core/library boundary.
6. Legend
| Field | Meaning |
|---|---|
active |
Builds and is part of the current surface. |
quarantined |
In tests/quarantine/ or marked broken; not part of CI. |
archived |
Legacy filename; kept for reference only. |
Receipt Boundary |
File produces or consumes Receipt values across the Core/library boundary. |