mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
allaun
558431fc45
- Renamed Corpus278/Matrices278 to Corpus250/Matrices250 across all Lean modules, Python shims, JSON schemas, and documentation - Applied SLOS-calibrated defaults to braid_search.py: bracket_cost base=8x/16x, crossing_penalty gap_reward=0.01 - Synced same defaults to research-compute-fabric submodule - Updated Burgers 0D defaults: nu=0.9995, advection=0.075 - Fixed 278→250 refs in pist_predictions JSON (claim_boundary, total) - Fixed stale schema refs in .devin/skills/lean-proof/SKILL.md - Updated AGENTS.md build baselines to post-clean counts (3314 jobs) - Updated lake-manifest.json sparkle rev to match lakefile.toml - Fixed Q16_16 signed conversion bug in qaoa_adapter tunable costs - NBody.lean: pre-existing dirty changes (introN failures, NOT our work) Build: 3314 jobs, 0 errors (lake build Compiler)
98 lines
3.7 KiB
Python
98 lines
3.7 KiB
Python
#!/usr/bin/env python3
|
||
# /// script
|
||
# requires-python = ">=3.10"
|
||
# dependencies = []
|
||
# ///
|
||
"""
|
||
Build Semantics/PIST/Matrices250.lean from rrc_pist_predictions_250_v1.json.
|
||
|
||
Python's role: read the predictions artifact, serialize each 8×8 matrix as a
|
||
Lean Array (Array Int) literal, emit a Std.HashMap keyed by rrc_eq_<hex>.
|
||
|
||
Generated Lean file is consumed by Semantics.PIST.Classify (classifyProxy/
|
||
classifyExact) when labels are computed in v2+.
|
||
|
||
Usage:
|
||
python3 4-Infrastructure/shim/build_pist_matrices_250.py
|
||
|
||
Dependencies:
|
||
shared-data/rrc_pist_predictions_250_v1.json (pist_matrix_builder.py output)
|
||
"""
|
||
from __future__ import annotations
|
||
import json, sys
|
||
from pathlib import Path
|
||
|
||
ROOT = Path("/home/allaun/Research Stack")
|
||
PREDICTIONS_JSON = ROOT / "shared-data/rrc_pist_predictions_250_v1.json"
|
||
OUT_LEAN = ROOT / "0-Core-Formalism/lean/Semantics/Semantics/PIST/Matrices250.lean"
|
||
|
||
|
||
def lean_str(s: str) -> str:
|
||
s = s.replace("\\", "\\\\").replace('"', '\\"')
|
||
return f'"{s}"'
|
||
|
||
|
||
def lean_array_int(xs: list[int]) -> str:
|
||
"""Format a list of ints as a Lean Array literal."""
|
||
inner = ", ".join(str(x) for x in xs)
|
||
return f"#[{inner}]"
|
||
|
||
|
||
def lean_matrix_rows(rows: list[list[int]]) -> str:
|
||
"""Format an 8×8 matrix as a Lean Array (Array Int) literal."""
|
||
inner = ",\n ".join(lean_array_int(r) for r in rows)
|
||
return f"#[\n {inner}\n ]"
|
||
|
||
|
||
def main() -> int:
|
||
preds = json.loads(PREDICTIONS_JSON.read_text())
|
||
raw = preds.get("predictions", [])
|
||
print(f"Loaded {len(raw)} predictions from {PREDICTIONS_JSON}", file=sys.stderr)
|
||
|
||
lines: list[str] = []
|
||
lines.append("-- Semantics.PIST.Matrices250 — AUTO-GENERATED by build_pist_matrices_250.py")
|
||
lines.append("-- DO NOT EDIT BY HAND. Regenerate with:")
|
||
lines.append("-- python3 4-Infrastructure/shim/build_pist_matrices_250.py")
|
||
lines.append("--")
|
||
lines.append("-- Source: shared-data/rrc_pist_predictions_250_v1.json")
|
||
lines.append("-- (generated by 4-Infrastructure/shim/pist_matrix_builder.py)")
|
||
lines.append("--")
|
||
lines.append("-- This file is consumed by Semantics.PIST.Classify (classifyProxy/")
|
||
lines.append("-- classifyExact) at compile time to produce pistProxyLabel/")
|
||
lines.append("-- pistExactLabel for each invariant equation_id.")
|
||
lines.append("")
|
||
lines.append("namespace Semantics.PIST.Matrices250")
|
||
lines.append("")
|
||
lines.append("/-- 8×8 braid adjacency matrices keyed by invariant equation_id, stored as")
|
||
lines.append(" an association list (key → matrix). 250 entries; linear lookup is fine.")
|
||
lines.append(" Generated from rrc_pist_predictions_250_v1.json. -/")
|
||
lines.append(f"def pistMatrices250 : List (String × Array (Array Int)) :=")
|
||
lines.append(" [")
|
||
|
||
entry_strs: list[str] = []
|
||
for p in raw:
|
||
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)
|
||
entry_strs.append(f" ({lean_str(eid)}, {matrix_lean})")
|
||
|
||
lines.append(",\n".join(entry_strs))
|
||
lines.append(" ]")
|
||
lines.append("")
|
||
lines.append("/-- Look up an 8×8 matrix by invariant equation_id. -/")
|
||
lines.append("def findMatrix (eqId : String) : Option (Array (Array Int)) :=")
|
||
lines.append(" pistMatrices250.find? (fun (k, _) => k = eqId) |>.map (fun (_, v) => v)")
|
||
lines.append("")
|
||
lines.append("end Semantics.PIST.Matrices250")
|
||
lines.append("")
|
||
|
||
OUT_LEAN.write_text("\n".join(lines))
|
||
print(f"Wrote {OUT_LEAN} ({len(entry_strs)} entries)", file=sys.stderr)
|
||
return 0
|
||
|
||
|
||
if __name__ == "__main__":
|
||
sys.exit(main())
|