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, a11oy_canonical_domain.py, a11oy_formula_tiers.py, a11oy_wireA_metrics.py, serve.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

@@ -615,7 +615,7 @@ COPY web/formulas.html web/v4_fleet_panel.html web/operator.html web/fleet-c2.ht
 # the guarded import falls back to a stub in the image and the react endpoints
 # 404. Restores wiring clobbered by a later integration-wave push built from a
 # stale base (the register block in serve.py + this COPY were both lost).
-COPY knowledge.json szl_parity_gaps.py compliance_crosswalk.py szl_compliance_mesh.py a11oy_warhacker_obs.py serve.py szl_governed_api.py szl_demo_tier1.py szl_assurance.py govern_showcase.html a11oy_wireA_metrics.py cathedral.html a11oy_operator_organ.py a11oy_hf_assets.py szl_b2_secdata.py gates_manifest.json a11oy_code_orchestrator.py a11oy_agent_loop.py a11oy_org_rag.py a11oy_mcp_client.py szl_rag.py a11oy_code_ide.html wayra_serve.py wayra_snapshot.json wayra_digests_7d.json szl_khipu_os_routes.py szl_spaces_proxy.py szl_spaces_surface.py szl_khipu_consensus.py szl_puriq_formulas.py ayni_os_serve.py szl_live_wires.py live_wires.html live_wires_3d.js szl_intoto.py szl_intoto_routes.py szl_scitt.py szl_dsse.py szl_provenance.py szl_be_hardening.py szl_unay.py szl_khipu_lmdb.py szl_khipu_replicate.py szl_unay_routes.py szl_warhacker_aliases.py a11oy_v4_hickok.py szl_khipu.py szl_formulas.py a11oy_v4_formulas.py szl_anatomy_3d.py szl_anatomy_routes.py _vendor_blobs.py szl_v4_fleet.py operator_shell_v4.py szl_bridge.py szl_bridge_schemas.py agent.html a11oy_bridge_cli.py szl_ken.py a11oy_formula_endpoints.py a11oy_formulas_page.py a11oy_frontier_patch.py a11oy_v4_agent.py szl_brain.py szl_wire.py szl_hub.py szl_rosie_companion.py szl_receipt_substrate.py szl_alloy_embed_fabric.py szl_ayni_quorum.py szl_agentic_loop.py szl_formula_wiring.py szl_formula_surfaces.py a11oy_code_engine.py a11oy_code.py a11oy_seismic.py szl_warhacker_real.py szl_warhacker_demos.py NOTICE_warhacker_demos.txt szl_llm_registry.py szl_elite_console.py szl_alloy_models.py szl_scaling.py szl_allodial.py szl_entanglement.py szl_neuroplasticity.py szl_chain_of_title.py szl_sovereign_compute.py a11oy_active_flux_router.py szl_energy_budget.py szl_energy_sovereign.py szl_energy_provenance.py szl_heart_blood.py szl_engine_status.py szl_backend_hardening.py revenue_endpoints.py a11oy_harvest_endpoints.py joule_billing.py szl_energy_ledger.py szl_energy_operator.py szl_energy_projection.py szl_cheapest_watt.py szl_energy_live.py szl_orbital_topology.py szl_orbital_projection.py a11oy_orbital_page.py a11oy_frontier_page.py szl_frontier_manifest.py a11oy_code_as_action.py a11oy_governed_kernel.py szl_lambda_tripwire.py szl_provenance_receipt.py szl_khipu_verify.py szl_attest_stack.py szl_demo_sign.py szl_sda.py szl_fabric_surface.py szl_nemo_agents.py szl_kverify.py szl_specdec.py szl_immune.py szl_quant_qbio_holo.py szl_materials.py szl_materials_predict.py a11oy_factory.py a11oy_constitution.py a11oy_nav_wireup.py szl_mbse_cosim.py szl_mbse_nav.py szl_mbse.py szl_factory.py szl_willay_gateway.py a11oy_willay_nav.py szl_waqay.py a11oy_waqay_nav.py szl_yupay.py a11oy_yupay_nav.py a11oy_uds_portability_nav.py szl_pinn_bounds.py physical_bounds_certificate.json agentic_decision_trail.json physical_bounds_certificate.dsse.json szl_pinn_inverse.py szl_governed_ipinn.py szl_calphad_inverse.py szl_pnt_mesh.py quantum_sensing_limits.py pnt_resilience.py nav_coasting.py fundamental_limits.py szl_counter_uas_proxy.py szl_gpu_quant.py szl_joules_truth.py revenue_model.py szl_prod_hardening.py szl_resilience.py szl_observability.py szl_corpus_publish.py szl_lake_store.py szl_lake_ingest.py szl_e8.py szl_trajectory_sign.py szl_nemotron_ingest.py szl_nemotron_corpus.py szl_nemo_verify.py a11oy_nemo_core.py szl_restraint.py szl_sapa.py szl_sapa_patch.py szl_restraint_energy.py a11oy_react_core.py szl_org_lambda.py ./
+COPY knowledge.json szl_parity_gaps.py compliance_crosswalk.py szl_compliance_mesh.py a11oy_warhacker_obs.py serve.py szl_governed_api.py szl_demo_tier1.py szl_assurance.py govern_showcase.html a11oy_wireA_metrics.py cathedral.html a11oy_operator_organ.py a11oy_hf_assets.py szl_b2_secdata.py gates_manifest.json a11oy_code_orchestrator.py a11oy_agent_loop.py a11oy_org_rag.py a11oy_mcp_client.py szl_rag.py a11oy_code_ide.html wayra_serve.py wayra_snapshot.json wayra_digests_7d.json szl_khipu_os_routes.py szl_spaces_proxy.py szl_spaces_surface.py szl_khipu_consensus.py szl_puriq_formulas.py ayni_os_serve.py szl_live_wires.py live_wires.html live_wires_3d.js szl_intoto.py szl_intoto_routes.py szl_scitt.py szl_dsse.py szl_provenance.py szl_be_hardening.py szl_unay.py szl_khipu_lmdb.py szl_khipu_replicate.py szl_unay_routes.py szl_warhacker_aliases.py a11oy_v4_hickok.py szl_khipu.py szl_formulas.py a11oy_v4_formulas.py szl_anatomy_3d.py szl_anatomy_routes.py _vendor_blobs.py szl_v4_fleet.py operator_shell_v4.py szl_bridge.py szl_bridge_schemas.py agent.html a11oy_bridge_cli.py szl_ken.py a11oy_formula_endpoints.py a11oy_formulas_page.py a11oy_frontier_patch.py a11oy_v4_agent.py szl_brain.py szl_wire.py szl_hub.py szl_rosie_companion.py szl_receipt_substrate.py szl_alloy_embed_fabric.py szl_ayni_quorum.py szl_agentic_loop.py szl_formula_wiring.py szl_formula_surfaces.py a11oy_code_engine.py a11oy_code.py a11oy_seismic.py szl_warhacker_real.py szl_warhacker_demos.py NOTICE_warhacker_demos.txt szl_llm_registry.py szl_elite_console.py szl_alloy_models.py szl_scaling.py szl_allodial.py szl_entanglement.py szl_neuroplasticity.py szl_chain_of_title.py szl_sovereign_compute.py a11oy_active_flux_router.py szl_energy_budget.py szl_energy_sovereign.py szl_energy_provenance.py szl_heart_blood.py szl_engine_status.py szl_backend_hardening.py revenue_endpoints.py a11oy_harvest_endpoints.py joule_billing.py szl_energy_ledger.py szl_energy_operator.py szl_energy_projection.py szl_cheapest_watt.py szl_energy_live.py szl_orbital_topology.py szl_orbital_projection.py a11oy_orbital_page.py a11oy_frontier_page.py szl_frontier_manifest.py a11oy_code_as_action.py a11oy_governed_kernel.py szl_lambda_tripwire.py szl_provenance_receipt.py szl_khipu_verify.py szl_attest_stack.py szl_demo_sign.py szl_sda.py szl_fabric_surface.py szl_nemo_agents.py szl_kverify.py szl_specdec.py szl_immune.py szl_quant_qbio_holo.py szl_materials.py szl_materials_predict.py a11oy_factory.py a11oy_constitution.py a11oy_nav_wireup.py szl_mbse_cosim.py szl_mbse_nav.py szl_mbse.py szl_factory.py szl_willay_gateway.py a11oy_willay_nav.py szl_waqay.py a11oy_waqay_nav.py szl_yupay.py a11oy_yupay_nav.py a11oy_uds_portability_nav.py szl_pinn_bounds.py physical_bounds_certificate.json agentic_decision_trail.json physical_bounds_certificate.dsse.json szl_pinn_inverse.py szl_governed_ipinn.py szl_calphad_inverse.py szl_pnt_mesh.py quantum_sensing_limits.py pnt_resilience.py nav_coasting.py fundamental_limits.py szl_counter_uas_proxy.py szl_gpu_quant.py szl_joules_truth.py revenue_model.py szl_prod_hardening.py szl_resilience.py szl_observability.py szl_corpus_publish.py szl_lake_store.py szl_lake_ingest.py szl_e8.py szl_trajectory_sign.py szl_nemotron_ingest.py szl_nemotron_corpus.py szl_nemo_verify.py a11oy_nemo_core.py szl_restraint.py szl_sapa.py szl_sapa_patch.py szl_restraint_energy.py a11oy_react_core.py szl_org_lambda.py a11oy_canonical_domain.py a11oy_formula_tiers.py ./
 
 # DEV2 Build 1: TEE/TDX attestation hook (2026-06-30) — imported by serve.py (guarded);
 # MUST be per-file COPY'd or /api/a11oy/v1/tee/status + tee_attestation receipt field

