chore(sync): mirror backend .py + Dockerfile to Space (hf-sync-backend)

Automated backend sync from szl-holdings/a11oy main via hf-sync-backend.
Updated (differed from the Space): Dockerfile, src/a11oy/formulas/allodial.py, src/a11oy/formulas/allodial_gate.py, src/a11oy/formulas/entanglement.py, szl_dark_surfaces_register.py
Deleted (gone from the repo + Dockerfile COPY set): (none)

Keeps the Space-built backend (serve.py + the Dockerfile-COPY'd .py
modules) identical to GitHub main so the Space never rebuilds from a
stale backend, new endpoints don't 404 there, and orphaned modules
removed from the repo don't linger in the Space tree.

Dockerfile

@@ -338,6 +338,16 @@ COPY src/a11oy/formulas/bloom_filter.py ./src/a11oy/formulas/bloom_filter.py
 COPY src/a11oy/formulas/kalman.py ./src/a11oy/formulas/kalman.py
 COPY src/a11oy/formulas/hnsw_retrieval.py ./src/a11oy/formulas/hnsw_retrieval.py
 COPY src/a11oy/formulas/reidemeister.py ./src/a11oy/formulas/reidemeister.py
+# FIX (formula/* 404 repair): a11oy_formula_endpoints.py imports a11oy.formulas.{allodial,
+# allodial_gate, entanglement} alongside the formulas above, but these three were NEVER
+# COPY'd into the image. The package import therefore raised at boot, register() returned
+# "formulas-unavailable", and EVERY /api/a11oy/v1/formula/* route (sovereign, quorum, holevo,
+# bloom, kalman, formulas/index, …) 404'd through the Node proxy. Per-file COPY (this
+# Dockerfile never uses `COPY . .`). Mirrored byte-identical to the HF Space (hf-sync
+# APP_FILES lockstep). EXPERIMENTAL frontier gates — Λ = Conjecture 1 (never a theorem).
+COPY src/a11oy/formulas/allodial.py ./src/a11oy/formulas/allodial.py
+COPY src/a11oy/formulas/allodial_gate.py ./src/a11oy/formulas/allodial_gate.py
+COPY src/a11oy/formulas/entanglement.py ./src/a11oy/formulas/entanglement.py
 COPY src/a11oy/harvest/__init__.py ./src/a11oy/harvest/__init__.py
 COPY src/a11oy/harvest/wasted_energy_harvest.py ./src/a11oy/harvest/wasted_energy_harvest.py
 COPY src/a11oy/harvest/harvest_budget.py ./src/a11oy/harvest/harvest_budget.py

src/a11oy/formulas/allodial.py

