SilverSight/docs/ARCHITECTURE.md
SilverSight Agent 3c35fe50c2 Initial SilverSight: deterministic equation search via Fisher geometry
Core components:
- ChentsovFinite.lean (883 lines, 0 sorry): Fisher metric uniqueness on 8-state simplex
- HachimojiCodec.lean: Deterministic E=mc^2 -> Hachimoji state pipeline
- PVGS_DQ_Bridge (8 sections, ~6,150 lines): Photon-Varied Gaussian to Dual Quaternion
- UniversalMathEncoding.lean: 50-token math address space (~10^15 addresses)
- ChiralitySpace.lean: 4D descriptor (phase x chirality x direction x regime) ~2x10^25
- BindingSite (3 files): Amino acid vocabulary, entropy-based bindability
- Python: chaos game, Sidon addressing, Q16.16 canonical, Finsler metric, QUBO/QAOA
- CI: Lean check, Python check, Q16 roundtrip workflows

Papers: Giani-Win-Conti 2025, Chabaud-Mehraban 2022, Pizzimenti 2024, Wassner 2025
2026-06-21 18:02:05 +08:00

4.4 KiB

Architecture

Overview

Research-Stack v2 is organized into 6 layers, each with a single responsibility:

Layer 6: Infrastructure    <- CI/CD, docs, repo hygiene (this stage)
Layer 5: Integrate         <- Language bridges (C, Python, Lean FFI)
Layer 4: Optimize          <- QUBO/QAOA, Finsler annealing
Layer 3: Search            <- Chaos game, basin finding, equation candidates
Layer 2: Codec             <- Hachimoji encoding, Q16_16, Sidon addressing
Layer 1: Core              <- Chentsov theorem, statistical manifolds

Layer Details

Layer 1: Core (CoreFormalism/)

  • ChentsovTheorem.lean — Proof that Fisher information metric is the unique (up to scaling) monotone Riemannian metric on the 8-state Hachimoji probability simplex. 883 lines, 0 sorry.
  • StatisticalManifold.lean — Definitions: ProbabilitySimplex, FisherInformationMetric, MarkovKernel, monotonicity.
  • Q16_16.lean — Canonical fixed-point type with round-half-up semantics. Proven equivalent across Lean, C, and Python.

Status: PROVEN. No axioms beyond standard Lean/mathlib.

Layer 2: Codec (Codec/)

  • hachimoji_codec.py — Deterministic codec: UTF-8 string -> Hachimoji DNA sequence. No ML. No randomness. Pure function.
  • q16_roundtrip.py — Cross-language roundtrip test: Lean <-> C <-> Python.
  • sidon_address.py — Sidon set generation for collision-free memory addressing.

Key invariant: decode(encode(s)) == s for all valid UTF-8 strings s.

  • chaos_game.py — Iterated function system for basin boundary sampling.
  • basin_finder.py — Classifies orbits into basins of attraction.
  • equation_candidates.py — Generates equation candidates from basin representatives.

Status: PROTOTYPE. Chaos game converges; basin classification heuristic.

Layer 4: Optimize (Optimize/)

  • finsler_qubo.py — Finsler-anisotropic QUBO formulation.
  • qaoa_pipeline.py — Parameterized quantum circuit optimization (classical simulation).
  • annealer.py — Simulated annealing with Finsler metric temperature schedule.

Status: IN DEVELOPMENT. QUBO formulation solid; QAOA classical simulation slow.

Layer 5: Integrate (CBridge/, PythonBridge/)

  • CBridge/ — C shared library with Q16_16 operations, compiled to .so.
  • PythonBridge/ — Python ctypes bindings to C library. ctypes.CDLL("./libq16.so").
  • FFI/ — Lean FFI stubs (future work: direct Lean <-> C calls).

Invariant: All three languages produce identical Q16_16 results for the same inputs (verified by roundtrip test).

Layer 6: Infrastructure (.github/, docs, repo hygiene)

  • 4 CI workflows — lean-check, python-check, q16-roundtrip, doc-sync.
  • pre-commit hooks — Same checks as CI, run locally before every commit.
  • .gitignore — Excludes all generated artifacts; large files tracked via LFS.

Data Flow

Input equation string
    |
    v
[Codec] Hachimoji encode -> DNA sequence
    |
    v
[Search] Chaos game -> basin representative
    |
    v
[Optimize] QUBO/QAOA -> optimal parameters
    |
    v
[Core] Chentsov metric -> classification score
    |
    v
Output: classified equation with provenance

Cross-Language Contracts

Q16_16 Fixed-Point

Language File Semantics
Lean CoreFormalism/Q16_16.lean Round-half-up, saturating
C CBridge/libq16.c Round-half-up, saturating
Python PythonBridge/q16_binding.py Round-half-up, saturating

Verification: Tests/q16_roundtrip_test.py checks all triples (x, y) in [-1, 1] x [-1, 1] with step 1/256.

Build Commands

# Lean
lake build

# C
make -f CBridge/Makefile

# Python
pytest Tests/ -v

Repository Layout

/
├── CoreFormalism/       <- Layer 1: Lean proofs
├── Codec/              <- Layer 2: Encoding/decoding
├── Search/             <- Layer 3: Chaos game, basins
├── Optimize/           <- Layer 4: QUBO, QAOA
├── CBridge/            <- Layer 5: C library
├── PythonBridge/       <- Layer 5: Python bindings
├── FFI/                <- Layer 5: Lean FFI (stub)
├── Tests/              <- Cross-layer tests
├── .github/
│   ├── workflows/      <- 4 CI workflows
│   └── scripts/        <- doc-sync check
├── .gitignore
├── .pre-commit-config.yaml
├── README.md
└── ARCHITECTURE.md