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 0f15842507
commit 436e5ae8ca
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 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"]})

View file

@ -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,