@@ -0,0 +1,239 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+# © 2026 Lutar, Stephen P. — SZL Holdings · ORCID 0009-0001-0110-4173
+"""Allodial order-theoretic sovereignty checks — EXPERIMENTAL backbone.
+
+Mirrors the kernel-checked Lean declarations in ``Lutar/Allodial.lean`` (PR #229,
+merge 783a38d0).  These are PROPOSED engineering gates grounded in a 0-sorry,
+no-new-axiom EXPERIMENTAL Lean backbone — NOT locked-8 theorems and NOT formal
+Λ results.  Callers must treat them as EXPERIMENTAL-tier.
+
+Lean declarations mirrored (all EXPERIMENTAL, PR #229):
+  • allodial_dominates_all  — allodial element dominates every control class
+  • allodial_iff_top         — an element is allodial iff it equals ⊤
+  • feudal_has_overlord      — a feudal (non-allodial) element always has a strict overlord
+  • galois_preserves_allodial — adjoint (Galois) embeddings cannot destroy the allodial position
+  • ni_low_independent_of_high — operator-protected low output is independent of the
+                                  overlord/high state (non-interference)
+
+This is the formal grounding for the founder's central vision:
+  "allodial sovereign compute — no kill-switch, no one can switch it off."
+Any element that is NOT ⊤ has an overlord; an element that IS ⊤ is provably free.
+
+CITATION: Lutar/Allodial.lean (PR #229, merge 783a38d0)
+LEAN_THEOREM: Lutar/Allodial.lean::allodial_dominates_all / galois_preserves_allodial / ni_low_independent_of_high (EXPERIMENTAL — PROPOSED gate, not a locked theorem)
+"""
+from __future__ import annotations
+
+from typing import TypedDict, Any, Hashable
+
+CITATION = "Lutar/Allodial.lean (PR #229, merge 783a38d0)"
+LEAN_THEOREM = (
+    "Lutar/Allodial.lean::allodial_dominates_all / galois_preserves_allodial"
+    " / ni_low_independent_of_high"
+    " (EXPERIMENTAL — PROPOSED gate, not a locked theorem)"
+)
+_HONEST_NOTE = (
+    "EXPERIMENTAL-tier backbone: the Lean declarations are kernel-checked,"
+    " 0-sorry, no-new-axiom, but are PROPOSED engineering gates — NOT locked-8"
+    " theorems and NOT formal Λ results.  This Python module is a faithful but"
+    " informal mirror of those proofs, not the proof itself."
+)
+
+# ---------------------------------------------------------------------------
+# Core predicate functions
+# ---------------------------------------------------------------------------
+
+def is_allodial(elem: Hashable, top: Hashable) -> bool:
+    """Return True iff ``elem`` equals the lattice top element ⊤.
+
+    Mirrors ``allodial_iff_top``: allodial ↔ elem = ⊤.
+    An element is allodial (sovereign, no overlord) if and only if it IS the top.
+    """
+    return elem == top
+
+
+def dominates_all(
+    elem: Hashable,
+    elements: list[Hashable],
+    leq: list[tuple[Hashable, Hashable]],
+) -> bool:
+    """Return True iff ``elem`` is ≥ every other element in ``elements``.
+
+    Mirrors ``allodial_dominates_all``: if x is allodial (= ⊤) then ∀ y, y ≤ x.
+    ``leq`` is the list of (a, b) pairs meaning a ≤ b in the partial order.
+    Reflexivity (x ≤ x) is assumed; it need not appear in ``leq``.
+    """
+    leq_set: set[tuple[Hashable, Hashable]] = set(leq)
+    for y in elements:
+        if y == elem:
+            continue  # reflexivity
+        if (y, elem) not in leq_set:
+            return False
+    return True
+
+
+def has_overlord(
+    elem: Hashable,
+    top: Hashable,
+    elements: list[Hashable],
+    leq: list[tuple[Hashable, Hashable]],
+) -> bool:
+    """Return True iff ``elem`` has a strict overlord (i.e. is NOT allodial).
+
+    Mirrors ``feudal_has_overlord``: ¬allodial(x) → ∃ y, x < y.
+    A strict overlord is an element y ≠ elem such that elem ≤ y.
+    If elem IS the top, there is no overlord (allodial), so returns False.
+    """
+    if elem == top:
+        return False  # allodial — no overlord
+    leq_set: set[tuple[Hashable, Hashable]] = set(leq)
+    for y in elements:
+        if y == elem:
+            continue
+        if (elem, y) in leq_set:
+            return True  # found a strict overlord
+    return False
+
+
+def non_interference_check(
+    low_outputs_by_high_state: dict[Any, Any],
+) -> dict:
+    """Check whether the low-output is invariant across all high states.
+
+    Mirrors ``ni_low_independent_of_high``: the operator-protected low output
+    is independent of the overlord/high state.
+
+    ``low_outputs_by_high_state`` maps each high-state label → the low output
+    value observed when the system is in that high state.
+
+    Returns a dict with:
+      value      — True iff all low outputs are identical (non-interference holds)
+      invariant  — same as value
+      unique_low_outputs — the set of distinct low output values seen
+      high_state_count   — how many high states were checked
+      citation   — canonical citation
+      lean_theorem — the Lean theorem tag
+      tier       — "experimental"
+      honest_note — honesty annotation
+    """
+    values = list(low_outputs_by_high_state.values())
+    unique = set(values) if values else set()
+    invariant = len(unique) <= 1
+    return {
+        "value": invariant,
+        "invariant": invariant,
+        "unique_low_outputs": sorted(str(v) for v in unique),
+        "high_state_count": len(low_outputs_by_high_state),
+        "citation": CITATION,
+        "lean_theorem": LEAN_THEOREM,
+        "tier": "experimental",
+        "honest_note": _HONEST_NOTE,
+    }
+
+
+class AllodialResult(TypedDict):
+    value: bool
+    is_allodial: bool
+    dominates_all: bool
+    has_overlord: bool
+    elem: str
+    top: str
+    citation: str
+    lean_theorem: str
+    tier: str
+    honest_note: str
+
+
+def allodial_check(
+    elem: Hashable,
+    top: Hashable,
+    elements: list[Hashable],
+    leq: list[tuple[Hashable, Hashable]],
+) -> AllodialResult:
+    """Full allodiality assessment for ``elem`` on the given finite control lattice.
+
+    Returns the HONEST schema with EXPERIMENTAL-tier annotation.
+    ``value`` is True iff elem is allodial (= ⊤ and dominates all).
+    """
+    ia = is_allodial(elem, top)
+    da = dominates_all(elem, elements, leq)
+    ho = has_overlord(elem, top, elements, leq)
+    verdict = ia and da and not ho
+    return AllodialResult(
+        value=verdict,
+        is_allodial=ia,
+        dominates_all=da,
+        has_overlord=ho,
+        elem=str(elem),
+        top=str(top),
+        citation=CITATION,
+        lean_theorem=LEAN_THEOREM,
+        tier="experimental",
+        honest_note=_HONEST_NOTE,
+    )
+
+
+__all__ = [
+    "is_allodial",
+    "dominates_all",
+    "has_overlord",
+    "non_interference_check",
+    "allodial_check",
+    "CITATION",
+    "LEAN_THEOREM",
+]
+
+# Doctrine v11 LOCKED — 749/14/163 — c7c0ba17 · Λ = Conjecture 1 (NEVER a theorem)
+# SLSA L1 honest. L2 build-provenance attestation = roadmap (Wire D) — not yet claimed. L3 not claimed.
+
+
+if __name__ == "__main__":
+    # -----------------------------------------------------------------------
+    # Self-tests: 4-element lattice  ⊥ < a < b < ⊤
+    #   Elements: {bot, a, b, top}
+    #   Partial order (non-reflexive pairs stored explicitly):
+    #     bot≤a, bot≤b, bot≤top, a≤b, a≤top, b≤top
+    # -----------------------------------------------------------------------
+    elements = ["bot", "a", "b", "top"]
+    leq = [
+        ("bot", "a"), ("bot", "b"), ("bot", "top"),
+        ("a", "b"), ("a", "top"),
+        ("b", "top"),
+    ]
+    top = "top"
+    checks = 0
+
+    # 1. allodial_iff_top: top is allodial, others are not
+    assert is_allodial("top", top) is True, "top should be allodial"
+    assert is_allodial("a", top) is False, "'a' should not be allodial"
+    assert is_allodial("bot", top) is False, "'bot' should not be allodial"
+    checks += 3
+
+    # 2. dominates_all: top dominates everything; 'a' does NOT dominate 'b'
+    assert dominates_all("top", elements, leq) is True, "top must dominate all"
+    assert dominates_all("a", elements, leq) is False, "'a' must not dominate 'b' or 'top'"
+    checks += 2
+
+    # 3. has_overlord: non-top elements have an overlord; top does not
+    assert has_overlord("a", top, elements, leq) is True, "'a' has overlord 'b' (and 'top')"
+    assert has_overlord("bot", top, elements, leq) is True, "'bot' has overlords"
+    assert has_overlord("top", top, elements, leq) is False, "top has no overlord"
+    checks += 3
+
+    # 4. non_interference_check: invariant when low outputs are constant
+    ni_ok = non_interference_check({"high_a": "out_x", "high_b": "out_x", "high_c": "out_x"})
+    assert ni_ok["invariant"] is True, "constant low output must be non-interfering"
+    # FAILS when low outputs vary by high state
+    ni_fail = non_interference_check({"high_a": "out_x", "high_b": "out_y"})
+    assert ni_fail["invariant"] is False, "varying low output must flag interference"
+    checks += 2
+
+    # 5. Full allodial_check on the lattice
+    top_result = allodial_check("top", top, elements, leq)
+    assert top_result["value"] is True, "top must pass full allodial check"
+    a_result = allodial_check("a", top, elements, leq)
+    assert a_result["value"] is False, "'a' must fail full allodial check"
+    checks += 2
+
+    print(f"ok:true checks:{checks}")

