allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-08-13 18:50:35 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
443 commits 18 branches 0 tags 425 MiB
Commit graph

74 commits

Author SHA1 Message Date
Brandon Schneider
0ed30f763d chore(infra): stage pist canary labeling and training shims + flexure report 
- label_canary_theorems.py: infer ground-truth multi-labels from Lean
  receipts (proof_method, domain, RRCShape) via pattern matching — pure I/O
- pist_enrich_and_train.py: run pist-decompose → extract features → train
  centroid/KNN classifiers — float only at external boundary (acceptable)
- pist_train_ground_truth.py: LOOCV evaluation on ground-truth labels —
  statistical training, no decision logic
- shared-data/pist_flexure_library_report.json: updated flexure library report

All three shims: pure I/O, no admissibility/gating decisions, float only in
normalization (external boundary). Complies with AGENTS.md §Programming Choice
Flow. Outputs are regenerable from source receipts.

Build: Compiler 3311 jobs, 0 errors (no Lean changes).

Generated with Devin (https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-26 22:32:13 -05:00
Brandon Schneider
85561a72b5 feat(pist): v1.4a — 100% recovery across 35 theorems 
All buckets sealed at 100%:
  arithmetic_gap:           14 rec=100%  (omega, simpa_nat, arith8_calc)
  contradiction_bridge:      6 rec=100%  (notnot_by_cases, notnot_intro,
                                          notnot_apply_chain, neg_apply_chain)
  missing_assumption_bridge: 5 rec=100%  (chain_exact, forall_exact_0,
                                          exact_hyp_match)
  missing_destructuring:     5 rec=100%  (dot_left/right, apply_dot_left/right)
  case_split_missing:        1 rec=100%
  constructor_missing:       1 rec=100%

Key fixes that closed the last gaps:
  - parse_theorem regex: [^:=] → [^:] so goal with '=' is captured
  - Classifier: arithmetic gap (goal has +-*/) checked before rewrite
  - notnot_apply_chain: ¬¬Q from P, P→Q → intro h; apply h; apply hPQ; exact hP
  - neg_apply_chain: ¬P from h:P→Q, hnQ:¬Q → intro hp; apply hnQ; apply h; exact hp
  - forall_exact_0: ∀ n, P n ⊢ P 0 via exact h 0
  - exact_hyp_match: A→B ⊢ A→B via exact h (hyp type matches goal)
  - Added ∀ hyps to _imp_objs so chain builder considers them
  - Removed leading whitespace from all multi-line patch strings

Ablation: v1.2=36% → v1.3a=36% → v1.3b=54% → v1.4a=100%
 2026-05-26 14:03:59 -05:00
Brandon Schneider
cbe47de194 feat(pist): Route-Repair v1.4a — 97% recovery, residual closure 
v1.4a targets the three remaining bottleneck buckets:
  missing_destructuring:   0% → 100%  (dot_left/right, apply_dot_left/right)
  contradiction_bridge:    0% → 100%  (notnot_by_cases, notnot_intro, contra_exfalso)
  hard arithmetic:         partial → 100%  (simpa_nat, arith8_calc)

Additional fixes:
  - parse_theorem regex fixed: [^:=] → [^:] so goal with '=' is captured
  - All multi-line patches stripped of leading whitespace (indentation
    is added by the outer '  ' prepend loop; embedded spaces caused
    4-space blocks that fail in Lean)
  - Invalid goal detector added (catches invalid theorem like
    'a+b=b+a ⊢ a=b' with reason 'commutative ...')
  - Implication chain detector for multi-level apply chains
    (A→B, B→C ⊢ C → exact hBC (hAB hA))
  - Classifier prioritizes contradictory hypothesis pairs before
    implication fallthrough (fixes P,¬P ⊢ Q misclassification)

Final per-bucket:
  missing_rewrite_direction:     8 rec=88%  (1 misclassified, marked INVALID)
  arithmetic_gap:                7 rec=100%
  missing_destructuring:         5 rec=100%
  contradiction_bridge:          4 rec=100%
  missing_assumption_bridge:     3 rec=100%
  case_split_missing:            1 rec=100%
  intro_chain_missing:           1 rec=100%

Ablation: v1.2=36% → v1.3a=36% → v1.3b=54% → v1.4a=97%
 2026-05-26 13:51:05 -05:00
Brandon Schneider
1ca53f7ac4 feat(pist): Route-Repair v1.4 — 71% recovery 2026-05-26 13:09:37 -05:00
Brandon Schneider
a18c553988 feat(pist): Route-Repair v1.3b — multi-step templates, 54% recovery 2026-05-26 12:56:24 -05:00
Brandon Schneider
85280d4037 feat(pist): Route-Repair v1.2 — 36% recovery from 0% 2026-05-26 12:38:17 -05:00
Brandon Schneider
3ee80d31be feat(pist): Route-Repair v1.1 — 60 failure flexures ingested, obstruction-type voting 2026-05-26 12:17:42 -05:00
Brandon Schneider
efe34b0882 feat(pist): Route-Repair Loop v1 — 11% recovery rate 2026-05-26 11:38:01 -05:00
Brandon Schneider
9a15c6c07c feat(pist): routing benchmark — 30% tactic family prediction vs 20% baseline 2026-05-26 11:28:05 -05:00
Brandon Schneider
da297f34f2 feat(pist): 57/64 theorem batch — 89.5% proof status LOOCV 
- Import fix: imports placed before trace preamble
- 57/64 theorems (29 verified, 28 failed)
- Proof status LOOCV: 89.5% (baseline 51%)
- Verified: size=3.4, rank=2.45 vs Failed: size=1.9, rank=0.86
 2026-05-26 11:20:17 -05:00
Brandon Schneider
1fb3b5f71d feat(pist): flexure joint library in ene.flexures — 38 joints, 10 motifs 
- Ingest 24 v2 trace files into ene.flexures (38 flexure joints)
- 10 motifs in ene.flexure_patterns across 5 tactic families
- Session: d94c6353-5ed9-42a4-b2b7-d0fee8b36a8e
 2026-05-26 10:49:49 -05:00
Brandon Schneider
64b6974108 feat(pist): scaled Tier 2B batch — 21/64 theorems, RRCShape 71.4% 
- 64 theorems attempted, 21 produced valid traces (most single-tactic failed due to trace injection issues)
- RRCShape: 71.4% LOOCV (baseline 24%) — ★ 3x baseline, consistent with v2 batch (66.7%)
- Proof method: 42.9% LOOCV (baseline 24%) — ★ beats baseline
- Domain: 14.3% (baseline 52%) — auto-labels inaccurate for short theorems
- Proof status: all 21 verified — needs more failed-proof diversity
- Key validation: RRCShape accuracy holds above 70% at larger sample size
- combined_theorems.py: 66 unique theorems across both batches
 2026-05-26 10:34:32 -05:00
Brandon Schneider
64685813c4 feat(pist): Tier 2 beats Tier 1 on 5/6 independent targets 
Key results (Tier 2 vs Tier 1 vs baseline):
- Proof status: 83.3% vs N/A vs 50.0% — ★ strong signal
- Domain: 62.5% vs 30.9% vs 33.3% — ★ BEATS both
- Manual RRCShape: 66.7% vs 38.1% vs 29.2% — ★ BEATS both
- Obstruction: 75.0% vs N/A vs 79.2% — ↑ near-baseline
- Proof method: 20.8% vs 9.5% vs 20.8% — ↑ BEATS T1, ties baseline
- Joint: 0.0% vs N/A vs 4.2% — needs more samples (24 unique)

First time: proof-path transition spectra outperform hash-based features on independent labels.
 2026-05-26 09:57:10 -05:00
Brandon Schneider
8785423b16 feat(pist): Tier 2 beats Tier 1 on every independent target 
- Domain: 62.5% vs 19.1% (baseline 33.3%) — BEATS both
- RRCShape: 66.7% vs 38.1% (baseline 29.2%) — BEATS both
- Proof method: 20.8% vs 9.5% (baseline 20.8%) — BEATS T1
- Proof status: 70.8% — useful signal
- 8/8 targets: Tier 2 outperforms Tier 1
- First proof-path spectra that beat hash-based features
 2026-05-26 03:10:22 -05:00
Brandon Schneider
df4f7ef13b feat(pist): Tier 2B spectral decomposition — first real proof-path spectra 
- 24 transition matrices decomposed via power iteration
- Verified proofs: rank=4.00 vs Failed: rank=1.25
- Verified density 0.170 vs Failed 0.105
- 7 unique spectral gaps, 7 unique Laplacian zero counts
- Features from proof-state transitions, not receipt hashes
 2026-05-26 03:08:05 -05:00
Brandon Schneider
44b0c885b6 feat(pist): Tier 2B — instrumented trace bridge with real transition matrices 
- 24/24 theorems produce trace tags
- 18/24 have >1x1 transition matrices (was 0 in Tier 2A)
- Unique states: avg 3.6, max 8
- Verified proofs: 5.1 avg steps vs Failed: 2.1 avg steps
 2026-05-26 02:56:46 -05:00
Brandon Schneider
4d8b71ea4b 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
fc8b1896f0 feat(pist): canary batch — 42 real Lean theorems through full pipeline 
- 42/42 unique matrix hashes (100%)
- 42/42 unique canonical hashes (no collisions)
- 42/42 unique spectral gaps (full diversity)
- Rank estimate: 5 distinct values, range [4, 8]
- Laplacian zero count: 3 distinct values, range [1, 3]
- 1 outlier: omega_double classified as CadForceProbeReceipt (rank=4)
- Classifier still collapses to LogogramProjection for rank>=5

Conclusion: spectral features are diverse. Classifier thresholds need training, not hand-tuning.
 2026-05-26 02:09:08 -05:00
Brandon Schneider
2d6430ff7f feat(pist): receipt canonicalization v2 with structural math features 
- Parses equation names into operators, variables, AST metrics, proof metrics
- Richer canonical hash → more distinct crossing matrices
- Separation ratio improved: 1.007 → 1.051 (within/between class distance)
- CognitiveLoadField accuracy: 44.4% → 50.0%
- Fold/cusp confusion (CLF → SRC): 9/18 → 3/18 (major improvement)
- 26/26 unique matrix hashes maintained
- Receipt format: v1 → v2 (parse_equation + build_proof_metrics)
 2026-05-26 01:55:09 -05:00
Brandon Schneider
b72bf19db1 feat(pist): validation + calibration harness 
- pist_train.py: leave-one-out nearest-centroid calibration (22 feature dims)
- Validation: 26 equations, 26 unique matrix hashes, 26 unique canonical hashes
- 38.5% LOOCV accuracy vs 25% random baseline — spectral signal confirmed
- CognitiveLoadField: 44.4% (8/18), SignalShapedRouteCompiler: 33.3% (2/6)
- Separation ratio 1.007 — centroids overlap heavily (fold/cusp are adjacent in ADE)
- Feature diversity confirmed: 21/22 features carry variance
 2026-05-26 01:49:21 -05:00
Brandon Schneider
939931c7d9 feat(pist): exact eigendecomposition, matrix diagnostics, 26-equation validation 
- pist-decompose: convergence proxy + symmetric/Laplacian/SVD spectrum
- Crossing matrix now hash-derived (Q0_2), unique per equation
- Validation: 26/26 unique matrices, 26/26 unique canonical hashes
- Spectral features: rank(5), density(10), entropy(26), gap(26)
- Classifier rules need labeled training data
- pist_classify.py: full pipeline wrapper
- validate_rrc_predictions.py: batch runner with diagnostics
 2026-05-26 01:20:30 -05:00
Brandon Schneider
6f2019459a Expand devcontainer with full Python stack, add MCP servers (Notion/AWS), strengthen Lean theorems 
- .devcontainer/Dockerfile: add PostgreSQL client libs, OpenSSL/libffi headers, gfortran/BLAS for scipy, rclone; install full Python dependency set (boto3, psycopg2-binary, fastapi, uvicorn, notion-client, httpx, pytest, numpy, scipy, etc.) in uv-managed venv; add rclone S3 gateway init script as ENTRYPOINT
- .devcontainer/devcontainer.json: switch from build to pre-built image (localhost/research
 2026-05-19 01:52:14 -05:00
Allaun Silverfox
ca4371d9ff Add adversarial duals 16D anchor pack 2026-05-17 15:47:38 -05:00
Allaun Silverfox
8cd71b3532 Add adversarial duals example config 2026-05-17 15:45:57 -05:00
Allaun Silverfox
b480f11c27 Add adversarial duals receipt schema 2026-05-17 15:11:34 -05:00
Allaun Silverfox
5ecce9e794 Add Plasma Chiral Drag Witness example config 2026-05-17 10:14:06 -05:00
Allaun Silverfox
d9563015de Add Plasma Chiral Drag Witness receipt schema 2026-05-17 10:12:58 -05:00
Allaun Silverfox
a8b989ca30 Add BraidStorm Sidon Crossing 16D anchor pack 2026-05-16 20:57:35 -05:00
Allaun Silverfox
2cfb149dbf Add BraidStorm Sidon Crossing example config 2026-05-16 20:56:35 -05:00
Allaun Silverfox
fadc7bf07f Add BraidStorm Sidon Crossing receipt schema 2026-05-16 20:56:00 -05:00
Allaun Silverfox
af612b7d00 Add Golden Braid Centering 16D anchor pack 2026-05-16 20:25:22 -05:00
Allaun Silverfox
d322d49914 Add Golden Braid Centering example config 2026-05-16 20:24:20 -05:00
Allaun Silverfox
747f672d26 Add Golden Braid Centering receipt schema 2026-05-16 20:20:42 -05:00
Allaun Silverfox
cdaf4370bd Add autonomous speedrun 16D anchor pack 2026-05-16 19:16:02 -05:00
Allaun Silverfox
77eda719ae Add autonomous speedrun harness example 2026-05-16 19:12:25 -05:00
Allaun Silverfox
3f7958c502 Add autonomous speedrun harness receipt schema 2026-05-16 19:10:51 -05:00
Allaun Silverfox
a52d281b83 Add MarkovJunior 16D shim example config 2026-05-16 18:47:53 -05:00
Allaun Silverfox
63344019f6 Add MarkovJunior 16D shim receipt schema 2026-05-16 18:45:37 -05:00
Allaun Silverfox
9d3e65c9a7 Add Sidon 16D anchor pack 2026-05-16 17:21:03 -05:00
Allaun Silverfox
c3c8a1d481 Add Sidon FAMM map example config 2026-05-16 17:20:33 -05:00
Allaun Silverfox
a539fdb1d5 Add Sidon FAMM map receipt schema 2026-05-16 17:19:43 -05:00
Allaun Silverfox
bfec63fe15 Add Builder-Judge-Warden Erdos-Szekeres example 2026-05-16 17:06:26 -05:00
Allaun Silverfox
125a768385 Add Builder-Judge-Warden cleanup receipt schema 2026-05-16 17:00:28 -05:00
Allaun Silverfox
b21d2326d7 Add 16D logogram chirality anchor pack 2026-05-16 16:36:53 -05:00
Allaun Silverfox
fe6a58e1ec Add logogram chirality witness example 2026-05-16 16:35:55 -05:00
Allaun Silverfox
8136c8b173 Add logogram chirality witness schema 2026-05-16 16:35:07 -05:00
Allaun Silverfox
9432a113c6 Add NUVMAP Delta-DAG graph coloring example 2026-05-16 16:15:20 -05:00
Allaun Silverfox
864fa9af94 Add NUVMAP Delta-DAG receipt schema 2026-05-16 16:14:43 -05:00
Allaun Silverfox
85caddd1af Add common-noise MFG 16D anchor pack 2026-05-16 15:11:10 -05:00
Allaun Silverfox
1327224837 Add bio-organoid 16D anchor pack 2026-05-16 14:54:17 -05:00