mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00

allaun fa8f6a2586 chore: commit utility scripts, MCP backend source, and archived data

Utility scripts:
- download_leanstral.py: HuggingFace model download for autoproof
- download_leanstral_urllib.py: stdlib-only variant
- prime_slos_explore.py: spectral signature exploration for primes

Infrastructure:
- scripts/mcp_backend/: Rust MCP backend (src + Cargo.toml/lock, target/ gitignored)

Data:
- .openresearch/artifacts/slos_checkpoints/: 128K checkpoint data
- archive/dead_code_2026-07-03/: 360K archived dead code

2026-07-04 02:06:51 -05:00

1.6 KiB

Raw Permalink Blame History

Dead Code Archive — 2026-07-03

Files removed from the active build. All contain sorries, native_decide calls, or are otherwise incomplete. Archived for reference; not compiled by lake build.

Removed Modules

File	Lines	Reason
`CoreFormalism/CharacterTransform.lean`	—	Not in lakefile; unverified character table
`PVGS_DQ_Bridge/` (8 .lean + 1 .py)	~3000	Commented out in lakefile; 979-case enumeration sorries
`UniversalEncoding/` (2 .lean)	~600	Not in lakefile; chirality space stubs
`SilverSight/PIST/SpectralWitness.lean`	—	Not in lakefile; witness-only, no theorems
`SilverSight/Bind.lean`	—	Not in lakefile; quaternion bindings with sorries
`SilverSight/FeasibleSet/TestChain.lean`	—	Not in lakefile; test-only, no formal content

PVGS_DQ_Bridge Details

The PVGS (Pólya-Vinogradov / Goormaghtigh / Sidon) bridge contained significant formalization effort (7 sections + master receipt) but was blocked on:

BMS region enumeration (979 cases, T4.1)
Hermite sieve verification (T4.2)
Quantum sensing distinguishability bound

All 18 axioms in this directory carried HONESTY CLASS tags. The math is correct but the finite enumeration was never completed.

UniversalEncoding Details

ChiralitySpace and UniversalMathEncoding stubs for a proposed "universal math receipt" encoding LaTeX expressions into 16D space. Never integrated into the active build.

Recovery

To restore any file: cp archive/dead_code_2026-07-03/<path> formal/<path> Then add the corresponding entry to lakefile.lean.

1.6 KiB Raw Permalink Blame History