mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
4a72ad1183
## New module: Semantics.PIST.Spectral Ports the two domain-logic functions from pist_trace_classify_mcp.py that were previously executing in unverified Python: ### classify_tactic_from_name → classifyTacticFromName - `TacticFamily` inductive (rewrite, normalization, arithmetic, induction, algebraic, case_analysis, discharge, reflexivity, unknown) - Pure string-lookup; 5 executable witnesses confirm all branches. ### compute_spectral → computeSpectral - `isqrt` — integer Newton's method for floor(√n); 4 witnesses. - `powerIteration` — Q16_16 fixed-point dominant eigenvalue via power iteration with Rayleigh quotient; identity-matrix witness = 65536. - `SpectralProfile` structure — 10 fields (matrix_size, rank, spectral_gap, density, trace_val, frobenius_norm, laplacian_zero_count, adjacency_eigenvalue_max, laplacian_eigenvalue_max, singular_value_max). - `computeSpectral` — symmetrize → lap → powerIteration → shift-deflation for second eigenvalue → AᵀA for singular value; 3 witnesses on 2×2 fixture. No Float in any compute path. All magic constants documented with formulas. ## Other changes - Semantics.lean: add `import Semantics.PIST.Spectral` - AgenticOrchestration.lean:163: expand bare `-- TODO(lean-port):` label - pist_trace_classify_mcp.py: update PARTIAL BOUNDARY comment to name the Lean module that now owns spectral logic ## Build baseline lake build Compiler → 3311 jobs, 0 errors Generated with [Devin](https://cli.devin.ai/docs) Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com> |
||
|---|---|---|
| .. | ||
| conversions/hardware | ||
| external/OTOM | ||
| LeanGPT | ||
| Semantics | ||
| CHAIN_ALL_REVIEW_REPORT.md | ||