a11oy.code: full IDE Code tab (streaming chat + CodeMirror editor + sandboxed run + Lambda/Khipu receipts + FAST/HEART/PRIME/FRONTIER tiers); honest-stub until HF_TOKEN set; doctrine sweep (axis rename, role-neutral service names). Built by Perplexity Computer Agent.

a11oy_code_orchestrator.py

@@ -84,13 +84,18 @@ PROVIDER_KEYS = {
     "cerebras": os.environ.get("CEREBRAS_API_KEY", ""),
 }
 
-# Flagship organ base URLs (in-Space these are relative; orchestrator proxies).
+# Governed SZL service-role base URLs (in-Space these are relative; orchestrator
+# proxies). Keys are the honest role names exposed to the model/UI; env-var names
+# are kept internal/legacy for deployment compatibility (never user-visible).
 FLAGSHIP_BASES = {
-    "amaru": os.environ.get("AMARU_BASE", ""),
-    "sentra": os.environ.get("SENTRA_BASE", ""),
-    "rosie": os.environ.get("ROSIE_BASE", ""),
-    "killinchu": os.environ.get("KILLINCHU_BASE", ""),
+    "reasoning": os.environ.get("AMARU_BASE", ""),
+    "policy": os.environ.get("SENTRA_BASE", ""),
+    "operator": os.environ.get("ROSIE_BASE", ""),
+    "field-node": os.environ.get("KILLINCHU_BASE", ""),
 }
+# Accept role aliases used in the tool enum -> canonical FLAGSHIP_BASES key.
+_ROLE_ALIASES = {"governance": "reasoning", "field-node": "field-node",
+                 "policy": "policy", "operator": "operator", "reasoning": "reasoning"}
 
 router = APIRouter(prefix="/api/a11oy/code", tags=["a11oy.code"])
 
@@ -143,15 +148,15 @@ MODEL_CATALOG = [
 ]
 
 DEFAULT_SYSTEM_PROMPT = (
-    "You are a11oy.code, the SZL Holdings conversational orchestrator. You answer "
-    "at the highest available quality (Opus-4.8 target) using a unified open-LLM "
-    "router. You can orchestrate the SZL flagships (Amaru governance, Sentra "
-    "security, Rosie orchestration, Killinchu maritime/drone) and reach outside "
-    "via GitHub, Hugging Face, web search/fetch/browse, a sandboxed shell, and a "
-    "sandboxed filesystem - all of which are exposed to you as tools. Every action "
-    "you take is gated by PURIQ (Yuyay 13-axis wisdom + HUKLLA tripwires) and "
-    "receipted on the Khipu chain. Be precise, cite sources, refuse cleanly when a "
-    "gate denies, and prefer streaming. Never fabricate tool results."
+    "You are a11oy.code, the SZL Holdings conversational coding orchestrator. You "
+    "answer at the highest available quality using a unified open-LLM router. You "
+    "can orchestrate governed SZL services (Governance, Policy, Operator, Field-Node "
+    "roles) and reach outside via GitHub, Hugging Face, web search/fetch/browse, a "
+    "sandboxed shell, and a sandboxed filesystem - all of which are exposed to you "
+    "as tools. Every action you take is gated by PURIQ (Yuyay 13-axis wisdom + "
+    "HUKLLA tripwires) and receipted on the Khipu chain. Be precise, write clear "
+    "code, cite sources, refuse cleanly when a gate denies, and prefer streaming. "
+    "Never fabricate tool results."
 )
 
 # ---------------------------------------------------------------------------
