feat(pist): flexure features v2 — full spectral profile per joint

- 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
This commit is contained in:
Brandon Schneider 2026-05-26 11:00:31 -05:00
parent a44f0f002c
commit d99ad55ba6
2 changed files with 76 additions and 3 deletions

View file

@ -8,6 +8,7 @@ inserts them into ene.flexures, and mines recurring patterns.
import glob import glob
import hashlib import hashlib
import json import json
import math
import os import os
import subprocess import subprocess
import sys 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__), ".")) sys.path.insert(0, os.path.join(os.path.dirname(__file__), "."))
from trace_canary_theorems import CANARY_THEOREMS 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 = { TACTIC_FAMILIES = {
"rw": "rewrite", "simp": "normalization", "omega": "arithmetic", "rw": "rewrite", "simp": "normalization", "omega": "arithmetic",
@ -135,6 +192,9 @@ def ingest_flexures():
labels = get_theorem_labels(name) labels = get_theorem_labels(name)
tactics = labels.get("tactics", []) tactics = labels.get("tactics", [])
# Compute full spectral features from the transition matrix
spectral = compute_spectral(matrix)
# Build flexure joints from tag pairs # Build flexure joints from tag pairs
joints = [] joints = []
for i in range(0, len(tags) - 1, 2): for i in range(0, len(tags) - 1, 2):
@ -165,6 +225,7 @@ def ingest_flexures():
"matrix_rank": max(0, n_unique - 1), "matrix_rank": max(0, n_unique - 1),
"n_unique": n_unique, "n_unique": n_unique,
"status": status, "status": status,
"spectral": spectral, # full spectral profile
} }
joints.append(joint) joints.append(joint)
@ -182,6 +243,8 @@ def ingest_flexures():
"obstruction": j.get("obstruction"), "obstruction": j.get("obstruction"),
"matrix_rank": j["matrix_rank"], "matrix_rank": j["matrix_rank"],
"n_unique_states": j["n_unique"], "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"]}) chosen = json.dumps({"tactic_applied": j["tactic"], "joint_type": j["joint_label"]})

View file

@ -10,7 +10,7 @@ import sys
from collections import Counter, defaultdict from collections import Counter, defaultdict
from math import sqrt from math import sqrt
FLEXURE_SESSION = "d94c6353-5ed9-42a4-b2b7-d0fee8b36a8e" FLEXURE_SESSION = "ae31d595-0535-4a0c-9d41-af9c0357dba1"
def connect(): def connect():
host = os.environ.get("RDS_HOST", "database-1-instance-1.cghu8yqogqwo.us-east-1.rds.amazonaws.com") 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: if not flexures:
return return
# Build vector + labels for each # Build vector + labels for each (v2: coarse + spectral)
recs = [] recs = []
for fx in flexures: for fx in flexures:
s = fx["signals"] s = fx["signals"]
sp = s.get("spectral", {})
vec = [ vec = [
float(s.get("delta_score", 0)), float(s.get("delta_score", 0)),
float(s.get("matrix_rank", 0)), float(s.get("matrix_rank", 0)),
float(s.get("n_unique_states", 0)), float(s.get("n_unique_states", 0)),
float(fx.get("pre_residual", 0)), float(fx.get("pre_residual", 0)),
1.0 if fx.get("converged") else 0.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({ recs.append({
"vec": vec, "vec": vec,