Commit graph

409 commits

Author SHA1 Message Date
Allaun Silverfox
93d02caab9 feat(lean): define MCP surface manifest schema for JsonL connector tools 2026-05-26 17:32:55 -05:00
Allaun Silverfox
2c725fb6fd docs: add Lean-first boundary contract (Lean vs shims, receipts, float ban) 2026-05-26 17:31:54 -05:00
Allaun Silverfox
ceb6a91d97 cleanup(ene): load node list from nodes.yaml instead of hardcoded hostnames 2026-05-26 17:16:02 -05:00
Allaun Silverfox
a5a10723ab cleanup(ene): use nodes.yaml inventory instead of hardcoded host resource map 2026-05-26 17:15:50 -05:00
Allaun Silverfox
87e5eb33a7 cleanup(ene): make obsidian shim provenance configurable and schema-complete 2026-05-26 16:54:12 -05:00
Allaun Silverfox
e36cff917b cleanup(ene): make provenance node/tailscale configurable via env vars and CLI arg 2026-05-26 16:42:03 -05:00
Allaun Silverfox
1181849cea cleanup(ene): make provenance node/tailscale configurable via env vars and CLI arg 2026-05-26 16:40:35 -05:00
Allaun Silverfox
d200887e42 cleanup(ene): make provenance node/lake_seed/tailscale_ip configurable via env vars 2026-05-26 16:39:43 -05:00
Allaun Silverfox
c4c50bb78f cleanup(ene): read canonical SQL schema file for chat tables; remove embedded DDL string 2026-05-26 16:34:23 -05:00
Allaun Silverfox
b8cc57943e cleanup(ene): add canonical SQL schema for chat/session sync tables 2026-05-26 16:23:51 -05:00
Allaun Silverfox
e630fd0612 cleanup(ene): remove hardcoded schema path, drop inline schema fallback, add legacy shim strip receipt 2026-05-26 16:22:40 -05:00
Allaun Silverfox
4dbb4121a4 docs(shim): annotate alignment shim as legacy pending AVM port; add strip receipt metadata 2026-05-26 16:14:52 -05:00
Allaun Silverfox
98f5f0e795 docs(shim): annotate as legacy shim pending AVM port; add strip receipt metadata 2026-05-26 16:13:43 -05:00
Allaun Silverfox
a84a704dbf feat(avm): add Lean-only strict-typed ISA skeleton (v1) 2026-05-26 16:05:08 -05:00
Allaun Silverfox
6d73a1b251 docs(avm): strengthen float prohibition and documentation requirement 2026-05-26 16:02:05 -05:00
Allaun Silverfox
1b6f58c5ce docs(avm): add stripping policy and bad-code elimination rules 2026-05-26 15:59:41 -05:00
Allaun Silverfox
3b4ee97588 docs(avm): redefine AVM as Lean-only ISA with adapter shims/backends 2026-05-26 15:58:25 -05:00
Allaun Silverfox
64fee9a863 fix(pist): correct repo root + fail-on-raw-disagreement check 2026-05-26 15:50:29 -05:00
Allaun Silverfox
07c31da663 docs: add RRC PIST shape-alignment phase 2026-05-26 15:47:19 -05:00
Allaun Silverfox
4e91db4052 feat(pist): add RRC PIST shape-alignment calibration pass 2026-05-26 15:43:45 -05:00
Allaun Silverfox
3cd6e1507b archive: remove duplicate PISTMachine search-space copy 2026-05-26 15:42:48 -05:00
Allaun Silverfox
846a2ef241 feat(pist): add RRC PIST validation report cleaner 2026-05-26 15:38:07 -05:00
Allaun Silverfox
3b8f8d2f8c fix(lean): remove stale PISTMachine sorries 2026-05-26 15:31:59 -05:00
Allaun Silverfox
34c82705b5 docs: add receipt-density verification sequence 2026-05-26 15:19:07 -05:00
Allaun Silverfox
2c9e029923 feat(pist): add receipt-density sidecar readback validator 2026-05-26 15:18:11 -05:00
Allaun Silverfox
14aac49e96 test(pist): add receipt-density injector regression harness 2026-05-26 15:16:40 -05:00
Allaun Silverfox
0686b39428 feat(pist): use shared rds_connect for receipt-density writer 2026-05-26 15:13:35 -05:00
Brandon Schneider
fc2ade9681 chore: remove unused import subprocess from v14a (handled by rds_connect) 2026-05-26 15:11:11 -05:00
Brandon Schneider
7eda71868a 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
d18b414ea0 docs: add PIST receipt-density backfill guide 2026-05-26 14:46:55 -05:00
Allaun Silverfox
0409a80929 feat(pist): add RRC receipt-density backfill injector 2026-05-26 14:46:13 -05:00
Allaun Silverfox
11c20c0958 wiki: link PIST route-repair receipt update from home 2026-05-26 14:38:39 -05:00
Allaun Silverfox
d78c792fc7 wiki: add PIST route-repair receipt update tiddler 2026-05-26 14:36:34 -05:00
Allaun Silverfox
c9ff24e5f0 docs: add PIST route-repair and receipt update 2026-05-26 14:36:15 -05:00
Allaun Silverfox
1d0a9dad8f archive: remove duplicate PISTMachine search-space copy 2026-05-26 14:31:44 -05:00
Allaun Silverfox
19c21dbc35 archive: preserve duplicate PISTMachine search-space copy 2026-05-26 14:30:39 -05:00
Allaun Silverfox
088307d997 fix(lean): remove stale PISTMachine sorries 2026-05-26 14:29:04 -05:00
Allaun Silverfox
aeb98c4166 fix(lean): align SLUQ quaternion theorem with unit witness receipts 2026-05-26 14:25:04 -05:00
Allaun Silverfox
d478fae13c fix(lean): prove resonance quaternion unit witness preservation 2026-05-26 14:22:00 -05:00
Allaun Silverfox
a367bc98f5 fix(lean): align genomic quaternion theorems with unit receipts 2026-05-26 14:18:28 -05:00
Allaun Silverfox
26a83bae15 fix(lean): replace quaternion sorries with unit witness receipts 2026-05-26 14:14:31 -05:00
Allaun Silverfox
9629817bb0 feat(pist): add genus-0 sphere shell projection demo 2026-05-26 14:10:17 -05:00
Brandon Schneider
1ff91d138f 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
d6f4df42b5 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
b14c7a924f feat(pist): Route-Repair v1.4 — 71% recovery 2026-05-26 13:09:37 -05:00
Brandon Schneider
77dc9f5361 feat(pist): Route-Repair v1.3b — multi-step templates, 54% recovery 2026-05-26 12:56:24 -05:00
Brandon Schneider
63bdbfa885 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
ffadf92159 feat(pist): Route-Repair v1.2 — 36% recovery from 0% 2026-05-26 12:38:17 -05:00
Brandon Schneider
420bafc0e6 feat(pist): Route-Repair v1.1 — 60 failure flexures ingested, obstruction-type voting 2026-05-26 12:17:42 -05:00
Brandon Schneider
e087aee10c feat(pist): Route-Repair Loop v1 — 11% recovery rate 2026-05-26 11:38:01 -05:00