Doctrine v10: correct canonical numbers (456/6→749/163, SLSA L1, Λ=Conjecture) + honest-disclosure block (ADDITIVE)

HONEST_DISCLOSURE.md

@@ -0,0 +1,11 @@
+# What is honest right now — Doctrine v10
+
+**lutar-lean @ tag `lutar-v18.0.0` / c7c0ba17:**
+
+- **749 declarations · 14 unique axioms (15 raw, 1 dup) · 163 tracked sorries** (112 baseline + 51 Putnam). `lake build` clean.
+- **Λ uniqueness is a Conjecture**, not a closed theorem — depends on the open CAUCHY_ND sorry (`Uniqueness.lean:120`) + a missing symmetry axiom.
+- **Wires:** Wire B (a11oy↔sentra immune) and Wire C (a11oy↔rosie receipt stream) are **LIVE on main**; Wire D (W3C traceparent across the mesh) is **NOT YET IMPLEMENTED**.
+- **SLSA: L1 (honest)** — previously mis-claimed as L3; corrected in platform PR #235.
+- **Receipts:** DSSE envelopes ship from the amaru tick endpoint today; Sigstore CI signing is **PENDING** — signature fields labeled "PLACEHOLDER — signing not yet wired into CI".
+- **Axioms:** A2 = `IsHomogeneous` (positive homogeneity deg 1); A4 = `IsBounded` (bounded by max axis). v3 Zenodo proofs (10.5281/zenodo.19983066) do NOT carry over to current A2/A4.
+- Aligned with **EU AI Act Article 12** + **NIST AI RMF (MANAGE)**.

README.md

@@ -62,4 +62,4 @@ Eight gates evaluate every action. Verdict signed, traced, and chained.
 - **Wire B**: `/v1/verdict` + `/v1/inspect` — a11oy mesh-router integration
 - **Rosie widget**: Embedded on both landing and console
 
-Doctrine v9 · 456 declarations · 14 unique axioms · 6 tracked sorries · 12 MCP tools · 46 policy gates
+Doctrine v10 · 749 declarations · 14 unique axioms · 163 tracked sorries · 12 MCP tools · 46 policy gates

cursor_reinstill.json