a11oy_canonical_domain.py

@@ -0,0 +1,39 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+# (c) 2026 Lutar, Stephen P. - SZL Holdings - ORCID 0009-0001-0110-4173
+"""
+a11oy_canonical_domain.py — make a-11-oy.com the single canonical host.
+
+a11oy.net is SUNSET. This installs an app-level 301 redirect so any request whose
+Host header is a11oy.net (or www.a11oy.net) is permanently redirected to the same
+path+query on https://a-11-oy.com. The canonical HF Space host
+(szlholdings-a11oy.hf.space), localhost, and a-11-oy.com itself are passed through
+untouched, so the app keeps working on its origin while the public URL converges.
+
+This is a READ-PATH-SAFE redirect: it is a pure 308/301 Location response, mints no
+receipt, signs nothing, and touches no state (provenance rule: never sign on a read
+path). Doctrine-safe: try/except-guarded register(app).
+"""
+
+CANONICAL_HOST = "a-11-oy.com"
+
+# Hosts that should be permanently redirected to the canonical host.
+SUNSET_HOSTS = {"a11oy.net", "www.a11oy.net"}
+
+
+def register(app):
+    """Install the a11oy.net -> a-11-oy.com 301 redirect middleware. Returns a status list."""
+    from starlette.responses import RedirectResponse
+
+    @app.middleware("http")
+    async def _canonical_host_redirect(request, call_next):
+        host = (request.headers.get("host") or "").split(":")[0].lower()
+        if host in SUNSET_HOSTS:
+            target = f"https://{CANONICAL_HOST}{request.url.path}"
+            if request.url.query:
+                target = f"{target}?{request.url.query}"
+            # 301: permanent. The sunset host must never be presented as canonical.
+            return RedirectResponse(url=target, status_code=301)
+        return await call_next(request)
+
+    return [f"301 {h} -> https://{CANONICAL_HOST}" for h in sorted(SUNSET_HOSTS)]

