mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
569c16088a
- 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.
123 lines
4.3 KiB
Python
123 lines
4.3 KiB
Python
#!/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())
|