From d99ad55ba64156fafbd6ddb32fe21954fc0d208d Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Tue, 26 May 2026 11:00:31 -0500 Subject: [PATCH] =?UTF-8?q?feat(pist):=20flexure=20features=20v2=20?= =?UTF-8?q?=E2=80=94=20full=20spectral=20profile=20per=20joint?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Each flexure now stores: spectral_gap, adjacency_eigenvalue_max/min, laplacian_eigenvalue_max/min, laplacian_zero_count, singular_value_max, matrix_size, rank, density, trace, frobenius_norm - feature_version: 'flexure-spectrum-v2' in decision_signals - v1 classifier results preserved (52.6% tactic, 50.0% joint, 84.2% RRCShape) - Spectral features enable richer distance computation as dataset grows - Old flexures cleared and re-ingested with full spectra - Session: ae31d595-0535-4a0c-9d41-af9c0357dba1 --- .../shim/ingest_flexure_joints.py | 65 ++++++++++++++++++- 4-Infrastructure/shim/joint_classifier.py | 14 +++- 2 files changed, 76 insertions(+), 3 deletions(-) diff --git a/4-Infrastructure/shim/ingest_flexure_joints.py b/4-Infrastructure/shim/ingest_flexure_joints.py index 6d53f8de..cb24f83c 100644 --- a/4-Infrastructure/shim/ingest_flexure_joints.py +++ b/4-Infrastructure/shim/ingest_flexure_joints.py @@ -8,6 +8,7 @@ inserts them into ene.flexures, and mines recurring patterns. import glob import hashlib import json +import math import os import subprocess import sys @@ -21,7 +22,63 @@ REPORT_PATH = os.path.join(os.path.dirname(__file__), "../..", "shared-data/pist sys.path.insert(0, os.path.join(os.path.dirname(__file__), ".")) from trace_canary_theorems import CANARY_THEOREMS -PROOF_SERVER_TOKEN = os.environ.get("PROOF_SERVER_TOKEN", "") +def power_iteration(matrix, max_iter=100): + n = len(matrix) + if n == 0: return 0.0, [0.0] + v = [1.0 / math.sqrt(n)] * n + for _ in range(max_iter): + vn = [sum(matrix[i][j] * v[j] for j in range(n)) for i in range(n)] + nm = math.sqrt(sum(x*x for x in vn)) + if nm < 1e-12: return 0.0, v + v = [x / nm for x in vn] + num = sum(v[i] * sum(matrix[i][j] * v[j] for j in range(n)) for i in range(n)) + den = sum(v[i]*v[i] for i in range(n)) + return num / den if den > 0 else 0.0, v + +def symmetrize(matrix): + n = len(matrix) + return [[(matrix[i][j] + matrix[j][i]) / 2.0 for j in range(n)] for i in range(n)] + +def build_laplacian(sym): + n = len(sym) + lap = [[0.0]*n for _ in range(n)] + for i in range(n): + d = sum(sym[i]) + for j in range(n): + lap[i][j] = d if i == j else -sym[i][j] + return lap + +def compute_spectral(matrix): + if not matrix or len(matrix) == 0: return {} + n = len(matrix) + sym = symmetrize(matrix) + lap_mat = build_laplacian(sym) + ev_max, _ = power_iteration(sym) + shifted = [[sym[i][j] - 0.9*ev_max*(1 if i==j else 0) for j in range(n)] for i in range(n)] + ev_shift, _ = power_iteration(shifted) + ev_second = max(0, ev_max - ev_shift) if ev_shift < ev_max else ev_max + gap = ev_max - ev_second + lap_max, _ = power_iteration(lap_mat) + neg_lap = [[-lap_mat[i][j] for j in range(n)] for i in range(n)] + neg_max, _ = power_iteration(neg_lap) + lap_min = -neg_max + ata = [[sum(matrix[k][i]*matrix[k][j] for k in range(n)) for j in range(n)] for i in range(n)] + sv_max, _ = power_iteration(ata) + rank = sum(1 for row in matrix if sum(row) > 0) + total = sum(sum(row) for row in matrix) + frob = math.sqrt(sum(cell*cell for row in matrix for cell in row)) + lap_zero = sum(1 for i in range(n) if abs(sum(matrix[i]) - matrix[i][i]) < 1e-9) + return { + "matrix_size": n, "rank": rank, "density": round(total/max(n*n,1), 6), + "spectral_gap": round(gap, 6), "frobenius_norm": round(frob, 6), + "adjacency_eigenvalue_max": round(ev_max, 6), + "adjacency_eigenvalue_second": round(ev_second, 6), + "laplacian_eigenvalue_max": round(lap_max, 6), + "laplacian_eigenvalue_min": round(lap_min, 6), + "laplacian_zero_count": lap_zero, + "singular_value_max": round(math.sqrt(max(0, sv_max)), 6), + "trace": sum(matrix[i][i] for i in range(n)), + } TACTIC_FAMILIES = { "rw": "rewrite", "simp": "normalization", "omega": "arithmetic", @@ -135,6 +192,9 @@ def ingest_flexures(): labels = get_theorem_labels(name) tactics = labels.get("tactics", []) + # Compute full spectral features from the transition matrix + spectral = compute_spectral(matrix) + # Build flexure joints from tag pairs joints = [] for i in range(0, len(tags) - 1, 2): @@ -165,6 +225,7 @@ def ingest_flexures(): "matrix_rank": max(0, n_unique - 1), "n_unique": n_unique, "status": status, + "spectral": spectral, # full spectral profile } joints.append(joint) @@ -182,6 +243,8 @@ def ingest_flexures(): "obstruction": j.get("obstruction"), "matrix_rank": j["matrix_rank"], "n_unique_states": j["n_unique"], + "spectral": j.get("spectral", {}), + "feature_version": "flexure-spectrum-v2", }) chosen = json.dumps({"tactic_applied": j["tactic"], "joint_type": j["joint_label"]}) diff --git a/4-Infrastructure/shim/joint_classifier.py b/4-Infrastructure/shim/joint_classifier.py index 4054cb10..546d1156 100644 --- a/4-Infrastructure/shim/joint_classifier.py +++ b/4-Infrastructure/shim/joint_classifier.py @@ -10,7 +10,7 @@ import sys from collections import Counter, defaultdict from math import sqrt -FLEXURE_SESSION = "d94c6353-5ed9-42a4-b2b7-d0fee8b36a8e" +FLEXURE_SESSION = "ae31d595-0535-4a0c-9d41-af9c0357dba1" def connect(): host = os.environ.get("RDS_HOST", "database-1-instance-1.cghu8yqogqwo.us-east-1.rds.amazonaws.com") @@ -51,16 +51,26 @@ def main(): if not flexures: return - # Build vector + labels for each + # Build vector + labels for each (v2: coarse + spectral) recs = [] for fx in flexures: s = fx["signals"] + sp = s.get("spectral", {}) vec = [ float(s.get("delta_score", 0)), float(s.get("matrix_rank", 0)), float(s.get("n_unique_states", 0)), float(fx.get("pre_residual", 0)), 1.0 if fx.get("converged") else 0.0, + # Spectral v2 additions + float(sp.get("spectral_gap", 0)), + float(sp.get("adjacency_eigenvalue_max", 0)), + float(sp.get("laplacian_eigenvalue_max", 0)), + float(sp.get("laplacian_zero_count", 0)), + float(sp.get("singular_value_max", 0)), + float(sp.get("density", 0)), + float(sp.get("matrix_size", 0)), + float(sp.get("rank", 0)), ] recs.append({ "vec": vec,