Brandon Schneider
|
153a8da5c5
|
feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems
- 24/24 processed, 0 errors (12 verified, 12 failed)
- Average 2.0 steps per proof (max 5 steps)
- 11 tactic families detected
- Verified proofs: avg gap=2.50 vs Failed: avg gap=1.50
- proof_traces/*.trace.json + *.decomp.json stored per theorem
|
2026-05-26 02:37:22 -05:00 |
|
Brandon Schneider
|
b3d4ef4206
|
feat(pist): Tier 2 trace bridge — tactic-level goal transitions
- lean_trace_bridge.py: captures Goal_i → tactic → Goal_{i+1} transitions
- Builds ProofTraceReceipt v1 with step deltas, transition matrix, flexure joints
- Handles single-line by-blocks, semicolon-separated, and indented multi-line
- pist_trace_decompose.py: spectral analysis of transition matrix
- Power iteration for eigenvalue estimation
- Spectral gap, rank, density, Laplacian zero count
- Tactic family distribution, delta statistics
- Full pipeline: Lean theorem → trace → transition graph → spectral features
|
2026-05-26 02:28:16 -05:00 |
|