src/a11oy/formulas/allodial_gate.py

@@ -0,0 +1,201 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+# © 2026 Lutar, Stephen P. — SZL Holdings · ORCID 0009-0001-0110-4173
+"""Sovereignty gate — EXPERIMENTAL, grounded in Allodial non-interference.
+
+Operationalizes the half-state doctrine: a node is sovereign ONLY when a local
+or owner-controlled node ACTUALLY serves requests.  The critical failure mode —
+the "half-state" — is when a banner claims sovereignty while request routing is
+silently delegated to an external/third-party router.  This is the ONLY
+unacceptable outcome and is explicitly flagged.
+
+Doctrine grounding:
+  The allodial non-interference theorem (``ni_low_independent_of_high`` in
+  ``Lutar/Allodial.lean``, PR #229, merge 783a38d0) establishes that the
+  sovereign (low-security, user-visible) verdict must be INDEPENDENT of the
+  external (high-security, overlord) router's state.  When routing is
+  externally delegated, the low output (sovereignty verdict) becomes a function
+  of the external router's state — violating non-interference and destroying the
+  allodial position.
+
+The half-state is the lattice analogue of a feudal element claiming the allodial
+position: the banner says ⊤ while the actual routing position is strictly below
+⊤ (under an external overlord).
+
+CITATION: Lutar/Allodial.lean (PR #229, merge 783a38d0) — ni_low_independent_of_high
+LEAN_THEOREM: Lutar/Allodial.lean::ni_low_independent_of_high / allodial_iff_top (EXPERIMENTAL — PROPOSED gate, not a locked theorem)
+"""
+from __future__ import annotations
+
+from typing import TypedDict
+
+CITATION = "Lutar/Allodial.lean (PR #229, merge 783a38d0)"
+LEAN_THEOREM = (
+    "Lutar/Allodial.lean::ni_low_independent_of_high / allodial_iff_top"
+    " (EXPERIMENTAL — PROPOSED gate, not a locked theorem)"
+)
+_HONEST_NOTE = (
+    "EXPERIMENTAL-tier backbone: the Lean non-interference declaration is"
+    " kernel-checked, 0-sorry, no-new-axiom, but is a PROPOSED engineering gate"
+    " — NOT a locked-8 theorem and NOT a formal Λ result.  The half-state check"
+    " is a faithful but informal mirror of that proof, not the proof itself."
+    " The sovereignty verdict is ONLY true when a local/owned node actually serves;"
+    " any external routing delegation is the uniquely unacceptable half-state."
+)
+
+
+class SovereignVerdictOut(TypedDict):
+    sovereign: bool
+    half_state: bool
+    served_by: str
+    base_url: str
+    local_node_serving: bool
+    reason: str
+    citation: str
+    lean_theorem: str
+    tier: str
+    honest_note: str
+
+
+def sovereign_verdict(
+    served_by: str,
+    base_url: str,
+    local_node_serving: bool,
+) -> SovereignVerdictOut:
+    """Compute the sovereignty verdict for a serving node.
+
+    Mirrors ``ni_low_independent_of_high``: the low-security (user-visible)
+    sovereignty output must be invariant of the external (overlord) router state.
+    When an external router intermediates, the output becomes router-state-dependent,
+    destroying the allodial position.
+
+    Parameters
+    ----------
+    served_by          : identifier of the serving entity (e.g. "local", "a11oy-node-0",
+                         "external-router", "third-party-cdn", etc.)
+    base_url           : the base URL at which this service is presented
+    local_node_serving : True iff a local/owner-controlled node is ACTUALLY serving
+                         requests right now (not just claimed in a banner)
+
+    Returns
+    -------
+    SovereignVerdictOut with:
+      sovereign   — True ONLY when local_node_serving is True
+      half_state  — True when banner-sovereignty is claimed (via base_url or served_by)
+                    but local_node_serving is False — the uniquely unacceptable outcome
+      reason      — human-readable explanation
+    """
+    # Determine whether the banner/branding implies a sovereignty claim.
+    # We treat any non-external served_by as an implicit sovereignty assertion.
+    external_keywords = {
+        "external", "router", "cdn", "proxy", "third-party", "thirdparty",
+        "cloudflare", "akamai", "fastly", "aws", "gcp", "azure",
+    }
+    served_by_lower = (served_by or "").lower()
+    banner_claims_sovereign = not any(kw in served_by_lower for kw in external_keywords)
+
+    if local_node_serving:
+        # Local node IS serving — allodial position is held.
+        # Non-interference is satisfied: the sovereignty verdict is independent
+        # of any external router's state because we are NOT routing through one.
+        return SovereignVerdictOut(
+            sovereign=True,
+            half_state=False,
+            served_by=served_by,
+            base_url=base_url,
+            local_node_serving=True,
+            reason=(
+                "Local/owned node is actively serving: allodial position held."
+                "  The sovereignty verdict is independent of any external router"
+                " state (ni_low_independent_of_high satisfied)."
+            ),
+            citation=CITATION,
+            lean_theorem=LEAN_THEOREM,
+            tier="experimental",
+            honest_note=_HONEST_NOTE,
+        )
+
+    # Local node is NOT serving.
+    if banner_claims_sovereign:
+        # HALF-STATE: banner claims sovereignty, but routing is externally delegated.
+        # This makes the sovereignty verdict (low output) a function of the external
+        # router's state — violating non-interference.  UNIQUELY UNACCEPTABLE.
+        return SovereignVerdictOut(
+            sovereign=False,
+            half_state=True,
+            served_by=served_by,
+            base_url=base_url,
+            local_node_serving=False,
+            reason=(
+                "HALF-STATE DETECTED: the banner asserts sovereignty but routing is"
+                " delegated externally.  The low (user-visible) sovereignty verdict"
+                " now depends on the external router's state — this violates"
+                " ni_low_independent_of_high and the allodial position is lost."
+                "  This is the uniquely unacceptable outcome."
+            ),
+            citation=CITATION,
+            lean_theorem=LEAN_THEOREM,
+            tier="experimental",
+            honest_note=_HONEST_NOTE,
+        )
+
+    # External router is explicit; no sovereignty claim made — honest non-sovereign state.
+    return SovereignVerdictOut(
+        sovereign=False,
+        half_state=False,
+        served_by=served_by,
+        base_url=base_url,
+        local_node_serving=False,
+        reason=(
+            "External routing acknowledged openly: no sovereignty claim made."
+            "  Not allodial, but no half-state deception — this is honest."
+        ),
+        citation=CITATION,
+        lean_theorem=LEAN_THEOREM,
+        tier="experimental",
+        honest_note=_HONEST_NOTE,
+    )
+
+
+__all__ = ["sovereign_verdict", "CITATION", "LEAN_THEOREM"]
+
+# Doctrine v11 LOCKED — 749/14/163 — c7c0ba17 · Λ = Conjecture 1 (NEVER a theorem)
+# SLSA L1 honest. L2 build-provenance attestation = roadmap (Wire D) — not yet claimed. L3 not claimed.
+
+
+if __name__ == "__main__":
+    # -----------------------------------------------------------------------
+    # Self-tests for the sovereignty gate
+    # -----------------------------------------------------------------------
+    checks = 0
+
+    # 1. local_node_serving=True → sovereign:true, half_state:false
+    r = sovereign_verdict("a11oy-node-0", "https://a11oy.net", True)
+    assert r["sovereign"] is True, "local serving must yield sovereign:true"
+    assert r["half_state"] is False, "local serving must not be a half-state"
+    checks += 2
+
+    # 2. Banner sovereign (non-external served_by) + local_node_serving=False → half_state:true, sovereign:false
+    r2 = sovereign_verdict("a11oy-node-0", "https://a11oy.net", False)
+    assert r2["sovereign"] is False, "external routing must yield sovereign:false"
+    assert r2["half_state"] is True, "banner+no-local-serving must be half_state:true"
+    checks += 2
+
+    # 3. Explicit external router + local_node_serving=False → sovereign:false, half_state:false (honest)
+    r3 = sovereign_verdict("external-router", "https://a11oy.net", False)
+    assert r3["sovereign"] is False, "explicit external must yield sovereign:false"
+    assert r3["half_state"] is False, "explicit external with no claim must not be half-state"
+    checks += 2
+
+    # 4. CDN variant: served_by contains "cloudflare", local_node_serving=False
+    r4 = sovereign_verdict("cloudflare-cdn", "https://a11oy.net", False)
+    assert r4["half_state"] is False, "known external CDN must not be half-state"
+    assert r4["sovereign"] is False, "CDN serving must yield sovereign:false"
+    checks += 2
+
+    # 5. Sovereignty is ONLY true when local_node_serving is True (tier/citation checks)
+    assert r["tier"] == "experimental", "must carry experimental tier"
+    assert "ni_low_independent_of_high" in r["lean_theorem"], "must reference non-interference theorem"
+    checks += 2
+
+    print(f"ok:true checks:{checks}")

