Theory feed: feeder progress toward valence-shell (D127 standing umbrella) #210

Standing umbrella for D127, the owner's doctrine of 2026-09-30:

Theory, type, prover and language repos are feeders of valence-shell. Their progress is judged by what it contributes here, and valence-shell's needs steer their next proofs and engineering, and their direction for the rest of the estate.

Feeders (17, per D127 and D205):

• proof/kernel: januskey, absolute-zero, echidna, tangle
• type theories: echo-types, epistemic-types, secret-types, choreographic-types, residual-evidence-types, tropical-types, nextgen-typing, typell
• languages: ephapax, affinescript, oblibeny
• provers/infra: echidnabot, proof-burrower

Direction doc: docs/THEORY-FEED.adoc, in #211. It gives a per-feeder map of what each feeder proves today, what it feeds valence-shell, the existing and missing links, and its next direction.

Measured baseline (2026-09-30):

• No valence-shell proof file imports any feeder module.
• Every link today is a comment, a doc or ECHIDNA tooling.
• januskey has no link at all.

All labelled feeder issues: issues carrying feeds:valence-shell, a label that is repo-local by D206: search

Next work (from THEORY-FEED)

• NW-1: one filesystem model. Ruled D204:
  • absolute-zero factors out an abstract CNO interface;
  • valence-shell instantiates it, which is the first real feeder import;
  • januskey refines valence-shell's model;
  • see absolute-zero#167, januskey#137 and nextgen-typing#118.
• NW-2: ECHIDNA tri-state verdict plus project context (ECHIDNA pipeline reports 15 known-good proofs "invalid" — provers invoked without project/library context #162, echidna main.rs). Stop reading environment errors as disproofs.
• NW-3: first real echo-types import ([Integration] Ground L3 (reversibility + equivalence + loss) theorems in echo-types LAYER3 module #51). Prerequisites: echo-types#329 (Agda red) and #322 (unpinned agda).
• NW-4: januskey becomes a proof consumer. Replace the placeholder Proofs.idr theorems; its store, log and HMAC design serves B-7.
• NW-5: tropical-types resource bounds for glob and history (Bound recursive glob traversal depth and resource consumption #191, Add configurable operation-history retention and resource bounds #190).
• NW-6: oblibeny as a verified reversible script subset (oblibeny#78).
• NW-7: epistemic receipts for audit-log anchoring (B-7, Add configurable operation-history retention and resource bounds #190, Define and implement history analysis/export subsystem boundary #192).
• NW-8: residual-evidence types for explain and history (Define and implement history analysis/export subsystem boundary #192).
• NW-9: AffineScript primitives for the MCP port. Replace the Deno.affine stub (Deno is banned) with a bun binding; blocked by affinescript#746 (no HMAC).
• NW-10: registry and naming hygiene.
  • Add a valence-shell consumer row in TYPE-CONNECTIONS.
  • Give every frontier item a Feeder: field (D-3).
  • Make echidnabot the D-1 axiom gate.

How progress is judged

A link moves from comment to doc when a bridge doc exists. It moves to mechanised only when a valence-shell proof file imports the feeder module and builds in CI.

Every new feeder issue or PR states Feeds valence-shell: <frontier id | issue | none>.