allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-30 18:56:16 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions 1
Research-Stack/6-Documentation/docs/RESEARCH_EXECUTION_PLAN_2026-06-10.md
allaun 475f6319ea chore(repo): push local 768-commit branch state onto clean remote baseline 
This squashes all local history (768 commits) onto the scrubbed PR #90
baseline. Individual commits were lost during filter-repo corruption;
the working tree content is preserved intact.

Build: N/A (working tree state only)
2026-06-15 22:46:50 -05:00

9.1 KiB
Raw Permalink Blame History

Research Execution Plan — 2026-06-10

Status: EXECUTION_PLAN_ACTIVE Rule: every goal below has a receipt-shaped success criterion. A goal without its receipt is not done, regardless of how much work happened near it. Companion docs: erdos329-synthesis-program-2026-06-10.md (Track C rationale), NUTBREAKER_*.md ×4 in this directory (Track B payloads), sidon-lifting-relaxation-program.md (guardrails, inherited everywhere).

Track A — Substrate repair (unblocks everything; do first)

A1. cupfox back on the Tailscale mesh

  • Goal: tailscale status on this machine lists cupfox (100.72.130.76) and kubectl get nodes -o wide returns all agents Ready.
  • How: console/physical access to cupfox → check systemctl status tailscaled and tailscale up; if the box is down, boot it. Then from the laptop: kubectl get nodes.
  • Blocks: C1 (Ray jobs), C3, any fabric-tier work.

A2. Fix neon IP drift

  • Goal: no file in distributed-compute-fabric references the stale Tailscale IP 100.100.75.113; verify-internal.sh exits 0.
  • Status: ✅ DONE — 3 files updated (infrastructure-status.md, research plan, SSH config). Live IP 100.92.88.64. MagicDNS name neon-64gb is the durable reference moving forward.

A3. ENE database access from this machine

  • Goal: psql "$DATABASE_URL" -c "select count(*) from <equations table>" returns ~33,890 from the neon-hosted Postgres.
  • Status: ✅ DONE — Postgres 16 running on neon (arxiv-pg container, port 5432). Shared user services, databases created for appflowy, obsidian_sync, ene. DATABASE_URL exported in ~/.bashrc and ~/.config/ene/ene.env. Redis (port 6379) and CouchDB (port 5984) also running on neon for service support.

A4. Relocate singer-theorem-lean out of /tmp

  • Goal: repo lives at a permanent path, builds there (lake build exit 0), ContextStream mapping updated.
  • How: mv /tmp/singer-theorem-lean ~/Projects/singer-theorem-lean (create dir), rebuild, update the pattern in ~/.contextstream/mappings.json (and legacy ~/.contextstream-mappings.json).
  • Risk if skipped: /tmp is wiped on reboot; the public Erdos30 export vanishes.

A5. Session restart to load the MCP stack

  • Goal: in a fresh Claude Code session, /mcp shows contextstream, lean-lsp, nixos, k8s, arxiv all connected and their tools callable.
  • How: restart Claude Code. Nothing else needed; all five are registered at user scope and health-check ✔.

Track B — Formal debt (sorry + axiom elimination)

Fire order is chosen so each success de-risks the next. All prompts are in 6-Documentation/docs/. Verification commands are inside each prompt.

B1. Singer port — fire NUTBREAKER (Singer prompt, already existed)

  • Goal: SidonSets.lean:738 sorry closed; lake build 0 errors; grep -n sorry Semantics/SidonSets.lean empty.
  • Why first: clearest success criteria, upstream reference exists (Erdos30/SingerTheorem.lean), and C2 consumes the result.

B2. SSMS — fire NUTBREAKER_SSMS_PROMPT.md

  • Goal: ssms_step_nonexpansive + ssms_contraction_theorem proven; no sorry in SSMS.lean; Compiler + full build at baseline.

B3. AdjugateMatrix — fire NUTBREAKER_ADJUGATE_MATRIX_PROMPT.md

  • Goal: cofactor_identity closed OR formally classified (exactness hypotheses added, epistemic branch documented). Both outcomes are receipts.

B4. BraidSpherionBridge — fire NUTBREAKER_BRAID_SPHERION_BRIDGE_PROMPT.md

  • Goal: all 9 drift-repair sorries closed, zero new axioms.

B5. Burgers bridge — fire NUTBREAKER_BURGERS_BRIDGE_PROMPT.md

  • Goal: burgersToBraidDef constructive def + shim-replay witness + energy/mass correspondence lemmas on a stated domain; bare-axiom uses contained. Step-correspondence level (exact / bounded-error / witnessed conjecture) explicitly reported.

B6. Axiom census receipt (cheap, high leverage — can run today)

  • Goal: AGENTS.md gains a standing "Axiom Census" table: per-module axiom count + one-line justification status; regenerating it is part of the post-interaction workflow.
  • How: grep -rn '^axiom\|^\s*axiom ' Semantics/Semantics/*.lean Semantics/Semantics/**/*.lean | sort → table. Add the regeneration command to the workflow section.
  • Why: converts the "746 verified modules" claim from vulnerable to audit-proof; the ledger starts pricing axioms the way RRC prices everything.

