Spaces:
Running
Running
chore(sync): mirror backend .py + Dockerfile to Space (hf-sync-backend)
Browse filesAutomated backend sync from szl-holdings/a11oy main via hf-sync-backend.
Updated (differed from the Space): a11oy_formula_endpoints.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.
- a11oy_formula_endpoints.py +87 -0
a11oy_formula_endpoints.py
CHANGED
|
@@ -20,6 +20,10 @@ Endpoints:
|
|
| 20 |
GET /api/a11oy/v1/formula/reidemeister?a=1,-1&b= -> braid equivalence
|
| 21 |
GET /api/a11oy/v1/formula/hnsw -> honest Reasoning-delegate status
|
| 22 |
GET /api/a11oy/v1/formula/bls -> BLS backend availability (honest)
|
|
|
|
|
|
|
|
|
|
|
|
|
| 23 |
GET /api/a11oy/v1/formulas/index -> list of wired formulas + citations
|
| 24 |
|
| 25 |
Doctrine v11 LOCKED — 749/14/163 — c7c0ba17 · Λ = Conjecture 1 (NEVER a theorem).
|
|
@@ -48,9 +52,12 @@ except Exception: # pragma: no cover
|
|
| 48 |
|
| 49 |
try:
|
| 50 |
from a11oy.formulas import (
|
|
|
|
|
|
|
| 51 |
bloom_filter,
|
| 52 |
bls_aggregate,
|
| 53 |
byzantine_quorum,
|
|
|
|
| 54 |
hnsw_retrieval,
|
| 55 |
holevo_bound,
|
| 56 |
kalman,
|
|
@@ -86,6 +93,19 @@ _INDEX = [
|
|
| 86 |
"lean_theorem": "Wave17/BinaryPinsker.lean::binary_pinsker (CF-23)", "tier": "experimental"},
|
| 87 |
{"name": "aftershock", "citation": "Reasenberg–Jones 1989; Gasperini–Lolli 2006 (α≈⅔b); USGS live feed",
|
| 88 |
"lean_theorem": "(seismic forecast — not a Lean theorem; generic-parameter R–J model)", "tier": "live-data"},
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 89 |
]
|
| 90 |
|
| 91 |
|
|
@@ -263,6 +283,73 @@ def register(app, ns: str = "a11oy") -> str:
|
|
| 263 |
"lean_theorem": bls_aggregate.LEAN_THEOREM,
|
| 264 |
})
|
| 265 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 266 |
return f"formulas-wired:{len(_INDEX)}"
|
| 267 |
|
| 268 |
|
|
|
|
| 20 |
GET /api/a11oy/v1/formula/reidemeister?a=1,-1&b= -> braid equivalence
|
| 21 |
GET /api/a11oy/v1/formula/hnsw -> honest Reasoning-delegate status
|
| 22 |
GET /api/a11oy/v1/formula/bls -> BLS backend availability (honest)
|
| 23 |
+
GET /api/a11oy/v1/formula/allodial?elem=&top=&elements=&leq= -> allodiality check (EXPERIMENTAL)
|
| 24 |
+
GET /api/a11oy/v1/formula/entanglement?c0=&gamma=&t= -> cap-bound (EXPERIMENTAL)
|
| 25 |
+
GET /api/a11oy/v1/formula/sovereign?served_by=&base_url=&local_node_serving= -> sovereignty gate (EXPERIMENTAL)
|
| 26 |
+
POST /api/a11oy/v1/formula/sovereign {served_by, base_url, local_node_serving} -> sovereignty gate (EXPERIMENTAL)
|
| 27 |
GET /api/a11oy/v1/formulas/index -> list of wired formulas + citations
|
| 28 |
|
| 29 |
Doctrine v11 LOCKED — 749/14/163 — c7c0ba17 · Λ = Conjecture 1 (NEVER a theorem).
|
|
|
|
| 52 |
|
| 53 |
try:
|
| 54 |
from a11oy.formulas import (
|
| 55 |
+
allodial,
|
| 56 |
+
allodial_gate,
|
| 57 |
bloom_filter,
|
| 58 |
bls_aggregate,
|
| 59 |
byzantine_quorum,
|
| 60 |
+
entanglement,
|
| 61 |
hnsw_retrieval,
|
| 62 |
holevo_bound,
|
| 63 |
kalman,
|
|
|
|
| 93 |
"lean_theorem": "Wave17/BinaryPinsker.lean::binary_pinsker (CF-23)", "tier": "experimental"},
|
| 94 |
{"name": "aftershock", "citation": "Reasenberg–Jones 1989; Gasperini–Lolli 2006 (α≈⅔b); USGS live feed",
|
| 95 |
"lean_theorem": "(seismic forecast — not a Lean theorem; generic-parameter R–J model)", "tier": "live-data"},
|
| 96 |
+
# ---- EXPERIMENTAL frontier backbones (Lutar/Allodial.lean + Lutar/Entanglement.lean) ----
|
| 97 |
+
{"name": "allodial",
|
| 98 |
+
"citation": "Lutar/Allodial.lean (PR #229, merge 783a38d0)",
|
| 99 |
+
"lean_theorem": "Lutar/Allodial.lean::allodial_dominates_all / galois_preserves_allodial / ni_low_independent_of_high (EXPERIMENTAL — PROPOSED gate, not a locked theorem)",
|
| 100 |
+
"tier": "experimental"},
|
| 101 |
+
{"name": "entanglement",
|
| 102 |
+
"citation": "Lutar/Entanglement.lean (PR #230, merge 3a7f222ed3bb)",
|
| 103 |
+
"lean_theorem": "Lutar/Entanglement.lean::capBound_antitone / entanglement_decays_under_bound (EXPERIMENTAL — PROPOSED gate, not a locked theorem)",
|
| 104 |
+
"tier": "experimental"},
|
| 105 |
+
{"name": "sovereign",
|
| 106 |
+
"citation": "Lutar/Allodial.lean (PR #229, merge 783a38d0) — ni_low_independent_of_high",
|
| 107 |
+
"lean_theorem": "Lutar/Allodial.lean::ni_low_independent_of_high / allodial_iff_top (EXPERIMENTAL — PROPOSED gate, not a locked theorem)",
|
| 108 |
+
"tier": "experimental"},
|
| 109 |
]
|
| 110 |
|
| 111 |
|
|
|
|
| 283 |
"lean_theorem": bls_aggregate.LEAN_THEOREM,
|
| 284 |
})
|
| 285 |
|
| 286 |
+
# ---- EXPERIMENTAL frontier: Allodial order-theoretic sovereignty checks ----
|
| 287 |
+
@app.get(f"{base}/allodial")
|
| 288 |
+
async def _allodial(elem: str = "top", top: str = "top",
|
| 289 |
+
elements: str = "bot,a,b,top",
|
| 290 |
+
leq: str = "bot:a,bot:b,bot:top,a:b,a:top,b:top"):
|
| 291 |
+
"""Allodial check on a finite control lattice (EXPERIMENTAL).
|
| 292 |
+
|
| 293 |
+
Pass `elem`, `top`, `elements` (comma-sep), and `leq` (comma-sep a:b pairs).
|
| 294 |
+
Returns the HONEST EXPERIMENTAL-tier allodiality assessment.
|
| 295 |
+
NOTE: EXPERIMENTAL backbone — Lutar/Allodial.lean PR #229, NOT locked-8, NOT a formal \u039b result.
|
| 296 |
+
"""
|
| 297 |
+
try:
|
| 298 |
+
elems_list = [e.strip() for e in elements.split(",") if e.strip()]
|
| 299 |
+
leq_pairs = []
|
| 300 |
+
for pair in leq.split(","):
|
| 301 |
+
pair = pair.strip()
|
| 302 |
+
if ":" in pair:
|
| 303 |
+
a_part, b_part = pair.split(":", 1)
|
| 304 |
+
leq_pairs.append((a_part.strip(), b_part.strip()))
|
| 305 |
+
result = allodial.allodial_check(elem, top, elems_list, leq_pairs)
|
| 306 |
+
return JSONResponse(dict(result))
|
| 307 |
+
except ValueError as e:
|
| 308 |
+
return JSONResponse({"error": str(e)}, status_code=400)
|
| 309 |
+
|
| 310 |
+
# ---- EXPERIMENTAL frontier: Entanglement-generating-capacity bound ----
|
| 311 |
+
@app.get(f"{base}/entanglement")
|
| 312 |
+
async def _entanglement(c0: float = 1.0, gamma: float = 0.5, t: float = 1.0):
|
| 313 |
+
"""Coherence\u2192entanglement-generating-capacity upper bound cap_bound(C\u2080,\u03b3,t) = C\u2080\u00b7exp(\u2212\u03b3t).
|
| 314 |
+
|
| 315 |
+
This is a CAPACITY UPPER BOUND, not a claimed entanglement rate.
|
| 316 |
+
NOTE: EXPERIMENTAL backbone \u2014 Lutar/Entanglement.lean PR #230, NOT locked-8, NOT a formal \u039b result.
|
| 317 |
+
"""
|
| 318 |
+
try:
|
| 319 |
+
return JSONResponse(dict(entanglement.cap_bound_full(c0, gamma, t)))
|
| 320 |
+
except ValueError as e:
|
| 321 |
+
return JSONResponse({"error": str(e)}, status_code=400)
|
| 322 |
+
|
| 323 |
+
# ---- EXPERIMENTAL frontier: Sovereignty gate (half-state doctrine) ----
|
| 324 |
+
@app.get(f"{base}/sovereign")
|
| 325 |
+
async def _sovereign_get(served_by: str = "local", base_url: str = "",
|
| 326 |
+
local_node_serving: bool = False):
|
| 327 |
+
"""Sovereignty gate: returns sovereign:true ONLY when a local/owned node actually serves.
|
| 328 |
+
|
| 329 |
+
The half-state (banner claims sovereignty while routing to an external node) is the
|
| 330 |
+
ONLY unacceptable outcome and is flagged with half_state:true, sovereign:false.
|
| 331 |
+
Grounded in Lutar/Allodial.lean::ni_low_independent_of_high (EXPERIMENTAL).
|
| 332 |
+
"""
|
| 333 |
+
return JSONResponse(dict(allodial_gate.sovereign_verdict(
|
| 334 |
+
served_by, base_url, local_node_serving
|
| 335 |
+
)))
|
| 336 |
+
|
| 337 |
+
@app.post(f"{base}/sovereign")
|
| 338 |
+
async def _sovereign_post(req: Request):
|
| 339 |
+
"""Sovereignty gate via POST body {served_by, base_url, local_node_serving}.
|
| 340 |
+
|
| 341 |
+
The half-state (banner claims sovereignty while routing to an external node) is the
|
| 342 |
+
ONLY unacceptable outcome and is flagged with half_state:true, sovereign:false.
|
| 343 |
+
Grounded in Lutar/Allodial.lean::ni_low_independent_of_high (EXPERIMENTAL).
|
| 344 |
+
"""
|
| 345 |
+
body = await req.json()
|
| 346 |
+
served_by = str(body.get("served_by", "local"))
|
| 347 |
+
base_url = str(body.get("base_url", ""))
|
| 348 |
+
local_node_serving = bool(body.get("local_node_serving", False))
|
| 349 |
+
return JSONResponse(dict(allodial_gate.sovereign_verdict(
|
| 350 |
+
served_by, base_url, local_node_serving
|
| 351 |
+
)))
|
| 352 |
+
|
| 353 |
return f"formulas-wired:{len(_INDEX)}"
|
| 354 |
|
| 355 |
|