mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
feat(pist): port minimal PIST classifier surface to SilverSight
- Add SilverSight.PIST.Spectral with isqrt, powerIteration, SpectralProfile, and computeSpectral (pure Int + Q16_16; no Float, no photonic extras). - Add SilverSight.PIST.Classify with Matrix8, hashMatrix, classifyProxy, classifyExact, spectral-radius color gate, and blend rules. - Add SilverSight.PIST.Matrices250 auto-generated from Research Stack rrc_pist_predictions_250_v1.json (250 entries). - Add python/build_pist_matrices_250.py generator with deterministic ordering and content-hash comment. - Register PIST modules under SilverSightRRC in lakefile.lean. - Regenerate PROJECT_MAP.md/json. Build: 2981 jobs, 0 errors (lake build); SilverSightRRC: 2994 jobs, 0 errors.
This commit is contained in:
parent
e92d4d73d9
commit
569c16088a
7 changed files with 3191 additions and 16 deletions
|
|
@ -1,13 +1,13 @@
|
|||
{
|
||||
"schema": "silversight_project_map_v1",
|
||||
"generated_at": "2026-06-21T14:16:47.617133+00:00",
|
||||
"generated_at": "2026-06-21T14:45:59.149164+00:00",
|
||||
"repo": "https://github.com/allaunthefox/SilverSight",
|
||||
"local_path": "/tmp/SilverSight",
|
||||
"summary": {
|
||||
"total_files": 97,
|
||||
"lean_files": 48,
|
||||
"python_files": 20,
|
||||
"active": 96,
|
||||
"total_files": 101,
|
||||
"lean_files": 51,
|
||||
"python_files": 21,
|
||||
"active": 100,
|
||||
"quarantined": 1,
|
||||
"archived": 0,
|
||||
"receipt_boundary_files": 4
|
||||
|
|
@ -78,10 +78,10 @@
|
|||
"name": "PythonShims",
|
||||
"path": "python",
|
||||
"description": "I/O and feature extraction; no admissibility logic.",
|
||||
"file_count": 7,
|
||||
"file_count": 8,
|
||||
"lean_files": 0,
|
||||
"python_files": 7,
|
||||
"active": 7,
|
||||
"python_files": 8,
|
||||
"active": 8,
|
||||
"quarantined": 0,
|
||||
"archived": 0
|
||||
},
|
||||
|
|
@ -375,7 +375,7 @@
|
|||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 74
|
||||
"line_count": 89
|
||||
},
|
||||
{
|
||||
"path": "docs/LIBRARY_MANIFEST.md",
|
||||
|
|
@ -1386,6 +1386,53 @@
|
|||
"receipt_boundary": false,
|
||||
"line_count": 34
|
||||
},
|
||||
{
|
||||
"path": "formal/SilverSight/PIST/Classify.lean",
|
||||
"layer": "other",
|
||||
"language": "lean",
|
||||
"kind": "formal",
|
||||
"module": "SilverSight.PIST.Classify",
|
||||
"build_target": "SilverSightFormal",
|
||||
"status": "active",
|
||||
"imports": [
|
||||
"SilverSight.PIST.Spectral",
|
||||
"SilverSight.FixedPoint"
|
||||
],
|
||||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 229
|
||||
},
|
||||
{
|
||||
"path": "formal/SilverSight/PIST/Matrices250.lean",
|
||||
"layer": "other",
|
||||
"language": "lean",
|
||||
"kind": "formal",
|
||||
"module": "SilverSight.PIST.Matrices250",
|
||||
"build_target": "SilverSightFormal",
|
||||
"status": "active",
|
||||
"imports": [],
|
||||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 2526
|
||||
},
|
||||
{
|
||||
"path": "formal/SilverSight/PIST/Spectral.lean",
|
||||
"layer": "other",
|
||||
"language": "lean",
|
||||
"kind": "formal",
|
||||
"module": "SilverSight.PIST.Spectral",
|
||||
"build_target": "SilverSightFormal",
|
||||
"status": "active",
|
||||
"imports": [
|
||||
"SilverSight.FixedPoint"
|
||||
],
|
||||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 213
|
||||
},
|
||||
{
|
||||
"path": "formal/SilverSight/RRC/Emit.lean",
|
||||
"layer": "other",
|
||||
|
|
@ -1497,7 +1544,7 @@
|
|||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 56
|
||||
"line_count": 59
|
||||
},
|
||||
{
|
||||
"path": "lean-toolchain",
|
||||
|
|
@ -1527,6 +1574,24 @@
|
|||
"receipt_boundary": false,
|
||||
"line_count": 6
|
||||
},
|
||||
{
|
||||
"path": "python/build_pist_matrices_250.py",
|
||||
"layer": "python_shim",
|
||||
"language": "python",
|
||||
"kind": "python_shim",
|
||||
"module": null,
|
||||
"build_target": null,
|
||||
"status": "active",
|
||||
"imports": [
|
||||
"__future__",
|
||||
"argparse",
|
||||
"pathlib"
|
||||
],
|
||||
"research_stack_source": null,
|
||||
"role": "",
|
||||
"receipt_boundary": false,
|
||||
"line_count": 123
|
||||
},
|
||||
{
|
||||
"path": "python/chaos_game.py",
|
||||
"layer": "python_shim",
|
||||
|
|
@ -2046,6 +2111,21 @@
|
|||
"to": "Core/SilverSight/FixedPoint.lean",
|
||||
"relation": "imports"
|
||||
},
|
||||
{
|
||||
"from": "formal/SilverSight/PIST/Classify.lean",
|
||||
"to": "formal/SilverSight/PIST/Spectral.lean",
|
||||
"relation": "imports"
|
||||
},
|
||||
{
|
||||
"from": "formal/SilverSight/PIST/Classify.lean",
|
||||
"to": "Core/SilverSight/FixedPoint.lean",
|
||||
"relation": "imports"
|
||||
},
|
||||
{
|
||||
"from": "formal/SilverSight/PIST/Spectral.lean",
|
||||
"to": "Core/SilverSight/FixedPoint.lean",
|
||||
"relation": "imports"
|
||||
},
|
||||
{
|
||||
"from": "formal/SilverSight/RRC/Emit.lean",
|
||||
"to": "formal/SilverSight/RRCLogogramProjection.lean",
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
# SilverSight Project Map
|
||||
|
||||
**Generated:** 2026-06-21T14:16:47.617133+00:00
|
||||
**Generated:** 2026-06-21T14:45:59.149164+00:00
|
||||
|
||||
**Source repo:** https://github.com/allaunthefox/SilverSight
|
||||
|
||||
|
|
@ -8,10 +8,10 @@
|
|||
|
||||
## 1. Project Overview
|
||||
|
||||
- **Total tracked files:** 97
|
||||
- **Lean files:** 48
|
||||
- **Python files:** 20
|
||||
- **Active:** 96 | **Quarantined:** 1 | **Archived:** 0
|
||||
- **Total tracked files:** 101
|
||||
- **Lean files:** 51
|
||||
- **Python files:** 21
|
||||
- **Active:** 100 | **Quarantined:** 1 | **Archived:** 0
|
||||
- **Receipt-boundary files:** 4
|
||||
|
||||
## 2. Layer Summary
|
||||
|
|
@ -23,7 +23,7 @@
|
|||
| 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` | 7 | 0 | 7 | 7 | 0 | 0 | I/O and feature extraction; no admissibility logic. |
|
||||
| PythonShims | `python` | 8 | 0 | 8 | 8 | 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` | 2 | 0 | 2 | 1 | 1 | 0 | Verification fixtures. |
|
||||
| Infrastructure | `.github` | 6 | 0 | 2 | 6 | 0 | 0 | CI workflows and repo scripts. |
|
||||
|
|
@ -94,6 +94,7 @@
|
|||
|
||||
| File | Module | Build Target | Status | Receipt Boundary | Research-Stack Source | Role |
|
||||
|------|--------|--------------|--------|------------------|----------------------|------|
|
||||
| `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. |
|
||||
|
|
|
|||
229
formal/SilverSight/PIST/Classify.lean
Normal file
229
formal/SilverSight/PIST/Classify.lean
Normal file
|
|
@ -0,0 +1,229 @@
|
|||
-- SilverSight.PIST.Classify — minimal RRC shape classifier over 8×8 matrices
|
||||
--
|
||||
-- Ports only the classifier surface needed for Corpus250:
|
||||
-- • 8×8 braid adjacency matrix type
|
||||
-- • spectral-radius → RGB color → shape-name gate
|
||||
-- • matrix-hash lookup table (proxy classifier)
|
||||
-- • spectral-radius exact classifier
|
||||
-- • deterministic blending rules for shared equation_ids
|
||||
--
|
||||
-- Photonic/Kubelka-Munk/Quandela extensions from Research Stack are omitted.
|
||||
|
||||
import SilverSight.PIST.Spectral
|
||||
import SilverSight.FixedPoint
|
||||
|
||||
namespace SilverSight.PIST.Classify
|
||||
|
||||
open SilverSight.FixedPoint
|
||||
open SilverSight.FixedPoint.Q16_16
|
||||
open SilverSight.PIST.Spectral
|
||||
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
-- §1 Matrix type
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
abbrev Matrix8 : Type := Array (Array Int)
|
||||
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
-- §2 Spectral-radius thresholds
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
/-- High amplification threshold: λ ≥ 4.0 (Q16.16 raw). -/
|
||||
def oberthHighThreshold : Int := 262144
|
||||
|
||||
/-- Moderate amplification threshold: λ ≥ 2.0 (Q16.16 raw). -/
|
||||
def signalThreshold : Int := 131072
|
||||
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
-- §3 Spectral color gate
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
structure SpectralColor where
|
||||
red : Q16_16
|
||||
green : Q16_16
|
||||
blue : Q16_16
|
||||
deriving Repr
|
||||
|
||||
/-- Convert a raw spectral radius (Int) to an RGB SpectralColor. -/
|
||||
def spectralRadiusToColor (lam : Int) : SpectralColor :=
|
||||
let max_raw := oberthHighThreshold
|
||||
let r := if lam ≥ max_raw then one else zero
|
||||
let g := if lam ≥ signalThreshold then
|
||||
ofRawInt ((lam - signalThreshold) * 65536 / (max_raw - signalThreshold))
|
||||
else zero
|
||||
let b := if lam < signalThreshold then
|
||||
ofRawInt (lam * 65536 / signalThreshold)
|
||||
else zero
|
||||
{ red := r, green := g, blue := b }
|
||||
|
||||
/-- Extract the shape-name string from a SpectralColor. -/
|
||||
def colorToShapeName (c : SpectralColor) : Option String :=
|
||||
if c.red.toInt > 0 then some "CognitiveLoadField"
|
||||
else if c.green.toInt > 0 then some "SignalShapedRouteCompiler"
|
||||
else none
|
||||
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
-- §4 Blending rules for shared equation_ids
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
inductive BlendType where
|
||||
| additive
|
||||
| rms
|
||||
| vortex
|
||||
deriving Repr
|
||||
|
||||
def blend_additive (lam1 lam2 : Int) : Int :=
|
||||
max lam1 lam2
|
||||
|
||||
def blend_rms (lam1 lam2 : Int) : Int :=
|
||||
Int.ofNat (Nat.sqrt (((lam1 * lam1 + lam2 * lam2) / 2).toNat))
|
||||
|
||||
def blend_vortex (lam1 lam2 : Int) : Int :=
|
||||
(lam1 * lam2) / (lam1 + lam2 + 1)
|
||||
|
||||
/-- Blend a list of spectral radii under a given topology. -/
|
||||
def blendRadii (blendType : BlendType) (lams : List Int) : Int :=
|
||||
match lams with
|
||||
| [] => 0
|
||||
| lam :: rest =>
|
||||
rest.foldl (fun acc lam2 =>
|
||||
match blendType with
|
||||
| .additive => if acc ≥ lam2 then acc else lam2
|
||||
| .rms => isqrt ((acc * acc + lam2 * lam2) / 2)
|
||||
| .vortex => (acc * lam2) / (acc + lam2 + 1)
|
||||
) lam
|
||||
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
-- §5 Classifier surface
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
def hashMatrix (m : Matrix8) : Int :=
|
||||
let rec loop (i j : Nat) (pow_5 : Int) (acc : Int) : Int :=
|
||||
if i ≥ 8 then acc
|
||||
else if j ≥ 8 then loop (i + 1) 0 pow_5 acc
|
||||
else
|
||||
let val := m.getD i #[] |>.getD j 0
|
||||
loop i (j + 1) (pow_5 * 5) (acc + val * pow_5)
|
||||
loop 0 0 1 0
|
||||
|
||||
/-- Advisory shape proxy via matrix-hash lookup. -/
|
||||
def classifyProxy (m : Matrix8) : Option String :=
|
||||
match hashMatrix m with
|
||||
| 0 => some "CognitiveLoadField"
|
||||
| 25 => some "CognitiveLoadField"
|
||||
| 125 => some "CognitiveLoadField"
|
||||
| 625 => some "CognitiveLoadField"
|
||||
| 78125 => some "SignalShapedRouteCompiler"
|
||||
| 390625 => some "CognitiveLoadField"
|
||||
| 1953125 => some "SignalShapedRouteCompiler"
|
||||
| 9765625 => some "ProjectableGeometryTopology"
|
||||
| 48828125 => some "ProjectableGeometryTopology"
|
||||
| 244140625 => some "SignalShapedRouteCompiler"
|
||||
| 30517578125 => some "ProjectableGeometryTopology"
|
||||
| 152587890625 => some "ProjectableGeometryTopology"
|
||||
| 152587968750 => some "ProjectableGeometryTopology"
|
||||
| 3814697265625 => some "SignalShapedRouteCompiler"
|
||||
| 19073496093750 => some "CognitiveLoadField"
|
||||
| 476837158203150 => some "CadForceProbeReceipt"
|
||||
| 2384185791015625 => some "ProjectableGeometryTopology"
|
||||
| 11920928955078125 => some "ProjectableGeometryTopology"
|
||||
| 59604644775390626 => some "ProjectableGeometryTopology"
|
||||
| 59604644824218750 => some "CognitiveLoadField"
|
||||
| 298023223876953125 => some "ProjectableGeometryTopology"
|
||||
| 1490116119384765625 => some "ProjectableGeometryTopology"
|
||||
| 1490211486816406250 => some "ProjectableGeometryTopology"
|
||||
| 1502037048339843750 => some "CognitiveLoadField"
|
||||
| 7450580596923828125 => some "ProjectableGeometryTopology"
|
||||
| 7510185241699218875 => some "ProjectableGeometryTopology"
|
||||
| 37252902984619140625 => some "HoldForUnlawfulOrUnderspecifiedShape"
|
||||
| 186264514923095703125 => some "ProjectableGeometryTopology"
|
||||
| 931322574615478515625 => some "ProjectableGeometryTopology"
|
||||
| 4656612873077392578125 => some "CognitiveLoadField"
|
||||
| 4656612873077441406250 => some "CognitiveLoadField"
|
||||
| 23283064365386962890625 => some "ProjectableGeometryTopology"
|
||||
| 23283064365386962890626 => some "ProjectableGeometryTopology"
|
||||
| 23283064365386962890630 => some "CognitiveLoadField"
|
||||
| 23283064365386962890750 => some "SignalShapedRouteCompiler"
|
||||
| 23320317268371582031250 => some "SignalShapedRouteCompiler"
|
||||
| 116415321826934814453125 => some "SignalShapedRouteCompiler"
|
||||
| 116415321826965576171875 => some "SignalShapedRouteCompiler"
|
||||
| 582076609135443115234375 => some "CognitiveLoadField"
|
||||
| 582076621055603027343750 => some "CognitiveLoadField"
|
||||
| 2910383343696594482421875 => some "CognitiveLoadField"
|
||||
| 2910420298576354980468750 => some "CognitiveLoadField"
|
||||
| 14575198292732238769531250 => some "SignalShapedRouteCompiler"
|
||||
| 17462298274040222167968750 => some "SignalShapedRouteCompiler"
|
||||
| 72759576141929626464843750 => some "CognitiveLoadField"
|
||||
| 363797917962074279785156250 => some "CognitiveLoadField"
|
||||
| 9094947017729282379150390625 => some "CognitiveLoadField"
|
||||
| 9094947017729759216308593750 => some "ProjectableGeometryTopology"
|
||||
| 9094947203993797302246093750 => some "SignalShapedRouteCompiler"
|
||||
| 45474735088646411895751953125 => some "ProjectableGeometryTopology"
|
||||
| 45474735088646412048339846876 => some "CognitiveLoadField"
|
||||
| 45547494664788246155029687500 => some "CognitiveLoadField"
|
||||
| 227373675443232059478759765625 => some "SignalShapedRouteCompiler"
|
||||
| 227373675443232060241699609375 => some "ProjectableGeometryTopology"
|
||||
| 227373675443232063293457031250 => some "ProjectableGeometryTopology"
|
||||
| 227373675443234443664550781250 => some "CognitiveLoadField"
|
||||
| 227446435019376277923828125000 => some "CognitiveLoadField"
|
||||
| 5684341886080801486968994140625 => some "ProjectableGeometryTopology"
|
||||
| 5684414668940007686615234375000 => some "CognitiveLoadField"
|
||||
| 28421709430404007911682128906250 => some "CognitiveLoadField"
|
||||
| 28421709430405498027801513671875 => some "CognitiveLoadField"
|
||||
| 56843418860808014869689941406250 => some "CognitiveLoadField"
|
||||
| 56843491620384156703949218750000 => some "CognitiveLoadField"
|
||||
| 142108547152020037174226074218750 => some "ProjectableGeometryTopology"
|
||||
| 142108547152021527767181396484375 => some "CognitiveLoadField"
|
||||
| 170530256582424044609069824218750 => some "CognitiveLoadField"
|
||||
| 710542735760100185871124267578125 => some "ProjectableGeometryTopology"
|
||||
| 3552713678800500929355621337890750 => some "CognitiveLoadField"
|
||||
| 3552713678800500929355621337893750 => some "HoldForUnlawfulOrUnderspecifiedShape"
|
||||
| 3694822225952520966529846191409375 => some "HoldForUnlawfulOrUnderspecifiedShape"
|
||||
| 17763568394002504646778106689453125 => some "ProjectableGeometryTopology"
|
||||
| 17763568394002504646778106689468750 => some "ProjectableGeometryTopology"
|
||||
| 17763568394002504646778106933593750 => some "ProjectableGeometryTopology"
|
||||
| 17763568394002504646778107910156250 => some "ProjectableGeometryTopology"
|
||||
| 17905676941154524683952331542971875 => some "HoldForUnlawfulOrUnderspecifiedShape"
|
||||
| 17905677013914100825786590820312500 => some "SignalShapedRouteCompiler"
|
||||
| 88817841970012523233890533447265625 => some "ProjectableGeometryTopology"
|
||||
| 88817841970594599845409393554687500 => some "SignalShapedRouteCompiler"
|
||||
| 88817842333810441195964813232421875 => some "SignalShapedRouteCompiler"
|
||||
| 88959950517164543271064758300784375 => some "HoldForUnlawfulOrUnderspecifiedShape"
|
||||
| 444089209850062616169452667236328125 => some "CognitiveLoadField"
|
||||
| 444231318397214636206626892089846875 => some "HoldForUnlawfulOrUnderspecifiedShape"
|
||||
| 2220446049250313080847263336181640625 => some "ProjectableGeometryTopology"
|
||||
| 2220446049250313080849647521972656250 => some "SignalShapedRouteCompiler"
|
||||
| 2220588157797465100884437561035159375 => some "HoldForUnlawfulOrUnderspecifiedShape"
|
||||
| 11102372354798717424273490905761721875 => some "HoldForUnlawfulOrUnderspecifiedShape"
|
||||
| 55511151231257827021183967590341796875 => some "CognitiveLoadField"
|
||||
| 55511293339804979041218757629394534375 => some "HoldForUnlawfulOrUnderspecifiedShape"
|
||||
| 277555756156289135105907917022705078125 => some "CognitiveLoadField"
|
||||
| 277555898264836287125945091247558596875 => some "HoldForUnlawfulOrUnderspecifiedShape"
|
||||
| 1387778780781445675529539585113525391250 => some "HoldForUnlawfulOrUnderspecifiedShape"
|
||||
| 1387778780781445680186152458190917968750 => some "CognitiveLoadField"
|
||||
| 1387778780781446257606160640716552734375 => some "CognitiveLoadField"
|
||||
| 1387778780783264664933085441589355468750 => some "CognitiveLoadField"
|
||||
| 1387779491324181435629725456237792968750 => some "CognitiveLoadField"
|
||||
| 6938893903907228377647697925567628906250 => some "SignalShapedRouteCompiler"
|
||||
| 173472347597680709441192448139190673828125 => some "ProjectableGeometryTopology"
|
||||
| 173472347597680709441229701042175292968750 => some "ProjectableGeometryTopology"
|
||||
| 867361737988403547205963742733001708984375 => some "CognitiveLoadField"
|
||||
| 867361737988405366195403039455413818359375 => some "CognitiveLoadField"
|
||||
| 867361738698946282966062426567077636718750 => some "CognitiveLoadField"
|
||||
| 4336808689947702077915892004966735839843750 => some "SignalShapedRouteCompiler"
|
||||
| 4337086245698174025164917111396789550781250 => some "ProjectableGeometryTopology"
|
||||
| 4337086245698174025164917113780975341796875 => some "ProjectableGeometryTopology"
|
||||
| 8673617380594578207819722592830657958984375 => some "ProjectableGeometryTopology"
|
||||
| 21684321005466244969284161925315856933593750 => some "SignalShapedRouteCompiler"
|
||||
| 108420217248550443400745280086994171142578125 => some "ProjectableGeometryTopology"
|
||||
| 108420217248550443400745280086994201660156250 => some "CognitiveLoadField"
|
||||
| 108420217248550443400745280098915100097656250 => some "CognitiveLoadField"
|
||||
| _ => none
|
||||
|
||||
/-- Attested shape exact match via spectral-radius color gate. -/
|
||||
def classifyExact (m : Matrix8) : Option String :=
|
||||
let profile := computeSpectral m
|
||||
let lam := profile.adjacency_eigenvalue_max.toInt
|
||||
colorToShapeName (spectralRadiusToColor lam)
|
||||
|
||||
end SilverSight.PIST.Classify
|
||||
2526
formal/SilverSight/PIST/Matrices250.lean
Normal file
2526
formal/SilverSight/PIST/Matrices250.lean
Normal file
File diff suppressed because it is too large
Load diff
213
formal/SilverSight/PIST/Spectral.lean
Normal file
213
formal/SilverSight/PIST/Spectral.lean
Normal file
|
|
@ -0,0 +1,213 @@
|
|||
-- SilverSight.PIST.Spectral — minimal fixed-point spectral feature extraction
|
||||
--
|
||||
-- Ports only the surface needed for the RRC 250-equation classifier:
|
||||
-- • integer square root
|
||||
-- • power iteration for dominant eigenvalue
|
||||
-- • SpectralProfile record
|
||||
-- • computeSpectral over an 8×8 Int matrix
|
||||
--
|
||||
-- This is a stripped-down port of Research Stack's Semantics.PIST.Spectral.
|
||||
-- Photonic extensions, tactic-family heuristics, and Kubelka-Munk material
|
||||
-- are intentionally omitted to keep SilverSight focused on the RRC gate.
|
||||
|
||||
import SilverSight.FixedPoint
|
||||
|
||||
namespace SilverSight.PIST.Spectral
|
||||
|
||||
open SilverSight.FixedPoint
|
||||
open SilverSight.FixedPoint.Q16_16
|
||||
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
-- §1 Integer square root
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
/-- Integer square root via Newton's method. Returns floor(√n). -/
|
||||
def isqrt (n : Int) : Int :=
|
||||
if n ≤ 0 then 0
|
||||
else
|
||||
let rec loop (x : Int) (fuel : Nat) : Int :=
|
||||
match fuel with
|
||||
| 0 => x
|
||||
| f + 1 =>
|
||||
let x' := (x + n / x) / 2
|
||||
if x' ≥ x then x else loop x' f
|
||||
loop (n / 2 + 1) 64
|
||||
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
-- §2 Matrix-vector helpers (pure Int arithmetic)
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
@[inline]
|
||||
private def getEntry (mat : Array (Array Int)) (i j : Nat) : Int :=
|
||||
mat.getD i #[] |>.getD j 0
|
||||
|
||||
private def rowSum (mat : Array (Array Int)) (i n : Nat) : Int :=
|
||||
(List.range n).foldl (fun acc j => acc + getEntry mat i j) 0
|
||||
|
||||
private def symmetrize (mat : Array (Array Int)) (n : Nat) : Array (Array Int) :=
|
||||
Array.ofFn (n := n) fun i =>
|
||||
Array.ofFn (n := n) fun j =>
|
||||
(getEntry mat i.val j.val + getEntry mat j.val i.val) / 2
|
||||
|
||||
private def buildLaplacian (sym : Array (Array Int)) (n : Nat) : Array (Array Int) :=
|
||||
Array.ofFn (n := n) fun i =>
|
||||
let deg := rowSum sym i.val n
|
||||
Array.ofFn (n := n) fun j =>
|
||||
if i.val = j.val then deg else -(getEntry sym i.val j.val)
|
||||
|
||||
private def buildATA (mat : Array (Array Int)) (n : Nat) : Array (Array Int) :=
|
||||
Array.ofFn (n := n) fun i =>
|
||||
Array.ofFn (n := n) fun j =>
|
||||
(List.range n).foldl (fun acc k =>
|
||||
acc + getEntry mat k i.val * getEntry mat k j.val) 0
|
||||
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
-- §3 Power iteration (Q16_16 fixed-point)
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
private def normSqRaw (v : Array Q16_16) : Int :=
|
||||
v.foldl (fun acc x => acc + x.toInt * x.toInt) 0
|
||||
|
||||
private def matVecMul (mat : Array (Array Int)) (n : Nat) (v : Array Q16_16) : Array Q16_16 :=
|
||||
Array.ofFn (n := n) fun i =>
|
||||
let s : Int := (List.range n).foldl (fun acc j =>
|
||||
acc + getEntry mat i.val j * (v.getD j zero).toInt) 0
|
||||
ofRawInt s
|
||||
|
||||
/-- Dominant eigenvalue of a square Int matrix via power iteration. -/
|
||||
def powerIteration (mat : Array (Array Int)) (maxIter : Nat := 100) : Q16_16 :=
|
||||
let n := mat.size
|
||||
if n = 0 then zero
|
||||
else
|
||||
let initVal := ofRawInt ((q16Scale : Int) / (n : Int))
|
||||
let v₀ : Array Q16_16 := Array.replicate n initVal
|
||||
let rec iterate (v : Array Q16_16) (fuel : Nat) : Array Q16_16 :=
|
||||
match fuel with
|
||||
| 0 => v
|
||||
| f + 1 =>
|
||||
let mv := matVecMul mat n v
|
||||
let nm2 := normSqRaw mv
|
||||
if nm2 ≤ 0 then v
|
||||
else
|
||||
let nm := isqrt nm2
|
||||
if nm = 0 then v
|
||||
else
|
||||
let vn := mv.map (fun x => ofRawInt (x.toInt * q16Scale / nm))
|
||||
iterate vn f
|
||||
let vFinal := iterate v₀ maxIter
|
||||
let mv := matVecMul mat n vFinal
|
||||
let num : Int := (List.range n).foldl (fun acc i =>
|
||||
acc + (vFinal.getD i zero).toInt * (mv.getD i zero).toInt) 0
|
||||
let den : Int := normSqRaw vFinal
|
||||
if den ≤ 0 then zero
|
||||
else ofRawInt (num * q16Scale / den)
|
||||
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
-- §4 Spectral profile
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
structure SpectralProfile where
|
||||
matrix_size : Q16_16
|
||||
rank : Q16_16
|
||||
spectral_gap : Q16_16
|
||||
density : Q16_16
|
||||
trace_val : Q16_16
|
||||
frobenius_norm : Q16_16
|
||||
laplacian_zero_count : Q16_16
|
||||
adjacency_eigenvalue_max : Q16_16
|
||||
laplacian_eigenvalue_max : Q16_16
|
||||
singular_value_max : Q16_16
|
||||
deriving Repr
|
||||
|
||||
def emptyProfile : SpectralProfile :=
|
||||
{ matrix_size := zero
|
||||
rank := zero
|
||||
spectral_gap := zero
|
||||
density := zero
|
||||
trace_val := zero
|
||||
frobenius_norm := zero
|
||||
laplacian_zero_count := zero
|
||||
adjacency_eigenvalue_max := zero
|
||||
laplacian_eigenvalue_max := zero
|
||||
singular_value_max := zero }
|
||||
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
-- §5 computeSpectral
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
/-- Compute the full spectral profile of a proof transition matrix.
|
||||
Pure Int + Q16_16 arithmetic; no Float. -/
|
||||
def computeSpectral (mat : Array (Array Int)) : SpectralProfile :=
|
||||
let n := mat.size
|
||||
if n = 0 then emptyProfile
|
||||
else
|
||||
let sym := symmetrize mat n
|
||||
let lap := buildLaplacian sym n
|
||||
|
||||
let evMax := powerIteration sym
|
||||
|
||||
-- Second eigenvalue via shift-deflation (0.9 * ev_max on the diagonal)
|
||||
let shiftAmt : Int := (evMax.toInt * 58982) / q16Scale
|
||||
let shiftedMat : Array (Array Int) :=
|
||||
Array.ofFn (n := n) fun i =>
|
||||
Array.ofFn (n := n) fun j =>
|
||||
let base := getEntry sym i.val j.val
|
||||
if i.val = j.val then base - shiftAmt else base
|
||||
let evShift := powerIteration shiftedMat
|
||||
let evSecond : Q16_16 :=
|
||||
if evShift.toInt < evMax.toInt
|
||||
then ofRawInt (Int.natAbs (evMax.toInt - evShift.toInt) : Int)
|
||||
else evMax
|
||||
let spectralGap := sub evMax evSecond
|
||||
|
||||
let lapMax := powerIteration lap
|
||||
|
||||
let total : Int := mat.foldl (fun acc row => acc + row.foldl (· + ·) 0) 0
|
||||
let nSqI : Int := (n * n : Nat)
|
||||
let density := if nSqI ≤ 0 then zero else ofRawInt (total * q16Scale / nSqI)
|
||||
|
||||
let traceInt : Int := (List.range n).foldl (fun acc i => acc + getEntry mat i i) 0
|
||||
let traceVal := ofRawInt traceInt
|
||||
|
||||
let frobSq : Int := mat.foldl (fun acc row => acc + row.foldl (fun a c => a + c * c) 0) 0
|
||||
let frobNorm := ofRawInt (isqrt frobSq)
|
||||
|
||||
let rankVal : Int := mat.foldl (fun acc row =>
|
||||
acc + if row.any (· ≠ 0) then 1 else 0) 0
|
||||
|
||||
let lapZero : Int := (List.range n).foldl (fun acc i =>
|
||||
let rs := rowSum mat i n
|
||||
let d := getEntry mat i i
|
||||
acc + if rs - d = 0 then 1 else 0) 0
|
||||
|
||||
let ataM := buildATA mat n
|
||||
let ataEv := powerIteration ataM
|
||||
let svMax := if ataEv.toInt > 0 then sqrt ataEv else zero
|
||||
|
||||
{ matrix_size := ofRawInt (n : Int)
|
||||
rank := ofRawInt rankVal
|
||||
spectral_gap := spectralGap
|
||||
density := density
|
||||
trace_val := traceVal
|
||||
frobenius_norm := frobNorm
|
||||
laplacian_zero_count := ofRawInt lapZero
|
||||
adjacency_eigenvalue_max := evMax
|
||||
laplacian_eigenvalue_max := lapMax
|
||||
singular_value_max := svMax }
|
||||
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
-- §6 Witnesses
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
#eval isqrt 9 -- expect 3
|
||||
#eval isqrt 16 -- expect 4
|
||||
#eval isqrt 200 -- expect 14
|
||||
#eval isqrt 0 -- expect 0
|
||||
|
||||
#eval! (powerIteration #[#[1, 0], #[0, 1]]).toInt -- expect 65536
|
||||
|
||||
#eval! (computeSpectral #[#[1, 1], #[0, 1]]).matrix_size.toInt -- expect 2
|
||||
#eval! (computeSpectral #[#[1, 1], #[0, 1]]).rank.toInt -- expect 2
|
||||
#eval! (computeSpectral #[#[1, 1], #[0, 1]]).trace_val.toInt -- expect 2
|
||||
|
||||
end SilverSight.PIST.Spectral
|
||||
|
|
@ -36,6 +36,9 @@ lean_lib «SilverSightFormal» where
|
|||
lean_lib «SilverSightRRC» where
|
||||
srcDir := "formal"
|
||||
roots := #[
|
||||
`SilverSight.PIST.Spectral,
|
||||
`SilverSight.PIST.Classify,
|
||||
`SilverSight.PIST.Matrices250,
|
||||
`SilverSight.RRCLogogramProjection,
|
||||
`SilverSight.ReceiptCore,
|
||||
`SilverSight.RRC.Emit,
|
||||
|
|
|
|||
123
python/build_pist_matrices_250.py
Normal file
123
python/build_pist_matrices_250.py
Normal file
|
|
@ -0,0 +1,123 @@
|
|||
#!/usr/bin/env python3
|
||||
# /// script
|
||||
# requires-python = ">=3.10"
|
||||
# dependencies = []
|
||||
# ///
|
||||
"""
|
||||
Build formal/SilverSight/PIST/Matrices250.lean from
|
||||
shared-data/rrc_pist_predictions_250_v1.json (or a local copy).
|
||||
|
||||
Python's role: read the predictions artifact, serialize each 8×8 matrix as a
|
||||
Lean Array (Array Int) literal, emit an association list keyed by rrc_eq_<hex>.
|
||||
|
||||
The generated Lean file is consumed by SilverSight.PIST.Classify
|
||||
(classifyProxy/classifyExact) to produce pistProxyLabel/pistExactLabel.
|
||||
|
||||
Usage:
|
||||
python3 python/build_pist_matrices_250.py
|
||||
python3 python/build_pist_matrices_250.py \
|
||||
--predictions /path/to/rrc_pist_predictions_250_v1.json \
|
||||
--out-lean formal/SilverSight/PIST/Matrices250.lean
|
||||
"""
|
||||
from __future__ import annotations
|
||||
import argparse, hashlib, json, sys
|
||||
from pathlib import Path
|
||||
|
||||
|
||||
def lean_str(s: str) -> str:
|
||||
s = s.replace("\\", "\\\\").replace('"', '\\"')
|
||||
return f'"{s}"'
|
||||
|
||||
|
||||
def lean_array_int(xs: list[int]) -> str:
|
||||
inner = ", ".join(str(x) for x in xs)
|
||||
return f"#[{inner}]"
|
||||
|
||||
|
||||
def lean_matrix_rows(rows: list[list[int]]) -> str:
|
||||
inner = ",\n ".join(lean_array_int(r) for r in rows)
|
||||
return f"#[\n {inner}\n ]"
|
||||
|
||||
|
||||
def main() -> int:
|
||||
parser = argparse.ArgumentParser(
|
||||
description="Generate SilverSight PIST Matrices250.lean"
|
||||
)
|
||||
parser.add_argument(
|
||||
"--predictions",
|
||||
type=Path,
|
||||
default=Path("/home/allaun/Research Stack/shared-data/rrc_pist_predictions_250_v1.json"),
|
||||
help="Path to rrc_pist_predictions_250_v1.json",
|
||||
)
|
||||
parser.add_argument(
|
||||
"--out-lean",
|
||||
type=Path,
|
||||
default=Path("formal/SilverSight/PIST/Matrices250.lean"),
|
||||
help="Output Lean module path",
|
||||
)
|
||||
args = parser.parse_args()
|
||||
|
||||
preds = json.loads(args.predictions.read_text())
|
||||
raw = preds.get("predictions", [])
|
||||
print(f"Loaded {len(raw)} predictions from {args.predictions}", file=sys.stderr)
|
||||
|
||||
# Deterministic order by equation_id for reproducible builds.
|
||||
raw_sorted = sorted(raw, key=lambda p: p.get("equation_id", ""))
|
||||
|
||||
entries: list[str] = []
|
||||
for p in raw_sorted:
|
||||
eid = p.get("equation_id", "")
|
||||
mat = p.get("matrix_8x8", [])
|
||||
if not eid or len(mat) != 8:
|
||||
print(f"WARNING: skipping malformed entry {eid}", file=sys.stderr)
|
||||
continue
|
||||
matrix_lean = lean_matrix_rows(mat)
|
||||
entries.append(f" ({lean_str(eid)}, {matrix_lean})")
|
||||
|
||||
# Include a content hash so the generated file can be validated.
|
||||
content_blob = json.dumps(
|
||||
{p.get("equation_id"): p.get("matrix_8x8") for p in raw_sorted},
|
||||
sort_keys=True,
|
||||
separators=(",", ":"),
|
||||
).encode("utf-8")
|
||||
content_hash = hashlib.sha256(content_blob).hexdigest()
|
||||
|
||||
lines = [
|
||||
"-- SilverSight.PIST.Matrices250 — AUTO-GENERATED by python/build_pist_matrices_250.py",
|
||||
"-- DO NOT EDIT BY HAND. Regenerate with:",
|
||||
"-- python3 python/build_pist_matrices_250.py",
|
||||
"--",
|
||||
"-- Source: rrc_pist_predictions_250_v1.json",
|
||||
"-- Content hash (SHA-256 canonical matrices): " + content_hash,
|
||||
"--",
|
||||
"-- This file is consumed by SilverSight.PIST.Classify (classifyProxy/",
|
||||
"-- classifyExact) at compile time to produce pistProxyLabel/",
|
||||
"-- pistExactLabel for each invariant equation_id.",
|
||||
"",
|
||||
"namespace SilverSight.PIST.Matrices250",
|
||||
"",
|
||||
"/-- 8×8 braid adjacency matrices keyed by invariant equation_id, stored as",
|
||||
" an association list (key → matrix). Generated from",
|
||||
" rrc_pist_predictions_250_v1.json.",
|
||||
f" Entries: {len(entries)}. -/",
|
||||
"def pistMatrices250 : List (String × Array (Array Int)) :=",
|
||||
" [",
|
||||
",\n".join(entries),
|
||||
" ]",
|
||||
"",
|
||||
"/-- Look up an 8×8 matrix by invariant equation_id. -/",
|
||||
"def findMatrix (eqId : String) : Option (Array (Array Int)) :=",
|
||||
" pistMatrices250.find? (fun (k, _) => k = eqId) |>.map (fun (_, v) => v)",
|
||||
"",
|
||||
"end SilverSight.PIST.Matrices250",
|
||||
"",
|
||||
]
|
||||
|
||||
args.out_lean.parent.mkdir(parents=True, exist_ok=True)
|
||||
args.out_lean.write_text("\n".join(lines))
|
||||
print(f"Wrote {args.out_lean} ({len(entries)} entries)", file=sys.stderr)
|
||||
return 0
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
sys.exit(main())
|
||||
Loading…
Add table
Reference in a new issue