Experimental approach to math functions
Find a file
allaun 8ca87c63fb feat: add 8 solved Erdos problems to validation (18/18 deterministic)
New Erdos problems tested:
- Erdos squarefree (Ramaré-Granville 1996) λ=6.70 CognitiveLoadField
- Erdos-Moser (1+2=3) λ=5.38 CognitiveLoadField
- Erdos-Ginzburg-Ziv EGZ theorem λ=3.90 SignalShapedRouteCompiler
- Erdos-Ko-Rado intersecting families λ=5.95 CognitiveLoadField
- Erdos discrepancy (Tao 2015) λ=5.72 CognitiveLoadField
- Erdos primitive set (Lichtman 2022) λ=5.23 CognitiveLoadField
- Erdos-Graham Egyptian fractions (Croot 2000) λ=3.32 SignalShapedRouteCompiler
- Erdos-Heilbronn subset sums λ=6.38 CognitiveLoadField

All 18/18 deterministic, all signal detected (λ >= 1.5)
2026-06-30 06:49:39 -05:00
.github fix: Lean CI — remove redundant SilverSightFormal build (lake build handled by lean-action) 2026-06-30 06:45:03 -05:00
5-Applications/tools-scripts/llm fix: address adversarial review findings 2026-06-23 08:28:30 -05:00
6-Documentation/docs/specs fix: address adversarial review findings 2026-06-23 08:28:30 -05:00
c feat(rrc): port ReceiptDensity, PolyFactorIdentity, EntropyCandidates and add Q16_16 roundtrip test 2026-06-21 10:39:18 -05:00
Core chore: commit all pending work from prior sessions 2026-06-30 04:54:40 -05:00
data feat: README, CI pipeline, Dependabot config 2026-06-30 05:48:50 -05:00
docs chore: commit all pending work from prior sessions 2026-06-30 04:54:40 -05:00
exe refactor(rrc): rename corpus250→allFixtures/emitManifold, generic n-dimensional modules, Authentik deploy 2026-06-30 04:54:40 -05:00
experiments chore: add experiment file, gitignore qc_flag backups 2026-06-30 04:54:40 -05:00
extraction chore: commit all pending work from prior sessions 2026-06-30 04:54:40 -05:00
formal fix: HachimojiN8 theorem bug, all Lean module tests pass 2026-06-30 06:29:34 -05:00
infra/sigs fix: CORE API works without auth key (User-Agent header), 274 signatures 2026-06-30 05:40:44 -05:00
python feat: README, CI pipeline, Dependabot config 2026-06-30 05:48:50 -05:00
qubo chore: commit all pending work from prior sessions 2026-06-30 04:54:40 -05:00
scripts feat: add 8 solved Erdos problems to validation (18/18 deterministic) 2026-06-30 06:49:39 -05:00
signatures feat: add 8 solved Erdos problems to validation (18/18 deterministic) 2026-06-30 06:49:39 -05:00
specs docs: add BraidTree-Octree-COUCH synthesis spec 2026-06-30 04:54:40 -05:00
tests fix: HachimojiN8 theorem bug, all Lean module tests pass 2026-06-30 06:29:34 -05:00
.gitignore chore: add experiment file, gitignore qc_flag backups 2026-06-30 04:54:40 -05:00
AGENTS.md fix: receipt verifier, honest layer status, well-formedness witnesses 2026-06-30 05:52:43 -05:00
BREAKGLASS_LOG.md feat(lean): Sidon-orthogonality bypass closes operator-norm gap 2026-06-26 23:36:55 -05:00
CITATION.cff feat(fisher): Add parabola focal-chord to Fisher-Rao bridge 2026-06-25 18:06:23 -05:00
lake-manifest.json chore: update Mathlib manifest to v4.30.0-rc2 2026-06-23 07:54:26 -05:00
lakefile.lean refactor(rrc): rename corpus250→allFixtures/emitManifold, generic n-dimensional modules, Authentik deploy 2026-06-30 04:54:40 -05:00
lean-toolchain fix: PVGS Mathlib compatibility — update imports + toolchain 2026-06-23 07:53:36 -05:00
PORTING_MAP.md refactor(rrc): rename corpus250→allFixtures/emitManifold, generic n-dimensional modules, Authentik deploy 2026-06-30 04:54:40 -05:00
pytest.ini feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
README.md feat: README, CI pipeline, Dependabot config 2026-06-30 05:48:50 -05:00
REBASE_RULES.md feat(core): harden SilverSightCore and port canonical FixedPoint 2026-06-21 06:30:12 -05:00
requirements.txt chore(deps): bump pytest>=9.1.1, pyyaml>=6.0.3 2026-06-30 06:41:14 -05:00
SORRY_PROTOCOL.md docs(sorry-protocol): S1-S3 marked RESOLVED WEAKENED — Chentsov uniqueness → invariance 2026-06-23 06:00:46 -05:00
SORRY_RESOLUTION_S1S3.md chore(quality): native_decide migration, docs, and phi pipeline cleanup 2026-06-27 01:56:54 -05:00
TRACEABILITY_GRAPH.md chore(quality): native_decide migration, docs, and phi pipeline cleanup 2026-06-27 01:56:54 -05:00
VERIFICATION_LOG.md docs(verification): formulas 010-011 — τ parse tree + G2 collision breaking verified 2026-06-23 05:57:26 -05:00
WORK_LOG.md docs: update WORK_LOG.md with Cold Reviewer Protocol and Cartan formula 2026-06-26 23:56:36 -05:00