a11oy_formula_tiers.py

@@ -0,0 +1,144 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+# (c) 2026 Lutar, Stephen P. - SZL Holdings - ORCID 0009-0001-0110-4173
+"""
+a11oy_formula_tiers.py — canonical, honest 4-tier proof registry for the locked-8
+formulas and the real trust-math theorems that sit *outside* the locked baseline.
+
+This is the single source of truth for what each Lean obligation ACTUALLY proves.
+It exists because the historical console copy described the locked-8 with semantic
+governance meanings (F18 "DSSE seal", F19 "13-axis Λ geomean", F1 "gate-pass ⇒
+Λ≥0.90", …) and cited anchor files (Lutar/Soundness.lean, STL.lean, Gates.lean,
+Receipt.lean, Lambda.lean) that DO NOT EXIST in lutar-lean. The locked-8 in
+Lutar/Puriq/Formulas/ProvedFormulas.lean prove conservative Nat/Int surrogates;
+labelling them with the governance semantics they merely *motivate* is overclaiming.
+
+The four tiers (verify-it-yourself, never overclaim):
+  1. LOCKED-PROVEN     — in the no-axiom `locked_count_eight` baseline (Wave11),
+                         labelled with WHAT IT ACTUALLY PROVES.
+  2. SEMANTIC-VERIFIED — sorry-free real theorem proving a governance property, but
+                         NOT in the locked-8 set. This is where the real trust math
+                         lives; present it proudly, but distinctly from the baseline.
+  3. evidence-backed   — real runtime/algorithmic code, no Lean proof claim.
+  4. CONJECTURE        — Λ unconditional uniqueness (machine-checked FALSE as stated),
+                         Khipu BFT safety/liveness. Gray, NEVER green.
+
+Pure-Python STDLIB only. Doctrine-safe: try/except-guarded register(app); the route
+is pushed to the FRONT of app.router.routes so it wins over the Node proxy and SPA
+catch-all. Λ = Conjecture 1 (NEVER a theorem). 0 runtime CDN. No key, no signing.
+"""
+
+# lutar-lean files verified MISSING at depth-1 clone (2026-06-30). Never cite as anchors.
+PHANTOM_ANCHORS = [
+    "Lutar/Soundness.lean", "Lutar/STL.lean", "Lutar/Gates.lean",
+    "Lutar/Receipt.lean", "Lutar/Lambda.lean",
+]
+
+# Tier 1 — LOCKED-PROVEN. The no-axiom `locked_count_eight` baseline
+# (Lutar/Wave11/AxiomDisclosure.lean:96-100). Conservative surrogates in
+# Lutar/Puriq/Formulas/ProvedFormulas.lean (which also has 4 sorries OUTSIDE the
+# locked-8 — those 4 are NOT these theorems). Labels = what each ACTUALLY proves.
+LOCKED_PROVEN = [
+    {"id": "F1", "proves": "Replay-hash determinism — identical canonical input ⇒ identical receipt hash.",
+     "not": "NOT 'gate-pass ⇒ Λ ≥ 0.90'.",
+     "lean_file": "Lutar/Puriq/Formulas/ProvedFormulas.lean", "lean_name": "f1_replay_hash_determinism"},
+    {"id": "F4", "proves": "Khipu DAG acyclicity preserved under append.",
+     "not": None,
+     "lean_file": "Lutar/Puriq/Formulas/ProvedFormulas.lean", "lean_name": "f4_khipu_dag_acyclic_preserved"},
+    {"id": "F7", "proves": "Chaski FIFO ordering preserved.",
+     "not": None,
+     "lean_file": "Lutar/Puriq/Formulas/ProvedFormulas.lean", "lean_name": "f7_chaski_fifo_order"},
+    {"id": "F11", "proves": "Ayni reciprocity conservation — b + c balance over Int.",
+     "not": "NOT 'STL robustness ρ envelope'.",
+     "lean_file": "Lutar/Puriq/Formulas/ProvedFormulas.lean", "lean_name": "f11_ayni_reciprocity_conservation"},
+    {"id": "F12", "proves": "Kuramoto additive (p1 + p2 over k phases) — additivity, by decide.",
+     "not": "NOT 'deny-by-default gate monotonicity'.",
+     "lean_file": "Lutar/Puriq/Formulas/ProvedFormulas.lean", "lean_name": "f12_kuramoto_additive"},
+    {"id": "F18", "proves": "Reed-Solomon parity count — (10-6 : Nat) = 4, erasure-tolerance arithmetic, by decide.",
+     "not": "NOT 'DSSE seal binds canonical payload'.",
+     "lean_file": "Lutar/Puriq/Formulas/ProvedFormulas.lean", "lean_name": "f18_reed_solomon_parity_count"},
+    {"id": "F19", "proves": "Bekenstein additive — s1 ≤ s1 + s2, entropy-budget monotonicity over Nat.",
+     "not": "NOT '13-axis Λ geometric-mean aggregate'.",
+     "lean_file": "Lutar/Puriq/Formulas/ProvedFormulas.lean", "lean_name": "f19_bekenstein_additive"},
+    {"id": "F22", "proves": "Khipu emit append-only monotonicity.",
+     "not": None,
+     "lean_file": "Lutar/Puriq/Formulas/ProvedFormulas.lean", "lean_name": "f22_khipu_emit_monotone"},
+]
+
+# Tier 2 — SEMANTIC-VERIFIED. Sorry-free real theorems (except where a residual sorry
+# is disclosed) that prove the governance property, OUTSIDE the locked-8. This is the
+# real trust math: present proudly as "machine-checked, outside the frozen baseline."
+SEMANTIC_VERIFIED = [
+    {"id": "Λ-bound-max", "proves": "Λ ≤ max(axes) — aggregate upper bound. 0 sorries.",
+     "lean_file": "Lutar/Bound.lean", "lean_name": "Λ_le_max", "sorries": 0},
+    {"id": "Λ-bound-min", "proves": "min(axes) ≤ Λ — aggregate lower bound. 0 sorries.",
+     "lean_file": "Lutar/Bound.lean", "lean_name": "min_le_Λ", "sorries": 0},
+    {"id": "Λ-normalize", "proves": "Λ definition + axis normalization well-formed. 0 sorries.",
+     "lean_file": "Lutar/Invariant.lean", "lean_name": "a3_normalize_proof", "sorries": 0},
+    {"id": "Theorem-U", "proves": "Λ uniqueness CONDITIONAL on separability (the honest, proven conditional).",
+     "lean_file": "Lutar/Round13/LambdaSeparable.lean", "lean_name": "lambda_unique_of_separable", "sorries": 0},
+    {"id": "robustness", "proves": "STL/adversarial robustness preserved under composition.",
+     "lean_file": "Lutar/Composition/AdversarialRobustness.lean", "lean_name": "robustness_preserved_by_composition", "sorries": 0},
+    {"id": "F14-DSSE", "proves": "DSSE verifiability — under DISCLOSED axiom ecdsa_unforgeable.",
+     "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean", "lean_name": "f14_dsse_verifiable", "sorries": 0,
+     "axiom": "ecdsa_unforgeable (disclosed)"},
+    {"id": "receipt-transduction", "proves": "Receipt transduction invariant (receipts.in ≡ receipts.out).",
+     "lean_file": "Lutar/Transduction/ReceiptInvariant.lean", "lean_name": "receipt_transduction_invariant", "sorries": 1},
+]
+
+# Tier 4 — CONJECTURE / ADVISORY. Gray, NEVER green. The canonical Λ is a 13-axis
+# weighted geometric mean, advisory, floor 0.90 — its unconditional uniqueness is FALSE
+# as stated (machine-checked). Theorem U above is the proven *conditional* (Tier 2).
+CONJECTURE = [
+    {"id": "Conjecture-1", "claim": "Λ unconditional uniqueness.",
+     "status": "machine-checked FALSE as stated; Theorem U is the proven conditional.", "color": "gray"},
+    {"id": "Conjecture-2", "claim": "Khipu BFT safety.", "status": "conjecture, never proven.", "color": "gray"},
+    {"id": "Conjecture-3", "claim": "Khipu BFT liveness.", "status": "conjecture, never proven.", "color": "gray"},
+]
+
+LAMBDA = {
+    "definition": "13-axis weighted geometric mean",
+    "role": "advisory",
+    "floor": 0.90,
+    "bounds": "SEMANTIC-VERIFIED (Λ_le_max / min_le_Λ, 0 sorries)",
+    "uniqueness": "Theorem U conditional (SEMANTIC-VERIFIED) / Conjecture 1 unconditional (machine-checked FALSE)",
+}
+
+TIERS = {
+    "model": "4-tier honesty model (RECONCILE.md, binding)",
+    "locked_count": 8,
+    "locked_ids": [f["id"] for f in LOCKED_PROVEN],
+    "locked_theorem": "locked_count_eight (no-axiom, Lutar/Wave11/AxiomDisclosure.lean:96-100)",
+    "phantom_anchors_never_cited": PHANTOM_ANCHORS,
+    "lambda": LAMBDA,
+    "tiers": {
+        "LOCKED-PROVEN": LOCKED_PROVEN,
+        "SEMANTIC-VERIFIED": SEMANTIC_VERIFIED,
+        "evidence-backed": [{"note": "runtime/algorithmic rules with real code, no Lean proof claim."}],
+        "CONJECTURE": CONJECTURE,
+    },
+    "honest": ("Every locked-8 entry is labelled with what its Lean obligation ACTUALLY proves "
+               "(conservative Nat/Int surrogates), NOT the governance semantics it motivates. "
+               "The real trust math (Λ bounds, Theorem U conditional, DSSE verifiability) is "
+               "SEMANTIC-VERIFIED, machine-checked OUTSIDE the frozen locked-8. Conjectures are "
+               "gray and NEVER rendered green. Verify it yourself: clone lutar-lean, open the "
+               "cited file, count the sorries."),
+}
+
+
+def register(app):
+    """Mount GET /api/a11oy/v1/formula-tiers at the FRONT of the router. Returns route list."""
+    from fastapi.responses import JSONResponse
+    added = []
+
+    @app.get("/api/a11oy/v1/formula-tiers")
+    async def _a11oy_formula_tiers():
+        return JSONResponse(TIERS)
+
+    try:
+        r = app.router.routes.pop()
+        app.router.routes.insert(0, r)
+    except Exception:
+        pass
+    added.append("/api/a11oy/v1/formula-tiers")
+    return added