src/a11oy/formulas/entanglement.py

@@ -0,0 +1,184 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+# © 2026 Lutar, Stephen P. — SZL Holdings · ORCID 0009-0001-0110-4173
+"""Coherence-decay entanglement-generating-capacity bound — EXPERIMENTAL backbone.
+
+Mirrors the kernel-checked Lean declarations in ``Lutar/Entanglement.lean``
+(PR #230, merge 3a7f222ed3bb).  These are PROPOSED engineering gates grounded
+in a 0-sorry, no-new-axiom EXPERIMENTAL Lean backbone — NOT locked-8 theorems
+and NOT formal Λ results.  This is a CAPACITY BOUND, not a claimed rate.
+
+Lean declarations mirrored (all EXPERIMENTAL, PR #230):
+  • capBound C₀ γ t = C₀ · exp(−γ·t)   — the capacity-bound formula
+  • capBound_nonneg    — bound is ≥ 0 for non-negative inputs
+  • capBound_zero      — bound = 0 when C₀ = 0
+  • capBound_antitone  — bound is antitone (strictly decreasing) in t for γ > 0
+  • entanglement_decays_under_bound — entanglement-generating capacity stays ≤ capBound
+
+Physical interpretation: as coherence decays exponentially at rate γ, the upper
+bound on entanglement-generating capacity also decays.  This is a CEILING, not a
+guarantee of any specific entanglement rate.
+
+CITATION: Lutar/Entanglement.lean (PR #230, merge 3a7f222ed3bb)
+LEAN_THEOREM: Lutar/Entanglement.lean::capBound_antitone / entanglement_decays_under_bound (EXPERIMENTAL — PROPOSED gate, not a locked theorem)
+"""
+from __future__ import annotations
+
+import math
+from typing import TypedDict
+
+CITATION = "Lutar/Entanglement.lean (PR #230, merge 3a7f222ed3bb)"
+LEAN_THEOREM = (
+    "Lutar/Entanglement.lean::capBound_antitone"
+    " / entanglement_decays_under_bound"
+    " (EXPERIMENTAL — PROPOSED gate, not a locked theorem)"
+)
+_HONEST_NOTE = (
+    "EXPERIMENTAL-tier backbone: the Lean declarations are kernel-checked,"
+    " 0-sorry, no-new-axiom, but are PROPOSED engineering gates — NOT locked-8"
+    " theorems and NOT formal Λ results.  This is a CAPACITY UPPER BOUND on"
+    " entanglement-generating capacity under coherence decay; it does not"
+    " guarantee any specific entanglement rate.  The Python module is a"
+    " faithful but informal mirror of those proofs, not the proof itself."
+)
+
+
+class CapBoundOut(TypedDict):
+    value: float
+    cap_bound: float
+    c0: float
+    gamma: float
+    t: float
+    nonneg: bool
+    antitone_check: bool
+    citation: str
+    lean_theorem: str
+    tier: str
+    honest_note: str
+
+
+def cap_bound(c0: float, gamma: float, t: float) -> float:
+    """Coherence→entanglement-generating-capacity upper bound: C₀ · exp(−γ·t).
+
+    Mirrors ``capBound C₀ γ t`` in Lutar/Entanglement.lean.
+
+    Parameters
+    ----------
+    c0    : initial capacity (≥ 0)
+    gamma : decay rate (≥ 0; γ=0 → constant bound)
+    t     : time (≥ 0)
+
+    Returns the scalar bound value ≥ 0.
+    """
+    if c0 < 0.0:
+        raise ValueError("c0 must be >= 0 (initial capacity is non-negative)")
+    if gamma < 0.0:
+        raise ValueError("gamma must be >= 0 (decay rate is non-negative)")
+    if t < 0.0:
+        raise ValueError("t must be >= 0 (time is non-negative)")
+    return c0 * math.exp(-gamma * t)
+
+
+def cap_bound_nonneg(c0: float, gamma: float, t: float) -> bool:
+    """Return True iff cap_bound(c0, gamma, t) >= 0.
+
+    Mirrors ``capBound_nonneg``.  Always True for non-negative inputs (trivially
+    follows from exp being positive), but exposed as an explicit gate.
+    """
+    return cap_bound(c0, gamma, t) >= 0.0
+
+
+def cap_bound_antitone(
+    c0: float, gamma: float, t1: float, t2: float
+) -> bool:
+    """Return True iff cap_bound is antitone: t1 < t2 → cap_bound(t1) ≥ cap_bound(t2).
+
+    Mirrors ``capBound_antitone``.  For γ > 0 and t1 < t2 the bound strictly decreases.
+    For γ = 0 the bound is constant (weakly antitone, i.e. ≥ holds with equality).
+    """
+    if t1 >= t2:
+        raise ValueError("antitone check requires t1 < t2")
+    return cap_bound(c0, gamma, t1) >= cap_bound(c0, gamma, t2) - 1e-15
+
+
+def entanglement_decays_under_bound(
+    c0: float, gamma: float, t: float, observed_capacity: float
+) -> bool:
+    """Return True iff observed_capacity ≤ cap_bound(c0, gamma, t).
+
+    Mirrors ``entanglement_decays_under_bound``: the actual entanglement-generating
+    capacity is bounded above by the exponential decay envelope.  Use this as an
+    operational sanity gate on a measured or claimed capacity figure.
+    """
+    return observed_capacity <= cap_bound(c0, gamma, t) + 1e-15
+
+
+def cap_bound_full(c0: float, gamma: float, t: float) -> CapBoundOut:
+    """Full HONEST schema response for the capacity-bound endpoint."""
+    val = cap_bound(c0, gamma, t)
+    nonneg = val >= 0.0
+    # Antitone check: bound at t+1 should be <= bound at t (for t >= 0)
+    antitone = cap_bound_antitone(c0, gamma, t, t + 1.0) if gamma > 0.0 else True
+    return CapBoundOut(
+        value=val,
+        cap_bound=val,
+        c0=c0,
+        gamma=gamma,
+        t=t,
+        nonneg=nonneg,
+        antitone_check=antitone,
+        citation=CITATION,
+        lean_theorem=LEAN_THEOREM,
+        tier="experimental",
+        honest_note=_HONEST_NOTE,
+    )
+
+
+__all__ = [
+    "cap_bound",
+    "cap_bound_nonneg",
+    "cap_bound_antitone",
+    "entanglement_decays_under_bound",
+    "cap_bound_full",
+    "CITATION",
+    "LEAN_THEOREM",
+]
+
+# Doctrine v11 LOCKED — 749/14/163 — c7c0ba17 · Λ = Conjecture 1 (NEVER a theorem)
+# SLSA L1 honest. L2 build-provenance attestation = roadmap (Wire D) — not yet claimed. L3 not claimed.
+
+
+if __name__ == "__main__":
+    # -----------------------------------------------------------------------
+    # Self-tests for cap_bound and derivative predicates
+    # -----------------------------------------------------------------------
+    checks = 0
+
+    # 1. cap_bound(C0, γ, 0) == C0 (mirrors capBound_nonneg + zero-time identity)
+    assert abs(cap_bound(2.5, 0.3, 0.0) - 2.5) < 1e-12, "cap_bound at t=0 must equal C0"
+    assert abs(cap_bound(0.0, 0.5, 10.0) - 0.0) < 1e-12, "cap_bound with C0=0 must be 0"
+    checks += 2
+
+    # 2. nonneg: always true for non-negative inputs
+    assert cap_bound_nonneg(1.0, 0.5, 5.0) is True, "bound must be non-negative"
+    assert cap_bound_nonneg(0.0, 0.0, 0.0) is True, "zero bound is non-negative"
+    checks += 2
+
+    # 3. antitone: bound at t+1 <= bound at t for γ > 0
+    assert cap_bound_antitone(1.0, 0.5, 0.0, 1.0) is True, "antitone: t=0 >= t=1"
+    assert cap_bound_antitone(3.0, 0.1, 2.0, 5.0) is True, "antitone: t=2 >= t=5"
+    checks += 2
+
+    # 4. entanglement_decays_under_bound
+    # Observed at the bound itself: must pass
+    cb = cap_bound(1.0, 0.5, 2.0)
+    assert entanglement_decays_under_bound(1.0, 0.5, 2.0, cb) is True, "at bound: ok"
+    # Observed above the bound: must fail
+    assert entanglement_decays_under_bound(1.0, 0.5, 2.0, cb + 0.1) is False, "above bound: fail"
+    checks += 2
+
+    # 5. Strict decay check: cap_bound(1, 1, 1) < cap_bound(1, 1, 0)
+    assert cap_bound(1.0, 1.0, 1.0) < cap_bound(1.0, 1.0, 0.0), "strictly decays for γ>0"
+    checks += 1
+
+    print(f"ok:true checks:{checks}")