SilverSight

A formally verified, hardware-native computation stack for braid topology analysis, eigensolid compression, and cross-domain 1/n-scaling signature mining.

Quick Start

# Verify the entire pipeline (4 min)
bash scripts/run_entry_gate.sh

This runs all 4 anti-smuggle layers:

Layer Gate What it proves
0 check_determinism.py All artifacts are reproducible (SHA-256 chains, seeded RNG)
1 lake build All 3307 Lean jobs compile (Q16_16 fixed-point, AVM ISA, PIST classifiers)
2 rrc-emit-fixture The manifold receipt emits with 278/278 rows passing alignment
3 verify_with_sympy.py All Q16_16 computations cross-checked against SymPy symbolic math

What It Does

Core idea: Every byte is signal. Gaps, timing, and absences are the encoding. The compressor encodes everything; the decompressor must reconstruct everything, including the gaps — because the gaps are the compression.

Pipeline

Equation text → tokenizer → 8×8 strand adjacency matrix
                                       ↓
                              PIST spectral classifier
                              (MatrixN → SpectralN → ClassifyN)
                                       ↓
                              Q16_16Manifold (278 fixture rows)
                                       ↓
                              AVM ISA receipt (JSON)

Key Modules

Module Purpose
MatrixN Generic n×n matrix operations (power iteration, Laplacian, A^T A)
SpectralN Spectral profile: eigenvalue, spectral gap, density, Frobenius norm
ClassifyN Spectral-radius → color → shape-name classifier
BraidStateN n-strand braid state, crossStep, eigensolid convergence
FisherRigidityN n-dimensional Fisher-Rao geometric rigidity
FixedPointBridge Q16_16 ↔ Q0_64 quad matrix bridge (zero LSB error)
FeasibleSet QUBO k-hot relaxation with weak monotonicity proofs

Infrastructure

Service Host Purpose
AppFloyo Cloud neon-64gb:8000 Module dependency dashboard
GoTrue neon-64gb:9999 JWT auth for API access
Authentik neon-64gb:30001 SSO provider (OAuth2/OIDC)
Homarr neon-64gb:7575 Infrastructure dashboard
CouchDB neon-64gb:5984 Document store

Verification

# Full formal build
lake build                          # 3307 jobs, 0 errors

# Generate predictions from equations
python3 python/generate_predictions.py

# Build matrix data
python3 python/build_pist_matrices_250.py

# Build manifold fixture rows
python3 python/build_manifold.py

# Emit signed receipt
lake exe rrc-emit-fixture

# Cross-domain significance mining (arXiv + CORE API)
CORE_API_KEY="<key>" python3 infra/sigs/rydberg_miner.py
python3 scripts/cross_domain_significance.py

Project Structure

formal/          Lean 4 source (truth)
python/          Python I/O shims
scripts/         Anti-smuggle protocol, infrastructure
signatures/      Cross-domain signature data
infra/sigs/      Literature mining tools
specs/           Design documents

License

Apache 2.0