a11oy_wireA_metrics.py

@@ -401,12 +401,12 @@ def register(app):
 
     # ---- SQLite FTS5 search over an in-image governance corpus -------------------------
     _FTS_CORPUS = [
-        ("F1", "soundness gate-pass implies Λ ≥ 0.90 conjunctive soundness locked-proven"),
-        ("F11", "STL signal temporal logic robustness rho envelope geofence gates locked-proven"),
-        ("F12", "monotone policy gate deny-by-default monotonicity locked-proven"),
-        ("F18", "DSSE seal receipt signature binds canonical payload tamper-evident locked-proven"),
-        ("F19", "Λ aggregate 13-axis geometric mean trust advisory locked-proven"),
-        ("F23", "Λ uniqueness conditional slice multiplicativity axiom-free conjecture-1 unconditional"),
+        ("F1", "replay-hash determinism identical canonical input yields identical receipt hash locked-proven"),
+        ("F11", "Ayni reciprocity conservation balance over Int locked-proven"),
+        ("F12", "Kuramoto additive phase additivity locked-proven"),
+        ("F18", "Reed-Solomon parity count erasure tolerance arithmetic locked-proven"),
+        ("F19", "Bekenstein additive entropy budget monotonicity locked-proven"),
+        ("Lambda", "13-axis weighted geometric mean advisory floor 0.90 bounds SEMANTIC-VERIFIED uniqueness Conjecture-1 unconditional FALSE Theorem-U conditional"),
         ("organism", "living organism organ topology Reception Operator Provenance-Anchor Policy"),
         ("chain", "receipt hash-chain Khipu DSSE ledger locked-8 aggregate"),
         ("threat", "attack surface zero-trust path ingress auth-gate policy-gate egress"),
@@ -462,9 +462,11 @@ def register(app):
             "kind": kind, "p": p, "axes": xs, "variants": variants,
             "am_gm_hm_ordering_holds": ordered,
             "maturity": "Λ = Conjecture 1 (advisory, never a theorem)",
-            "lean": "Lutar/Lambda.lean::lambda_geomean_wellformed (F19, locked-proven well-formedness only)",
-            "honest": "Quasi-arithmetic (Kolmogorov–Nagumo) mean family. Λ generator = geometric (F19). "
-                      "Uniqueness is Conjecture 1 (machine-checked FALSE unconditionally).",
+            "lean": "Bounds SEMANTIC-VERIFIED: Lutar/Bound.lean::Λ_le_max, ::min_le_Λ (0 sorries). "
+                    "Uniqueness conditional: Lutar/Round13/LambdaSeparable.lean::lambda_unique_of_separable (Theorem U). "
+                    "F19 locked-proven theorem = f19_bekenstein_additive (entropy-budget monotonicity, NOT the Λ aggregate).",
+            "honest": "Quasi-arithmetic (Kolmogorov–Nagumo) mean family; canonical Λ = 13-axis weighted geometric mean. "
+                      "Unconditional uniqueness is Conjecture 1 (machine-checked FALSE); Theorem U is the proven conditional.",
             "note": NOTE,
         })
     _front("/api/a11oy/v1/wirea/lambda/panel")