Failed nutbreaker runs route down-pipeline per the existing tier map: DeepSeek-Prover MCP for lemma-sized fragments, fix-* subagents for context-heavy residue, epistemic blocks to manual decision.

Track C — Erdős #329 attack ladder (from the synthesis doc)

C1. Obstruction mining run on neon (needs A1 or direct neon access + A3)

  • Goal: RRC-tagged receipt rows in the ENE DB for Singer(q) and Bose–Chowla(p,h) witnesses across ≥100 prime powers: collision_count (must be 0), |Forbidden ∩ [1,cN]| for c ∈ {1,2,4,8}, Ω_N, Γ, M_Sidon. Mirror to Garage S3.
  • How: integer-only Python batch (pattern: rrc_ray_tagger.py), Ray over the fabric or run directly on neon. The Γ growth curves decide which family carries the program.

C2. Statement-level interop (needs B1)

  • Goal: LimsupDensityOne in SidonSets.lean matches formal-conjectures/ErdosProblems/329.lean's formulation; finiteWitness_requiresCollisionZero and additiveEmbedding_preservesCollisions proven (both short).
  • How: Tier 2 (DeepSeek-Prover) or in-session with lean-lsp MCP; the second lemma is the parent doc's "additive inclusion creates no slack" warning made permanent.

C3. Evolutionary digit-rule search (needs A1, C1)

  • Goal: first generation of p-adic digit-choice rules evaluated with M_Sidon fitness and collision-zero hard gate; best-of-generation receipts archived; survivor rules converted to native_decide finite certificates.
  • How: AlphaEvolve-shaped loop on the fabric — Hermes/Gemma for mutation volume, Fable for escape moves, neon for audits. Outputs are R_finite + U_asymptotic by construction.

C4. K/M → Forbidden-set formal bridge — promote or refute

  • Goal: a Lean statement transporting the totalKS/kmReflectanceBound residual functional to Forbidden-set counting for one explicit lift family, either proven (subquadratic obstruction bound — major) or refuted (the analogy is formula-shape only — also a receipt, closes S1 as P_analogy).

C5. Nesting theorem attempt on the best C1/C3 family

  • Goal: the actual #329 swing: a compatible-lift-chain theorem for the empirically best family. No deadline; this rung is earned by the others.

Track D — Metamathematical grounding (from the Chaitin discussion)

D1. Mass Numbers ⇄ resource-bounded Kolmogorov complexity

  • Goal: the mass-number doctrine gains a formal-grounding section mapping MassNumber(S,D,C,R) onto resource-bounded K / Levin's Kt, with the decoder-sup trap door named as forbidden; one Lean lemma tying a concrete MassNumber receipt to a decidable resource-bounded bound.
  • How: doc edit in mass_numbers_deanthropocentric_revision.md + small module or extension near MassNumberAdapter.lean.

D2. Weld the trap doors into RRC

  • Goal: RRC_OPERATING_CONTRACT.md gains three explicit QUARANTINE triggers: (1) any claim taking the supremum over all decoders, (2) any claim made from the limit of the certification ladder rather than a stage, (3) any signed incompressibility certificate. W-axis cross-ref to the Turing–Feferman ordinal-logic literature added to the Omega extension doc.
  • Why: the framework currently survives Chaitin by good habits; this makes survival structural.

Track E — External interface

E1. Community-legible Sidon/Singer artifact (needs A4, B1)

  • Goal: singer-theorem-lean (at its permanent home) builds against its pinned mathlib with zero OTOM vocabulary, README maps every theorem to community-standard names, definitions align with 329.lean.
  • Why: first externally verifiable OTOM output; mathlib's difference-set coverage is thin; this is the lineage of Pilatte's frontier method.

E2. Upstream contribution (after E1 stabilizes)

  • Goal: statement-level PR to google-deepmind/formal-conjectures (or lemma-level to mathlib) accepted, or constructive review feedback received.
  • How: start with the 329-adjacent finite lemmas from C2; smallest publishable unit first.

Dependency graph and firing order

Today, no blockers:   B1 → B2/B3/B4 (parallel) → B5, and B6 any time
Needs user input:     A3 (DATABASE_URL), A1 (cupfox physical access)
After A1+A3:          C1 → C3        After B1: C2 → E1 → E2
Independent:          A2, A4, A5, D1, D2
Earned, not scheduled: C4 → C5

Standing rules for every track

  1. Narrow build target before broad; broad before claiming.
  2. A refutation receipt counts as success (C4 explicitly).
  3. No new axioms anywhere except via the documented epistemic branch (B3).
  4. Receipts to ENE DB + Garage when fabric is up; to shared-data/ when not.
  5. Post-interaction workflow (root AGENTS.md) applies to every session.