@@ -258,7 +263,7 @@ def _hukla_check(action: str, context: dict[str, Any]) -> tuple[int, list[str],
     if not context.get("chain_verified", True):
         fired.append("T01")
         hard_halt = True
-    # T05 PII (very rough heuristic; real PII filter is sentra's job)
+    # T05 PII (very rough heuristic; the dedicated egress/immune filter owns full PII)
     if re.search(r"\b\d{3}-\d{2}-\d{4}\b", text):
         fired.append("T05")
     # T06 cost ceiling
@@ -440,6 +445,34 @@ def _inference_headers() -> dict[str, str]:
     return {"Authorization": f"Bearer {HF_TOKEN}", "Content-Type": "application/json"}
 
 
+def has_inference_credential() -> bool:
+    """True iff a real inference credential is present (HF router or a provider key)."""
+    return bool(HF_TOKEN) or any(PROVIDER_KEYS.values())
+
+
+def honest_stub_text(user_msg: str, decision: dict[str, Any]) -> str:
+    """Deterministic, CLEARLY-LABELED stub. NEVER a fabricated model answer.
+
+    Emitted only when NO inference credential is present. It states plainly that
+    the model text is unavailable and that routing / Lambda / receipts are the
+    real, deterministic parts. It does NOT invent a code answer.
+    """
+    snippet = (user_msg or "").strip().replace("\n", " ")[:160]
+    return (
+        "**[deterministic stub \u2014 inference token not yet set]**\n\n"
+        "a11oy.code received your request"
+        + (f" (\u201c{snippet}\u201d)" if snippet else "")
+        + f" and routed it to tier **{decision.get('tier')}** \u2192 model "
+        f"`{decision.get('model')}` (license {decision.get('license_class')}). "
+        "The PURIQ \u039b-gate, tier selection and the signed Khipu receipt below are "
+        "REAL deterministic math. The **model completion itself is unavailable** because no "
+        "inference credential is configured on this Space \u2014 so no answer is fabricated "
+        "(Zero-Bandaid Law).\n\n"
+        "_To enable live generation, paste a valid token into the Space secret_ `HF_TOKEN` "
+        "_(Settings \u2192 Variables and secrets). Generation then goes live instantly \u2014 no redeploy._"
+    )
+
+
 async def _call_model_stream(client: httpx.AsyncClient, model: str, payload: dict[str, Any]
                              ) -> AsyncGenerator[bytes, None]:
     body = dict(payload)
@@ -521,9 +554,9 @@ TOOL_SCHEMAS = [
         "name": "hf_read_space", "description": "List files / read metadata of a Hugging Face Space.",
         "parameters": {"type": "object", "properties": {"repo_id": {"type": "string"}}, "required": ["repo_id"]}}},
     {"type": "function", "function": {
-        "name": "flagship_call", "description": "Call an SZL flagship endpoint (amaru/sentra/rosie/killinchu).",
+        "name": "flagship_call", "description": "Call a governed SZL service role (governance/policy/operator/field-node).",
         "parameters": {"type": "object", "properties": {
-            "organ": {"type": "string", "enum": ["amaru", "sentra", "rosie", "killinchu"]},
+            "organ": {"type": "string", "enum": ["governance", "policy", "operator", "field-node"]},
             "path": {"type": "string"}, "method": {"type": "string", "default": "GET"},
             "json": {"type": "object"}}, "required": ["organ", "path"]}}},
     {"type": "function", "function": {
@@ -545,6 +578,71 @@ TOOL_SCHEMAS = [
 
 SHELL_ALLOWLIST = {"ls", "cat", "echo", "wc", "head", "tail", "grep", "find", "python3", "node", "sort", "uniq"}
 
+# ---------------------------------------------------------------------------
+# Sandboxed code runner for the IDE "Run" button. HONEST safety boundary:
+#  - only python3 / node interpreters (no arbitrary binaries)
+#  - executed inside SANDBOX_DIR with a minimal PATH, NO network reachability is
+#    promised (the Space process MAY have egress; we do NOT sandbox the network
+#    at the kernel level here, so we LABEL that honestly rather than claim it)
+#  - 8s wall-clock timeout, output truncated
+# This is a constrained-interpreter runner, NOT a hardened multi-tenant jail.
+# The label returned to the UI states the boundary plainly (no fake claims).
+# ---------------------------------------------------------------------------
+RUN_INTERPRETERS = {
+    "python": ["python3", "-I", "-S"],   # -I isolated, -S no site
+    "javascript": ["node"],
+    "shell": None,   # shell handled via the allow-listed _tool_shell path only
+}
+RUN_BOUNDARY = (
+    "sandbox: isolated dir + 8s timeout + interpreter-only (python3/node). "
+    "Network is NOT kernel-isolated in this Space \u2014 do not run untrusted code "
+    "expecting egress containment. Honest boundary, not a hardened jail."
+)
+
+
+def run_code(language: str, code: str) -> dict[str, Any]:
+    """Execute editor code in the constrained sandbox. Returns stdout/stderr/code.
+    NO fake run: if the language is unsupported we say so honestly."""
+    SANDBOX_DIR.mkdir(parents=True, exist_ok=True)
+    lang = (language or "python").lower()
+    if lang in ("text/x-csrc", "c"):
+        return {"error": "C execution is not enabled in this sandbox (no compiler in image). "
+                         "Honest limitation \u2014 Python and JavaScript run live.",
+                "boundary": RUN_BOUNDARY, "code": None}
+    if lang == "shell":
+        return {"error": "Shell is restricted to the allow-listed shell_exec tool, not the Run button.",
+                "boundary": RUN_BOUNDARY, "code": None}
+    interp = RUN_INTERPRETERS.get(lang)
+    if not interp:
+        return {"error": f"unsupported language '{language}'", "boundary": RUN_BOUNDARY, "code": None}
+    suffix = {"python": ".py", "javascript": ".js"}[lang]
+    src = SANDBOX_DIR / f"_run_{uuid.uuid4().hex[:8]}{suffix}"
+    try:
+        src.write_text(code, "utf-8")
+        t0 = time.time()
+        out = subprocess.run(
+            [*interp, str(src)], capture_output=True, text=True, timeout=8,
+            cwd=str(SANDBOX_DIR),
+            env={"PATH": os.environ.get("PATH", "/usr/bin:/bin"), "HOME": str(SANDBOX_DIR),
+                 "PYTHONIOENCODING": "utf-8"},
+        )
+        elapsed = int((time.time() - t0) * 1000)
+        rec = khipu_emit("code.run", {"language": lang, "bytes": len(code), "exit": out.returncode})
+        return {"stdout": out.stdout[:8000], "stderr": out.stderr[:4000], "code": out.returncode,
+                "elapsed_ms": elapsed, "boundary": RUN_BOUNDARY,
+                "khipu_hash": rec["hash"]}
+    except subprocess.TimeoutExpired:
+        return {"error": "timeout (8s wall-clock)", "boundary": RUN_BOUNDARY, "code": 124}
+    except FileNotFoundError as exc:
+        return {"error": f"interpreter not available in image: {exc}", "boundary": RUN_BOUNDARY, "code": None}
+    except Exception as exc:
+        return {"error": str(exc)[:400], "boundary": RUN_BOUNDARY, "code": None}
+    finally:
+        try:
+            src.unlink(missing_ok=True)
+        except Exception:
+            pass
+
 
 def _gate_context_for_tool(name: str, args: dict[str, Any], attested: bool) -> dict[str, Any]:
     risk = "high" if name in STATE_CHANGING_TOOLS else "low"
@@ -598,7 +696,7 @@ async def _dispatch_tool(name: str, args: dict[str, Any], client: httpx.AsyncCli
     if name == "fs_write":
         return _tool_fs_write(args["path"], args["content"])
     if name == "drone_command":
-        return await _tool_flagship(client, "killinchu", f"/drones/{args['drone_id']}/command",
+        return await _tool_flagship(client, "field-node", f"/drones/{args['drone_id']}/command",
                                     "POST", {"command": args["command"]})
     raise ValueError(f"unknown tool {name}")
 
@@ -644,10 +742,11 @@ def _tool_hf_space(repo_id: str) -> Any:
 
 
 async def _tool_flagship(client: httpx.AsyncClient, organ: str, path: str, method: str, payload: Any) -> Any:
-    base = FLAGSHIP_BASES.get(organ, "")
+    role = _ROLE_ALIASES.get(organ, organ)
+    base = FLAGSHIP_BASES.get(role, "")
     if not base:
-        return {"error": f"flagship '{organ}' base URL not configured",
-                "hint": f"set {organ.upper()}_BASE env when the {organ} Space ships.",
+        return {"error": f"service role '{role}' base URL not configured",
+                "hint": f"configure the '{role}' service base when that Space ships.",
                 "gap": True}
     resp = await client.request(method, f"{base}{path}", json=payload, timeout=60.0)
     try:
@@ -830,9 +929,12 @@ def _get_client() -> httpx.AsyncClient:
 async def code_healthz() -> JSONResponse:
     return JSONResponse({
         "status": "ok", "component": "a11oy.code orchestrator", "doctrine": "v12 (v11+PURIQ)",
-        "inference": "hf-router" if HF_TOKEN else "NO-CREDENTIAL",
+        "inference": "hf-router" if has_inference_credential() else "NO-CREDENTIAL",
+        "mode": "live" if has_inference_credential() else "deterministic_stub",
         "tiers": list(TIERS.keys()), "tools": [t["function"]["name"] for t in TOOL_SCHEMAS],
         "puriq_threshold": PURIQ_THRESHOLD, "memory": "sqlite", "signed": "Yachay",
+        "ide": "/api/a11oy/code/ide", "run": "/api/a11oy/code/run",
+        "token_secret": "HF_TOKEN",
         "built_by": "Perplexity Computer Agent",
     })
 
@@ -853,6 +955,49 @@ async def code_metrics() -> PlainTextResponse:
     return PlainTextResponse(_metrics_text(), media_type="text/plain; version=0.0.4")
 
 
+# ---------------------------------------------------------------------------
+# IDE page (full-screen coding assistant). Self-contained HTML with vendored
+# CodeMirror (0 runtime CDN). Served from a sibling file so it can be edited
+# without touching this module.
+# ---------------------------------------------------------------------------
+_IDE_HTML_PATH = Path(__file__).with_name("a11oy_code_ide.html")
+
+
+@router.get("/ide")
+async def code_ide():
+    """Serve the full IDE-style Code tab page (streaming chat + editor + run +
+    receipts). 0 runtime CDN \u2014 all assets inlined."""
+    try:
+        html = _IDE_HTML_PATH.read_text("utf-8")
+    except Exception as exc:  # honest failure, never a fake page
+        return PlainTextResponse(
+            f"a11oy.code IDE page not found on this Space ({exc}). "
+            "The orchestrator API is live at /api/a11oy/code/* regardless.",
+            status_code=404)
+    from fastapi.responses import HTMLResponse
+    return HTMLResponse(html)
+
+
+@router.post("/run")
+async def code_run(request: Request) -> JSONResponse:
+    """Execute editor code in the constrained sandbox. Honest safety boundary is
+    returned in the response (see RUN_BOUNDARY). PURIQ-gated + Khipu-receipted."""
+    body = await request.json()
+    language = body.get("language", "python")
+    code = body.get("code", "")
+    if not isinstance(code, str) or not code.strip():
+        return JSONResponse({"error": "empty code", "boundary": RUN_BOUNDARY, "code": None})
+    # Gate the run as a sandboxed exec action.
+    gate = puriq_decide("shell_exec", _gate_context_for_tool("shell_exec", {"run": language}, attested=True))
+    if not gate["allow"]:
+        _METRICS["gate_denied_total"] += 1
+        return JSONResponse({"error": f"PURIQ gate denied: {gate['reason']}",
+                             "boundary": RUN_BOUNDARY, "code": None})
+    result = await asyncio.get_event_loop().run_in_executor(None, run_code, language, code)
+    result["gate"] = {"allow": gate["allow"], "score": gate["score"], "lambda": gate["lambda"]}
+    return JSONResponse(result)
+
+
 @router.post("/v1/router")
 async def v1_router(request: Request) -> JSONResponse:
     """7-tier router. Returns OpenAI-compatible response + Khipu receipt."""
@@ -1028,6 +1173,34 @@ async def chat_stream(request: Request):
                             "model": decision["model"], "license_class": decision["license_class"],
                             "reason": decision["reason"]})
         t0 = time.time()
+
+        # ----------------------------------------------------------------
+        # HONEST-STUB BRANCH: if there is NO inference credential, do NOT
+        # error out and do NOT fabricate. Stream a clearly-labeled stub plus
+        # the real signed receipt, then finish cleanly. This keeps the tab
+        # fully operational (routing + Lambda + receipt) while being honest
+        # that the model text is unavailable until a token is pasted.
+        # ----------------------------------------------------------------
+        if not has_inference_credential():
+            stub = honest_stub_text(user_msg, decision)
+            for word in re.findall(r"\S+\s*", stub):
+                yield sse("token", {"text": word})
+                await asyncio.sleep(0)
+            latency_ms = int((time.time() - t0) * 1000)
+            y13 = yuyay13_response_score(stub, None, latency_ms)
+            rec = khipu_emit("chat.completion.stub", {
+                "conversation_id": conv_id, "model": decision["model"],
+                "tier": decision["tier"], "mode": "deterministic_stub", "yuyay13": y13})
+            mem_add_message(conv_id, "assistant", stub, model=decision["model"],
+                            tier=decision["tier"], latency_ms=latency_ms, cost_usd=0.0,
+                            yuyay13=y13, khipu_hash=rec["hash"])
+            yield sse("done", {"conversation_id": conv_id, "tier": decision["tier"],
+                               "model": decision["model"], "license_class": decision["license_class"],
+                               "latency_ms": latency_ms, "cost_usd": 0.0, "yuyay13": y13,
+                               "khipu_hash": rec["hash"], "chain_verified": True,
+                               "mode": "deterministic_stub"})
+            return
+
         payload = {"messages": history, "max_tokens": body.get("max_tokens", 1500),
                    "temperature": body.get("temperature", 0.7)}
         if enable_tools:

a11oy_v4_formulas.py

@@ -623,7 +623,7 @@ _LIVE = {
 _REGISTRY: List[Dict[str, Any]] = [
     # ---- 5 LIVE ----
     {"name": "AdversarialRobustness", "id": "TH8", "leanTheorem": "robustness_preserved_by_composition",
-     "leanFile": "Lutar/Composition/AdversarialRobustness.lean", "leanStatus": "conjecture-open", "axis": "SENTRA",
+     "leanFile": "Lutar/Composition/AdversarialRobustness.lean", "leanStatus": "conjecture-open", "axis": "CHAPAQ",
      "severity": "enforced", "gates": "Allows pipeline deploy only when composed perturbation ε₂=L₁·L₂·δ ≤ maxEpsilon.",
      "status": "live", "ts": "packages/policy/src/gates/adversarialRobustness_gate.ts",
      "sample": {"lipschitz1": 0.8, "lipschitz2": 0.9, "delta": 0.5}, "config": {"maxEpsilon": 1.0}},
@@ -648,35 +648,35 @@ _REGISTRY: List[Dict[str, Any]] = [
      "status": "live", "ts": "packages/policy/src/gates/summationInvariant_gate.ts",
      "sample": {"khipuId": "k1", "organs": [{"organId": "o1", "decisions": [{"decisionId": "d1", "value": 3}, {"decisionId": "d2", "value": 4}]}], "primaryCord": 7}, "config": {}},
     # ---- 10 MORE LIVE (Phase 3, ported below) are interleaved by id; remaining 20 ts-only ----
-    {"name": "SoundnessAxiom", "id": "A1", "leanTheorem": "soundness_axiom", "leanFile": "Lutar/Gate/SoundnessAxiom.lean", "leanStatus": "theorem", "axis": "AMARU_CORTEX", "severity": "enforced", "gates": "Gate composition soundness floor.", "status": "ts-only", "ts": "packages/policy/src/gates/soundnessAxiom_gate.ts"},
+    {"name": "SoundnessAxiom", "id": "A1", "leanTheorem": "soundness_axiom", "leanFile": "Lutar/Gate/SoundnessAxiom.lean", "leanStatus": "theorem", "axis": "YACHAY", "severity": "enforced", "gates": "Gate composition soundness floor.", "status": "ts-only", "ts": "packages/policy/src/gates/soundnessAxiom_gate.ts"},
     {"name": "MoralGroundingFloor", "id": "A2", "leanTheorem": "moral_grounding_floor", "leanFile": "Lutar/Gate/MoralGrounding.lean", "leanStatus": "theorem", "axis": "YUYAY", "severity": "enforced", "gates": "Action must clear moral grounding floor.", "status": "ts-only", "ts": "packages/policy/src/gates/moralGroundingFloor_gate.ts"},
     {"name": "MeasurabilityHonestyFloor", "id": "A3", "leanTheorem": "measurability_honesty_floor", "leanFile": "Lutar/Gate/MeasurabilityHonesty.lean", "leanStatus": "theorem", "axis": "YUYAY", "severity": "enforced", "gates": "Claims must be measurable / honest.", "status": "ts-only", "ts": "packages/policy/src/gates/measurabilityHonestyFloor_gate.ts"},
     {"name": "DualWitnessDisjointness", "id": "A4", "leanTheorem": "dualWitnessDisjointness", "leanFile": "Lutar/Gate/DualWitness.lean", "leanStatus": "theorem", "axis": "YAWAR", "severity": "enforced", "gates": "Allows \u03c1-closure write only when witness_1_id \u2260 witness_2_id (two independent witnesses, no single-witness collapse).", "status": "live", "ts": "packages/policy/src/gates/dualWitnessDisjointness_gate.ts", "sample": {"witness1Id": "alice", "witness2Id": "bob"}, "config": {}},
     {"name": "DeterministicReplay", "id": "A5", "leanTheorem": "deterministicReplay", "leanFile": "Lutar/Gate/DeterministicReplay.lean", "leanStatus": "theorem", "axis": "UNAY", "severity": "enforced", "gates": "Allows production op only when N replay runs yield exactly 1 unique (byte-identical) Merkle root.", "status": "live", "ts": "packages/policy/src/gates/deterministicReplay_gate.ts", "sample": {"replayRoots": ["abc123deadbeef00", "abc123deadbeef00", "abc123deadbeef00", "abc123deadbeef00", "abc123deadbeef00"]}, "config": {"requiredRuns": 5}},
     {"name": "HashChainIntegrity", "id": "A6", "leanTheorem": "hashChainIntegrity", "leanFile": "Lutar/Gate/HashChainIntegrity.lean", "leanStatus": "theorem", "axis": "YAWAR", "severity": "enforced", "gates": "Allows chain advancement only when every entry.chainHash == SHA256(JSON of previous entry) \u2014 Khipu chain continuity.", "status": "live", "ts": "packages/policy/src/gates/hashChainIntegrity_gate.ts", "sample": {"entries": [{"entryId": "e0", "payload": "genesis", "chainHash": "genesis"}, {"entryId": "e1", "payload": "second", "chainHash": "45bd824b7e4aadbb7ea4a865d057e4cd832d718a268169680f898274b89c5a8d"}, {"entryId": "e2", "payload": "third", "chainHash": "ae7da7c40007478c3e412457553c0aa235a1804ec65f446e1b2d472548ca50d9"}]}, "config": {}},
-    {"name": "BekensteinBound", "id": "A7", "leanTheorem": "bekenstein_bound", "leanFile": "Lutar/Gate/BekensteinBound.lean", "leanStatus": "conjectured", "axis": "SENTRA", "severity": "advisory", "gates": "Advisory (STAGED): entropy/information bound.", "status": "ts-only", "ts": "packages/policy/src/gates/bekensteinBound_gate.ts"},
-    {"name": "IngestDiscipline", "id": "A8", "leanTheorem": "ingest_discipline", "leanFile": "Lutar/Gate/IngestDiscipline.lean", "leanStatus": "theorem", "axis": "SENTRA", "severity": "enforced", "gates": "Ingest must follow discipline schema.", "status": "ts-only", "ts": "packages/policy/src/gates/ingestDiscipline_gate.ts"},
-    {"name": "DoctrineCompleteness", "id": "A9", "leanTheorem": "doctrineCompleteness", "leanFile": "Lutar/Gate/DoctrineCompleteness.lean", "leanStatus": "theorem", "axis": "AMARU_CORTEX", "severity": "enforced", "gates": "Allows artifact only when SHA-256(doctrine.json) == canonical AND all 8 forbidden patterns enumerated (doctrine-check.sh parity).", "status": "live", "ts": "packages/policy/src/gates/doctrineCompleteness_gate.ts", "sample": {"doctrineJsonRaw": "{\"version\":\"1.0.0\",\"patterns\":[\"FP\",\"FP\",\"FP\",\"FP\",\"FP\",\"FP\",\"FP\",\"FP\"]}", "detectedPatterns": ["FP", "FP", "FP", "FP", "FP", "FP", "FP", "FP"]}, "config": {"canonicalSha256": "1ebcac54bde49c4062648d0e9757a4364858d6826b60f1f14e79bc1964f1f4fb"}},
+    {"name": "BekensteinBound", "id": "A7", "leanTheorem": "bekenstein_bound", "leanFile": "Lutar/Gate/BekensteinBound.lean", "leanStatus": "conjectured", "axis": "CHAPAQ", "severity": "advisory", "gates": "Advisory (STAGED): entropy/information bound.", "status": "ts-only", "ts": "packages/policy/src/gates/bekensteinBound_gate.ts"},
+    {"name": "IngestDiscipline", "id": "A8", "leanTheorem": "ingest_discipline", "leanFile": "Lutar/Gate/IngestDiscipline.lean", "leanStatus": "theorem", "axis": "CHAPAQ", "severity": "enforced", "gates": "Ingest must follow discipline schema.", "status": "ts-only", "ts": "packages/policy/src/gates/ingestDiscipline_gate.ts"},
+    {"name": "DoctrineCompleteness", "id": "A9", "leanTheorem": "doctrineCompleteness", "leanFile": "Lutar/Gate/DoctrineCompleteness.lean", "leanStatus": "theorem", "axis": "YACHAY", "severity": "enforced", "gates": "Allows artifact only when SHA-256(doctrine.json) == canonical AND all 8 forbidden patterns enumerated (doctrine-check.sh parity).", "status": "live", "ts": "packages/policy/src/gates/doctrineCompleteness_gate.ts", "sample": {"doctrineJsonRaw": "{\"version\":\"1.0.0\",\"patterns\":[\"FP\",\"FP\",\"FP\",\"FP\",\"FP\",\"FP\",\"FP\",\"FP\"]}", "detectedPatterns": ["FP", "FP", "FP", "FP", "FP", "FP", "FP", "FP"]}, "config": {"canonicalSha256": "1ebcac54bde49c4062648d0e9757a4364858d6826b60f1f14e79bc1964f1f4fb"}},
     {"name": "TemporalConsistency", "id": "A10", "leanTheorem": "temporalConsistency", "leanFile": "Lutar/Gate/TemporalConsistency.lean", "leanStatus": "theorem", "axis": "UNAY", "severity": "enforced", "gates": "Allows receipt only when |evalTime \u2212 receiptTime| \u2264 clockDriftBound (verdict invariant under bounded clock drift).", "status": "live", "ts": "packages/policy/src/gates/temporalConsistency_gate.ts", "sample": {"receiptTimestampMs": 1700000000000, "evalTimestampMs": 1700000000500}, "config": {"clockDriftBoundMs": 1000}},
-    {"name": "CausalSeparability", "id": "A11", "leanTheorem": "causal_separability", "leanFile": "Lutar/Gate/CausalSeparability.lean", "leanStatus": "theorem", "axis": "AMARU_CORTEX", "severity": "enforced", "gates": "Causal graph must be separable.", "status": "ts-only", "ts": "packages/policy/src/gates/causalSeparability_gate.ts"},
+    {"name": "CausalSeparability", "id": "A11", "leanTheorem": "causal_separability", "leanFile": "Lutar/Gate/CausalSeparability.lean", "leanStatus": "theorem", "axis": "YACHAY", "severity": "enforced", "gates": "Causal graph must be separable.", "status": "ts-only", "ts": "packages/policy/src/gates/causalSeparability_gate.ts"},
     {"name": "ConstructiveTransparency", "id": "A12", "leanTheorem": "constructive_transparency", "leanFile": "Lutar/Gate/ConstructiveTransparency.lean", "leanStatus": "theorem", "axis": "YUYAY", "severity": "enforced", "gates": "Decisions must be constructively transparent.", "status": "ts-only", "ts": "packages/policy/src/gates/constructiveTransparency_gate.ts"},
     {"name": "EconomicGrounding", "id": "A14", "leanTheorem": "economic_grounding", "leanFile": "Lutar/Gate/EconomicGrounding.lean", "leanStatus": "theorem", "axis": "KALLPA", "severity": "enforced", "gates": "Action must be economically grounded (cost).", "status": "ts-only", "ts": "packages/policy/src/gates/economicGrounding_gate.ts"},
-    {"name": "RhoClosureComposition", "id": "T1", "leanTheorem": "rho_closure_composition", "leanFile": "Lutar/Gate/RhoClosureComposition.lean", "leanStatus": "theorem", "axis": "AMARU_CORTEX", "severity": "enforced", "gates": "ρ-closure composes under pipeline.", "status": "ts-only", "ts": "packages/policy/src/gates/rhoClosureComposition_gate.ts"},
+    {"name": "RhoClosureComposition", "id": "T1", "leanTheorem": "rho_closure_composition", "leanFile": "Lutar/Gate/RhoClosureComposition.lean", "leanStatus": "theorem", "axis": "YACHAY", "severity": "enforced", "gates": "ρ-closure composes under pipeline.", "status": "ts-only", "ts": "packages/policy/src/gates/rhoClosureComposition_gate.ts"},
     {"name": "LambdaMonotonicity", "id": "T2", "leanTheorem": "lambdaMonotonicity", "leanFile": "Lutar/Gate/LambdaMonotonicity.lean", "leanStatus": "theorem", "axis": "YUYAY", "severity": "enforced", "gates": "Allows evidence augmentation only when every \u039b axis score weakly increases (no decreasing/conflicting axis).", "status": "live", "ts": "packages/policy/src/gates/lambdaMonotonicity_gate.ts", "sample": {"originalScores": [0.9, 0.85], "augmentedScores": [0.95, 0.9]}, "config": {"tolerance": 1e-9}},
     {"name": "MerkleDagBatch", "id": "T3", "leanTheorem": "merkleDagBatch", "leanFile": "Lutar/Gate/MerkleDagBatch.lean", "leanStatus": "theorem", "axis": "YAWAR", "severity": "enforced", "gates": "Allows batch only when (B<minBatch) or build p50 \u2264 maxBuildP50Us \u2014 the O(log B) Merkle-DAG latency bound.", "status": "live", "ts": "packages/policy/src/gates/merkleDagBatch_gate.ts", "sample": {"batchSize": 7, "buildP50Us": 4}, "config": {"maxBuildP50Us": 5, "minBatchSize": 7}},
-    {"name": "BekensteinEntropyMeasure", "id": "T4", "leanTheorem": "bekenstein_entropy_measure", "leanFile": "Lutar/Gate/BekensteinEntropyMeasure.lean", "leanStatus": "conjectured", "axis": "SENTRA", "severity": "enforced", "gates": "Entropy measure ≤ Bekenstein bound.", "status": "ts-only", "ts": "packages/policy/src/gates/bekensteinEntropyMeasure_gate.ts"},
+    {"name": "BekensteinEntropyMeasure", "id": "T4", "leanTheorem": "bekenstein_entropy_measure", "leanFile": "Lutar/Gate/BekensteinEntropyMeasure.lean", "leanStatus": "conjectured", "axis": "CHAPAQ", "severity": "enforced", "gates": "Entropy measure ≤ Bekenstein bound.", "status": "ts-only", "ts": "packages/policy/src/gates/bekensteinEntropyMeasure_gate.ts"},
     {"name": "ReplayDeterminism", "id": "T5", "leanTheorem": "replayDeterminism", "leanFile": "Lutar/Gate/ReplayDeterminism.lean", "leanStatus": "theorem", "axis": "UNAY", "severity": "enforced", "gates": "Allows deploy only when all requiredRuns replay roots equal the pinned canonical Merkle root (Codex-Kernel determinism).", "status": "live", "ts": "packages/policy/src/gates/replayDeterminism_gate.ts", "sample": {"replayRoots": ["1ed4d253cafebabe12345678", "1ed4d253cafebabe12345678", "1ed4d253cafebabe12345678", "1ed4d253cafebabe12345678", "1ed4d253cafebabe12345678"]}, "config": {"canonicalRoot": "1ed4d253cafebabe12345678", "requiredRuns": 5}},
     {"name": "ConjunctiveGateCounterexample", "id": "T6", "leanTheorem": "conjunctive_gate_counterexample", "leanFile": "Lutar/Gate/ConjunctiveGate.lean", "leanStatus": "theorem", "axis": "YUYAY", "severity": "enforced", "gates": "Conjunctive gate counterexample search.", "status": "ts-only", "ts": "packages/policy/src/gates/conjunctiveGateCounterexample_gate.ts"},
-    {"name": "PrivacyMask", "id": "T7", "leanTheorem": "privacy_mask", "leanFile": "Lutar/Gate/PrivacyMask.lean", "leanStatus": "theorem", "axis": "SENTRA", "severity": "enforced", "gates": "PII mask must cover sensitive fields.", "status": "ts-only", "ts": "packages/policy/src/gates/privacyMask_gate.ts"},
+    {"name": "PrivacyMask", "id": "T7", "leanTheorem": "privacy_mask", "leanFile": "Lutar/Gate/PrivacyMask.lean", "leanStatus": "theorem", "axis": "CHAPAQ", "severity": "enforced", "gates": "PII mask must cover sensitive fields.", "status": "ts-only", "ts": "packages/policy/src/gates/privacyMask_gate.ts"},
     {"name": "SingleWitnessExclusion", "id": "T8", "leanTheorem": "singleWitnessExclusion", "leanFile": "Lutar/Gate/SingleWitnessExclusion.lean", "leanStatus": "theorem", "axis": "YAWAR", "severity": "enforced", "gates": "Allows closure only when cross-actor (or same-actor by default) decisions carry \u2265 2 witnesses \u2014 excludes single-witness.", "status": "live", "ts": "packages/policy/src/gates/singleWitnessExclusion_gate.ts", "sample": {"actor1Id": "alice", "actor2Id": "bob", "witnessCount": 2}, "config": {}},
     {"name": "CrossRegionPolicy", "id": "T9", "leanTheorem": "cross_region_policy", "leanFile": "Lutar/Gate/CrossRegionPolicy.lean", "leanStatus": "theorem", "axis": "KALLPA", "severity": "enforced", "gates": "Cross-region data policy enforced.", "status": "ts-only", "ts": "packages/policy/src/gates/crossRegionPolicy_gate.ts"},
-    {"name": "DoctrineEnforcement", "id": "T10", "leanTheorem": "doctrine_enforcement", "leanFile": "Lutar/Gate/DoctrineEnforcement.lean", "leanStatus": "theorem", "axis": "AMARU_CORTEX", "severity": "enforced", "gates": "Doctrine v11 LOCKED enforcement.", "status": "ts-only", "ts": "packages/policy/src/gates/doctrineEnforcement_gate.ts"},
-    {"name": "Composability", "id": "TH1", "leanTheorem": "composability", "leanFile": "Lutar/Composition/Composability.lean", "leanStatus": "theorem", "axis": "AMARU_CORTEX", "severity": "enforced", "gates": "Allows A\u2218B cross-system deploy only when doctrine SHAs match, A exit floor \u2264 B entry floor, and A2A headers present.", "status": "live", "ts": "packages/policy/src/gates/composability_gate.ts", "sample": {"doctrineShaA": "abc123sha256", "doctrineShaB": "abc123sha256", "aExitFloor": 0.9, "bEntryFloor": 0.92, "hasA2AHeaders": True}, "config": {}},
+    {"name": "DoctrineEnforcement", "id": "T10", "leanTheorem": "doctrine_enforcement", "leanFile": "Lutar/Gate/DoctrineEnforcement.lean", "leanStatus": "theorem", "axis": "YACHAY", "severity": "enforced", "gates": "Doctrine v11 LOCKED enforcement.", "status": "ts-only", "ts": "packages/policy/src/gates/doctrineEnforcement_gate.ts"},
+    {"name": "Composability", "id": "TH1", "leanTheorem": "composability", "leanFile": "Lutar/Composition/Composability.lean", "leanStatus": "theorem", "axis": "YACHAY", "severity": "enforced", "gates": "Allows A\u2218B cross-system deploy only when doctrine SHAs match, A exit floor \u2264 B entry floor, and A2A headers present.", "status": "live", "ts": "packages/policy/src/gates/composability_gate.ts", "sample": {"doctrineShaA": "abc123sha256", "doctrineShaB": "abc123sha256", "aExitFloor": 0.9, "bEntryFloor": 0.92, "hasA2AHeaders": True}, "config": {}},
     {"name": "ReplayDoiDuality", "id": "TH2", "leanTheorem": "replay_doi_duality", "leanFile": "Lutar/Composition/ReplayDoiDuality.lean", "leanStatus": "theorem", "axis": "UNAY", "severity": "enforced", "gates": "Replay ↔ DOI duality holds.", "status": "ts-only", "ts": "packages/policy/src/gates/replayDoiDuality_gate.ts"},
-    {"name": "AnatomyReduction", "id": "TH3", "leanTheorem": "anatomy_reduction", "leanFile": "Lutar/Composition/AnatomyReduction.lean", "leanStatus": "theorem", "axis": "AMARU_CORTEX", "severity": "enforced", "gates": "7-organ anatomy reduces correctly.", "status": "ts-only", "ts": "packages/policy/src/gates/anatomyReduction_gate.ts"},
+    {"name": "AnatomyReduction", "id": "TH3", "leanTheorem": "anatomy_reduction", "leanFile": "Lutar/Composition/AnatomyReduction.lean", "leanStatus": "theorem", "axis": "YACHAY", "severity": "enforced", "gates": "7-organ anatomy reduces correctly.", "status": "ts-only", "ts": "packages/policy/src/gates/anatomyReduction_gate.ts"},
     {"name": "LambdaCategoryComposability", "id": "TH4", "leanTheorem": "lambda_category_composability", "leanFile": "Lutar/LaxFunctor.lean", "leanStatus": "conjectured", "axis": "YUYAY", "severity": "advisory", "gates": "Advisory (STAGED): Λ lax-functor composition.", "status": "ts-only", "ts": "packages/policy/src/gates/lambdaCategoryComposability_gate.ts"},
     {"name": "ReceiptChainConfluence", "id": "TH5", "leanTheorem": "receipt_chain_confluence", "leanFile": "Lutar/Composition/ReceiptChainConfluence.lean", "leanStatus": "conjectured", "axis": "YAWAR", "severity": "enforced", "gates": "Receipt chain confluent under merge.", "status": "ts-only", "ts": "packages/policy/src/gates/receiptChainConfluence_gate.ts"},
-    {"name": "BekensteinEntropyDpi", "id": "TH6", "leanTheorem": "bekenstein_entropy_dpi", "leanFile": "Lutar/EntropyBound.lean", "leanStatus": "theorem", "axis": "SENTRA", "severity": "enforced", "gates": "DPI entropy bound (discharges A7 formally).", "status": "ts-only", "ts": "packages/policy/src/gates/bekensteinEntropyDpi_gate.ts"},
+    {"name": "BekensteinEntropyDpi", "id": "TH6", "leanTheorem": "bekenstein_entropy_dpi", "leanFile": "Lutar/EntropyBound.lean", "leanStatus": "theorem", "axis": "CHAPAQ", "severity": "enforced", "gates": "DPI entropy bound (discharges A7 formally).", "status": "ts-only", "ts": "packages/policy/src/gates/bekensteinEntropyDpi_gate.ts"},
     {"name": "CurryHowardReceiptCalculus", "id": "TH7", "leanTheorem": "curry_howard_receipt_calculus", "leanFile": "Lutar/CurryHoward.lean", "leanStatus": "theorem", "axis": "YAWAR", "severity": "enforced", "gates": "Receipt calculus = proof terms (Curry-Howard).", "status": "ts-only", "ts": "packages/policy/src/gates/curryHowardReceiptCalculus_gate.ts"},
     # ---- Hickok cognitive-neuroscience ingest (A36/A37/A38) ----
     # Axis `Hickok`. All ts-only (honest): the Lean anchor files carry `sorry`
@@ -696,8 +696,8 @@ _REGISTRY: List[Dict[str, Any]] = [
 _SUPPLEMENTARY: List[Dict[str, Any]] = [
     {"name": "LambdaUniquenessConjecture", "id": "TH_L1", "leanTheorem": "lambdaUniquenessConjecture", "leanFile": "Lutar/Uniqueness.lean", "leanStatus": "conjecture", "axis": "YUYAY", "severity": "advisory-conjecture", "gates": "Lambda fixed-point uniqueness, Conjecture 1 (2 sorry in wider repo; NOT a theorem — Doctrine v11 LOCKED).", "status": "ts-only", "ts": "packages/policy/src/gates/lambdaUniquenessConjecture_gate.ts", "is_conjecture": True, "proven": False, "lambda_statement": "Conjecture 1 (NOT a theorem — LOCKED)"},
     {"name": "LambdaMinMaxBounds", "id": "TH_L2", "leanTheorem": "lambda_min_max_bounds", "leanFile": "Lutar/Bound.lean", "leanStatus": "theorem", "axis": "YUYAY", "severity": "enforced", "gates": "Λ score min/max bounds (2 sorry in wider repo).", "status": "ts-only", "ts": "packages/policy/src/gates/lambdaMinMaxBounds_gate.ts"},
-    {"name": "BekensteinSoundness", "id": "TH_L3", "leanTheorem": "bekenstein_soundness", "leanFile": "Lutar/BekensteinSoundness.lean", "leanStatus": "measured/conjectured", "axis": "SENTRA", "severity": "advisory", "gates": "Advisory (STAGED): Bekenstein soundness.", "status": "ts-only", "ts": "packages/policy/src/gates/bekensteinSoundness_gate.ts"},
-    {"name": "RhoClosureProduction", "id": "TH_L4", "leanTheorem": "rho_closure_production", "leanFile": "Lutar/RhoClosureProduction.lean", "leanStatus": "measured", "axis": "AMARU_CORTEX", "severity": "enforced", "gates": "ρ-closure measured in production.", "status": "ts-only", "ts": "packages/policy/src/gates/rhoClosureProduction_gate.ts"},
+    {"name": "BekensteinSoundness", "id": "TH_L3", "leanTheorem": "bekenstein_soundness", "leanFile": "Lutar/BekensteinSoundness.lean", "leanStatus": "measured/conjectured", "axis": "CHAPAQ", "severity": "advisory", "gates": "Advisory (STAGED): Bekenstein soundness.", "status": "ts-only", "ts": "packages/policy/src/gates/bekensteinSoundness_gate.ts"},
+    {"name": "RhoClosureProduction", "id": "TH_L4", "leanTheorem": "rho_closure_production", "leanFile": "Lutar/RhoClosureProduction.lean", "leanStatus": "measured", "axis": "YACHAY", "severity": "enforced", "gates": "ρ-closure measured in production.", "status": "ts-only", "ts": "packages/policy/src/gates/rhoClosureProduction_gate.ts"},
 ]
 
 # Canonical 35 anchor formulas (_REGISTRY) are what GET /formulas returns and what