serve.py

@@ -10595,6 +10595,42 @@ except Exception as _wirea_e:
 # END: DEV-WIRE-A metrics layer
 # ============================================================================
 
+# ============================================================================
+# Canonical honest 4-tier formula registry (LOCKED-PROVEN truthful labels +
+# SEMANTIC-VERIFIED tier + CONJECTURE gray). Single source of truth for what
+# each Lean obligation ACTUALLY proves; replaces the historical overclaiming
+# console copy. Per-file COPY in Dockerfile (no COPY . .). Λ = Conjecture 1.
+# ============================================================================
+try:
+    import a11oy_formula_tiers as _ftiers_mod
+    import sys as _ftiers_sys
+    _ftiers_status = _ftiers_mod.register(app)
+    print(f"[a11oy] formula-tiers registered ({len(_ftiers_status)} routes): {_ftiers_status}", file=_ftiers_sys.stderr)
+    _A11OY_FTIERS_DIAG = {"status": "ok", "routes": _ftiers_status}
+except Exception as _ftiers_e:
+    import sys as _ftiers_sys, traceback as _ftiers_tb
+    print(f"[a11oy] formula-tiers FAILED (non-fatal): {_ftiers_e!r}", file=_ftiers_sys.stderr)
+    _ftiers_tb.print_exc(file=_ftiers_sys.stderr)
+    _A11OY_FTIERS_DIAG = {"status": "FAILED", "error": repr(_ftiers_e)}
+
+# ============================================================================
+# Canonical host: a-11-oy.com. a11oy.net is SUNSET — app-level 301 redirect so the
+# public URL converges on a-11-oy.com. Read-path-safe (pure Location response, no
+# receipt, no signing). Registered before uvicorn.run so the middleware stack is
+# built with it; passes through the HF Space host + localhost untouched.
+# ============================================================================
+try:
+    import a11oy_canonical_domain as _canon_mod
+    import sys as _canon_sys
+    _canon_status = _canon_mod.register(app)
+    print(f"[a11oy] canonical-domain registered ({len(_canon_status)} redirects): {_canon_status}", file=_canon_sys.stderr)
+    _A11OY_CANON_DIAG = {"status": "ok", "redirects": _canon_status}
+except Exception as _canon_e:
+    import sys as _canon_sys, traceback as _canon_tb
+    print(f"[a11oy] canonical-domain FAILED (non-fatal): {_canon_e!r}", file=_canon_sys.stderr)
+    _canon_tb.print_exc(file=_canon_sys.stderr)
+    _A11OY_CANON_DIAG = {"status": "FAILED", "error": repr(_canon_e)}
+
 # ============================================================================
 # SOVEREIGN COMPUTE single-pane (#320): ADDITIVE, pure-stdlib, try/except-guarded.
 # Honest single-pane readiness for the sovereign-AI substrate — each capability