szl_dark_surfaces_register.py

@@ -19,7 +19,8 @@ DARK SURFACES WIRED (route -> module -> register kind):
   /api/<ns>/v1/formula/sovereign   a11oy_formula_endpoints  register(app, ns)
   /api/<ns>/v1/energy/provenance   szl_energy_provenance    register(app, ns)
   /api/<ns>/v1/heart/pulse         szl_heart_blood          register(app, ns)
-  /v1/ayni (+ /v1/replay,/tinkuy)  ayni_os_serve            include_router(router)
+  /api/<ns>/v1/ayni (+ replay,    ayni_os_serve            include_router(prefix=/api/<ns>)
+   tinkuy; legacy bare /v1/ayni kept)
   /api/<ns>/v1/anatomy/loop        szl_anatomy_loop         register(app, ns)  [#341]
 
 ADDITIVE — never replaces a route, never edits another module. Registered BEFORE
@@ -99,22 +100,41 @@ def register(app: Any, ns: str = "a11oy") -> List[str]:
             _stderr(line)
             status.append(line)
 
-    # AYNI-OS is mounted via include_router (self-contained APIRouter at /v1/ayni,
-    # /v1/replay, /v1/tinkuy), NOT register(app, ns) — own try/except below.
+    # AYNI-OS is a self-contained APIRouter whose routes declare bare paths
+    # (/v1/ayni, /v1/replay, /v1/tinkuy). The DOCUMENTED, dashboard-facing contract
+    # is /api/<ns>/v1/ayni (the same /api/<ns>/v1/* shape every other dark surface
+    # uses); mounting the router WITHOUT a prefix left it at /v1/ayni, so the
+    # documented /api/<ns>/v1/ayni 404'd (it fell through to the Node proxy, which
+    # answered {"error":"not found","path":"/v1/ayni"}). FIX: include the router under
+    # prefix=/api/<ns> so the documented /api/<ns>/v1/ayni path resolves LOCALLY and
+    # wins ordering (registered here, before the SPA catch-all / Node proxy). We ALSO
+    # keep the legacy bare /v1/ayni mount for back-compat — purely additive, so any
+    # existing caller of the old path is never broken. NOT register(app, ns) — own
+    # try/except below so AYNI absent never blocks the other six surfaces.
     try:
         from ayni_os_serve import router as _ayni_router  # type: ignore
         included = False
         include_router = getattr(app, "include_router", None)
         if callable(include_router):
+            # Documented path: /api/<ns>/v1/ayni (+ /replay, /tinkuy). Resolves LOCALLY.
+            app.include_router(_ayni_router, prefix=f"/api/{ns}")
+            # Legacy path: bare /v1/ayni — additive back-compat, breaks no caller.
             app.include_router(_ayni_router)
             included = True
         else:
-            # Bare Starlette fallback: splice the router's routes onto app.router.
+            # Bare Starlette fallback: splice the router's routes onto app.router at
+            # BOTH the documented /api/<ns> prefix and the legacy bare path.
+            from starlette.routing import Route as _Route
             for _r in getattr(_ayni_router, "routes", []):
+                _path = getattr(_r, "path", None)
+                _ep = getattr(_r, "endpoint", None)
+                _methods = list(getattr(_r, "methods", []) or ["GET"])
+                if _path is not None and _ep is not None:
+                    app.router.routes.append(_Route(f"/api/{ns}{_path}", _ep, methods=_methods))
                 app.router.routes.append(_r)
             included = True
         if included:
-            line = "[a11oy:dark] AYNI-OS mounted: /v1/ayni + /v1/replay + /v1/tinkuy"
+            line = f"[a11oy:dark] AYNI-OS mounted: /api/{ns}/v1/ayni + /api/{ns}/v1/replay + /api/{ns}/v1/tinkuy (legacy /v1/ayni kept)"
             _stderr(line)
             status.append(line)
     except Exception as exc:  # additive: AYNI absent never blocks the other six