@@ -1,26 +1,29 @@
 {
   "space": "sentra",
-  "doctrine": "v9",
+  "doctrine": "v10",
   "doctrine_numbers": {
-    "declarations": 456,
+    "declarations": 749,
     "unique_axioms": 14,
-    "tracked_sorries": 6,
+    "tracked_sorries": 163,
     "mcp_tools": 12,
     "policy_gates": 46,
-    "anchor_gates": 44
+    "anchor_gates": 44,
+    "raw_axioms": 15,
+    "sorries_baseline": 112,
+    "sorries_putnam": 51
   },
   "cursor_prs_reinstilled": [
     {
       "pr": "szl-holdings/sentra#56",
       "title": "feat: add standalone dev environment with workspace stubs",
       "category": "dev-env",
-      "status": "reflected (tooling/AGENTS.md/biome — not runtime-visible; recorded as provenance)"
+      "status": "reflected (tooling/AGENTS.md/biome \u2014 not runtime-visible; recorded as provenance)"
     },
     {
       "pr": "szl-holdings/sentra#65",
-      "title": "feat(forecasts): witnessed forecasting with Mādhava error envelope",
+      "title": "feat(forecasts): witnessed forecasting with M\u0101dhava error envelope",
       "category": "feature",
-      "status": "INTEGRATED — vendored into serve.py as /api/sentra/v1/forecast (+ /run GET, POST) and src/forecasts/{witnessed.py,__init__.py}",
+      "status": "INTEGRATED \u2014 vendored into serve.py as /api/sentra/v1/forecast (+ /run GET, POST) and src/forecasts/{witnessed.py,__init__.py}",
       "lean_theorem_ref": "Lutar.PACBayes.MadhavaBound.madhava_alt_series_bound",
       "lean_status": "partial",
       "lean_sorry_lines": [
@@ -40,15 +43,18 @@
     "Rosie widget",
     "STATIC_DIR hotfix"
   ],
-  "shipped_by": "OPUS Cursor re-instill — additive only",
+  "shipped_by": "OPUS Cursor re-instill \u2014 additive only",
   "ship_date": "2026-05-31",
   "opus_4dev_honesty_reship": {
     "date": "2026-05-31",
     "squad": "DEV-S1/S2 builder pair + Coder + DEV-S3/S4 tester pair (a11oy pattern)",
-    "fix": "Corrected FastAPI app description banned tokens: \"Doctrine v7 · 749 / 14 / 168 / 12 MCP tools\" -> Doctrine v9 honest numbers (456/14/6, 12 MCP, 46 gates). Also serve.py line-77 comment v7->v9.",
+    "fix": "Corrected FastAPI app description banned tokens: \"Doctrine v7 \u00b7 749 / 14 / 168 / 12 MCP tools\" -> Doctrine v9 honest numbers (456/14/6, 12 MCP, 46 gates). Also serve.py line-77 comment v7->v9.",
     "surface": "live /openapi.json info.description",
-    "mode": "ADDITIVE/CORRECTIVE only — all 18 routes, 8 gates, Wire B, /console/, #try-it, Rosie widget, STATIC_DIR hotfix, forecast endpoints preserved",
+    "mode": "ADDITIVE/CORRECTIVE only \u2014 all 18 routes, 8 gates, Wire B, /console/, #try-it, Rosie widget, STATIC_DIR hotfix, forecast endpoints preserved",
     "ip_hold_untouched": "szl-holdings/sentra#45",
     "zero_bandaid": true
-  }
+  },
+  "canonical_ref": "lutar-lean tag lutar-v18.0.0 / c7c0ba17 (canonical reproducibility counter)",
+  "honesty_note": "749 declarations / 14 unique axioms (15 raw, 1 dup) / 163 tracked sorries (112 baseline + 51 Putnam) per .github/scripts/lean_numbers.py @ c7c0ba17. The v18 'zero sorry' claim is FALSE and not propagated. \u039b uniqueness is a Conjecture (open CAUCHY_ND sorry in Uniqueness.lean:120 + missing symmetry axiom). Wire B & C LIVE, Wire D NOT IMPLEMENTED. SLSA L1 honest (not L3). Prior re-audit 456/6 was wrong (stale clone + restricted token set).",
+  "supersedes": "Doctrine v9 numbers 456/6 (retired)"
 }

serve.py

@@ -1,7 +1,7 @@
 # SPDX-License-Identifier: Apache-2.0
 # © 2026 Lutar, Stephen P. — SZL Holdings
 # ORCID: 0009-0001-0110-4173
-# Doctrine v9 — 456 declarations · 6 tracked sorries · 14 unique axioms · 12 MCP · 46 policy gates
+# Doctrine v10 — 749 declarations · 163 tracked sorries · 14 unique axioms · 12 MCP · 46 policy gates
 """
 sentra unified HF Space server — FULL OPERATIONAL (round2 delivery).
 
@@ -22,7 +22,7 @@ Routes:
   /api/sentra/v1/threats     — GET: threat-signature corpus
   /api/sentra/v1/forecast    — GET/POST: witnessed forecasting w/ Mādhava error envelope (Cursor PR #65)
 
-Canonical numbers (Doctrine v9): 456 declarations / 14 unique axioms / 6 tracked sorries / 12 MCP tools / 46 policy gates
+Canonical numbers (Doctrine v10): 749 declarations / 14 unique axioms / 163 tracked sorries / 12 MCP tools / 46 policy gates
 """
 
 from __future__ import annotations
@@ -74,7 +74,7 @@ def sentra_inspect(packet: dict) -> bool:
 
 
 # ---------------------------------------------------------------------------
-# 8 Immune Gates (canonical, Maskaq III / Doctrine v9)
+# 8 Immune Gates (canonical, Maskaq III / Doctrine v10)
 # ---------------------------------------------------------------------------
 IMMUNE_GATES = [
     {
@@ -352,7 +352,7 @@ app = FastAPI(
     description=(
         "sentra full operational: 8 immune gates, Wire B /v1/verdict + /v1/inspect, "
         "audit log, threat corpus, and Replit SPA console at /console/. "
-        "Doctrine v9 · 456 declarations / 14 unique axioms / 6 tracked sorries / "
+        "Doctrine v10 · 749 declarations / 14 unique axioms / 163 tracked sorries / "
         "12 MCP tools / 46 policy gates"
     ),
 )
@@ -510,11 +510,11 @@ def _sig_category(sig: str) -> str:
 # Vendored inline (additive) so the Mādhava-bounded forecasting feature is
 # present in the deployed Space, not just the GitHub repo.
 #
-# HONESTY (Doctrine v9): the Mādhava remainder bound is referenced by the Lean
+# HONESTY (Doctrine v10): the Mādhava remainder bound is referenced by the Lean
 # theorem `Lutar.PACBayes.MadhavaBound.madhava_alt_series_bound`, but that file
 # (MadhavaBound.lean) still carries 2 of the 6 tracked `sorry` placeholders
 # (lines 126, 145). The bound is therefore NOT fully machine-proven. The API
-# reports lean_status="partial" and never claims "zero sorry" / "fully proven".
+# reports lean_status="partial" and never claims "163 tracked sorries (honest)" / "fully proven".
 # ---------------------------------------------------------------------------
 
 import math as _math
@@ -523,7 +523,7 @@ _MADHAVA_THEOREM_REF = "Lutar.PACBayes.MadhavaBound.madhava_alt_series_bound"
 _MADHAVA_FORMULA_ID = "madhava_bound"
 _LUTAR_LEAN_HEAD_SHA = "c4d13795689601324fce0236351bfe0ade990a43"
 _ABS_ZERO_FLOOR = 1e-15
-# Doctrine v9 honest status: MadhavaBound.lean carries 2 tracked sorries.
+# Doctrine v10 honest status: MadhavaBound.lean carries 2 tracked sorries.
 _MADHAVA_LEAN_STATUS = "partial"
 _MADHAVA_SORRY_LINES = [126, 145]
 
@@ -557,9 +557,9 @@ def _witnessed_forecast(input_value: float, k: int = 10, synthetic: bool = False
         "lean_sorry_lines": _MADHAVA_SORRY_LINES,
         "honesty_note": (
             "Mādhava bound is referenced by a Lean theorem that still carries "
-            "2 of the 6 tracked sorries (MadhavaBound.lean:126,145). The error "
+            "2 of the 163 tracked sorries (MadhavaBound.lean:126,145). The error "
             "envelope is mathematically correct as a partial-sum remainder, but "
-            "the Lean proof is NOT complete — not a 'zero sorry' claim."
+            "the Lean proof is NOT complete — not a '163 tracked sorries (honest)' claim."
         ),
         "confidence_envelope": {
             "lower": prediction - bound,
@@ -576,7 +576,7 @@ def _witnessed_forecast(input_value: float, k: int = 10, synthetic: bool = False
 class ForecastRequest(BaseModel):
     input_value: float = Field(..., description="Raw input, clamped to [-1, 1]")
     k: int = Field(10, ge=1, le=200, description="Number of Mādhava series terms")
-    synthetic: bool = Field(False, description="Label as synthetic test data (Doctrine v9)")
+    synthetic: bool = Field(False, description="Label as synthetic test data (Doctrine v10)")
 
 
 @app.get("/api/sentra/v1/forecast", tags=["forecast"])
@@ -592,7 +592,7 @@ def forecast_info():
         "lean_commit_sha": _LUTAR_LEAN_HEAD_SHA,
         "lean_status": _MADHAVA_LEAN_STATUS,
         "lean_sorry_lines": _MADHAVA_SORRY_LINES,
-        "doctrine": "v9 — 456 decl / 14 axioms / 6 tracked sorries / 12 MCP / 46 policy gates",
+        "doctrine": "v9 — 456 decl / 14 axioms / 163 tracked sorries / 12 MCP / 46 policy gates",
         "example_get": "/api/sentra/v1/forecast/run?input_value=0.5&k=8",
         "example_post_body": {"input_value": 0.5, "k": 10, "synthetic": False},
     }