allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
397 commits 18 branches 0 tags 425 MiB
Commit graph

397 commits

This branch
This branch
All branches
Author SHA1 Message Date
Allaun Silverfox
e19a6a56c7 docs(shim): annotate as legacy shim pending AVM port; add strip receipt metadata 2026-05-26 16:13:43 -05:00
Allaun Silverfox
2609c37c07 feat(avm): add Lean-only strict-typed ISA skeleton (v1) 2026-05-26 16:05:08 -05:00
Allaun Silverfox
8d61cdd482 docs(avm): strengthen float prohibition and documentation requirement 2026-05-26 16:02:05 -05:00
Allaun Silverfox
7e1326e812 docs(avm): add stripping policy and bad-code elimination rules 2026-05-26 15:59:41 -05:00
Allaun Silverfox
5ba91c2a01 docs(avm): redefine AVM as Lean-only ISA with adapter shims/backends 2026-05-26 15:58:25 -05:00
Allaun Silverfox
de2be89666 fix(pist): correct repo root + fail-on-raw-disagreement check 2026-05-26 15:50:29 -05:00
Allaun Silverfox
fd28cace2f docs: add RRC PIST shape-alignment phase 2026-05-26 15:47:19 -05:00
Allaun Silverfox
7d07dd073f feat(pist): add RRC PIST shape-alignment calibration pass 2026-05-26 15:43:45 -05:00
Allaun Silverfox
92fc07f93e archive: remove duplicate PISTMachine search-space copy 2026-05-26 15:42:48 -05:00
Allaun Silverfox
308ce86f27 feat(pist): add RRC PIST validation report cleaner 2026-05-26 15:38:07 -05:00
Allaun Silverfox
689b8130e8 fix(lean): remove stale PISTMachine sorries 2026-05-26 15:31:59 -05:00
Allaun Silverfox
e61e46f9b2 docs: add receipt-density verification sequence 2026-05-26 15:19:07 -05:00
Allaun Silverfox
575b52cb80 feat(pist): add receipt-density sidecar readback validator 2026-05-26 15:18:11 -05:00
Allaun Silverfox
0275b43405 test(pist): add receipt-density injector regression harness 2026-05-26 15:16:40 -05:00
Allaun Silverfox
5033fcac0e feat(pist): use shared rds_connect for receipt-density writer 2026-05-26 15:13:35 -05:00
Brandon Schneider
86f8ff0b21 chore: remove unused import subprocess from v14a (handled by rds_connect) 2026-05-26 15:11:11 -05:00
Brandon Schneider
02f1c928d7 refactor(rds): consolidate 14 psycopg2 connect patterns into shared rds_connect module 
Creates 4-Infrastructure/shim/rds_connect.py with a single connect_rds()
function that resolves connection parameters in priority order:
  1. explicit kwargs
  2. DATABASE_URL env var (postgres://user:pass@host:port/dbname?sslmode=...)
  3. individual RDS_* env vars (RDS_HOST, RDS_PORT, RDS_USER, etc.)
  4. built-in defaults

Auth resolution (when password is empty or RDS_IAM=1):
  1. RDS_IAM_TOKEN env var (pre-computed)
  2. boto3 SDK generate_db_auth_token (preferred)
  3. subprocess aws rds generate-db-auth-token (fallback)
  4. RDS_PASSWORD env var (non-IAM)

Replaces 8 connection pattern variants across 14 active shims:
  - subprocess + RDS_IAM_TOKEN fallback: pist_trace_classify_mcp, joint_classifier,
    pist_prove_and_classify, ingest_57_flexures
  - boto3 SDK: ene_wiki_body_reingest, ene_migrate_and_tag, dataset_ingest_rds
  - subprocess + RDS_PASSWORD: batch_embed_artifacts, sync_wiki_to_rds, seed_flexure_dataset
  - RDS_IAM_AUTH: pist_classify
  - bashrc parsed: credential_loader

v1.4a benchmark confirmed at 100% after refactor.
 2026-05-26 15:09:34 -05:00
Allaun Silverfox
4fccf72456 docs: add PIST receipt-density backfill guide 2026-05-26 14:46:55 -05:00
Allaun Silverfox
bf2748d61e feat(pist): add RRC receipt-density backfill injector 2026-05-26 14:46:13 -05:00
Allaun Silverfox
bfecf99b23 wiki: link PIST route-repair receipt update from home 2026-05-26 14:38:39 -05:00
Allaun Silverfox
b967e504f7 wiki: add PIST route-repair receipt update tiddler 2026-05-26 14:36:34 -05:00
Allaun Silverfox
a9f72e2437 docs: add PIST route-repair and receipt update 2026-05-26 14:36:15 -05:00
Allaun Silverfox
a734bb477b archive: remove duplicate PISTMachine search-space copy 2026-05-26 14:31:44 -05:00
Allaun Silverfox
9c73dc3a7a archive: preserve duplicate PISTMachine search-space copy 2026-05-26 14:30:39 -05:00
Allaun Silverfox
a89c8630fc fix(lean): remove stale PISTMachine sorries 2026-05-26 14:29:04 -05:00
Allaun Silverfox
cc0d9aa49a fix(lean): align SLUQ quaternion theorem with unit witness receipts 2026-05-26 14:25:04 -05:00
Allaun Silverfox
e7009d7fde fix(lean): prove resonance quaternion unit witness preservation 2026-05-26 14:22:00 -05:00
Allaun Silverfox
9b7a90b82e fix(lean): align genomic quaternion theorems with unit receipts 2026-05-26 14:18:28 -05:00
Allaun Silverfox
e53386997c fix(lean): replace quaternion sorries with unit witness receipts 2026-05-26 14:14:31 -05:00
Allaun Silverfox
3112c48daa feat(pist): add genus-0 sphere shell projection demo 2026-05-26 14:10:17 -05:00
Brandon Schneider
6623babbde 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
45b2e9af77 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
60bd39a333 feat(pist): Route-Repair v1.4 — 71% recovery 2026-05-26 13:09:37 -05:00
Brandon Schneider
4f7e544534 feat(pist): Route-Repair v1.3b — multi-step templates, 54% recovery 2026-05-26 12:56:24 -05:00
Brandon Schneider
1cb59dde81 feat(pist): Route-Repair v1.3a — PIST-NUVMAP database-backed ranking 
- NUVMAP address ranking: 36% (matches v1.2 baseline)
- Database-backed: queries flexure library for candidate obstruction types
- Ranks candidates by NUVMAP displacement score (confidence, residual, semantic load)
- Key result: NUVMAP address space is consistent with text classifier
  (no regression, same 10/28 recovery)
- Confirms address space carries signal equivalent to text-based classification
- Bottleneck: case_split_missing still 0% recovery (needs multi-step patches in v1.3b)
- Comparison: v1.1=0% → v1.2=36% → v1.3a=36% (NUVMAP preserves)
 2026-05-26 12:49:29 -05:00
Brandon Schneider
de90ab5579 feat(pist): Route-Repair v1.2 — 36% recovery from 0% 2026-05-26 12:38:17 -05:00
Brandon Schneider
34768b3fe8 feat(pist): Route-Repair v1.1 — 60 failure flexures ingested, obstruction-type voting 2026-05-26 12:17:42 -05:00
Brandon Schneider
e9843fc9ce feat(pist): Route-Repair Loop v1 — 11% recovery rate 2026-05-26 11:38:01 -05:00
Brandon Schneider
f008c13163 feat(pist): routing benchmark — 30% tactic family prediction vs 20% baseline 2026-05-26 11:28:05 -05:00
Brandon Schneider
721a6c620c feat(pist): pist_trace_classify MCP tool — classify proof traces against 57-theorem flexure library 
- MCP server: pist-trace-classify (Python, stdio JSON-RPC)
- Accepts trace_path or inline trace_json
- Computes full v2 spectral features from transition matrix
- Queries ene.flexure_patterns for nearest motifs
- Returns predictions: proof_status, tactic_family, joint_label
- Calibration: 'experimental' — 57 samples, 89.5% LOOCV
- Registered as MCP server in opencode.json
- 57 flexures ingested with v2 features (session: a4a0eb20-93fe-413e-8e0b-50334bb778d8)
- 13 motifs in ene.flexure_patterns
 2026-05-26 11:23:53 -05:00
Brandon Schneider
252a72ff57 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
d99ad55ba6 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
 2026-05-26 11:00:31 -05:00
Brandon Schneider
a44f0f002c feat(pist): joint-based classifier — 84.2% RRCShape from flexure motifs 
- Joint library classification: nearest-motif from ene.flexures
- Leave-one-flexure-out evaluation on 38 joints
- RRCShape: 84.2% (baseline 60.5%) — ★ highest accuracy seen
- Domain: 76.3% (baseline 60.5%)
- Tactic family: 52.6% (baseline 31.6%)
- Joint label: 50.0% (baseline 13.2%, 3.8× baseline)
- Simple 5-dim feature vector + nearest-neighbor
- Story: new proof traces can find similar stored joints and get predictions
 2026-05-26 10:56:01 -05:00
Brandon Schneider
31323b266e 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
0c364d3326 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
fb1025ec8f 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
d86c73b774 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
df3e37d263 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
4d25e6f5ac 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
31890cf3e9 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