FIX: honest proven count + Live System Map redesign (service-health dashboard)

packages/a11oy-knowledge/src/knowledge.json

@@ -1,10 +1,10 @@
 {
-  "version": "1.0.0",
+  "version": "5.1.0",
   "byline": "Lutar, Stephen P.",
   "orcid": "0009-0001-0110-4173",
   "email": "stephen@szlholdings.com",
   "org": "SZL Holdings",
-  "generated_at": "2026-05-15T16:30:00Z",
+  "generated_at": "2026-06-06T06:00:00Z",
   "axioms": [
     {
       "id": "A1",
@@ -92,9 +92,9 @@
     {
       "id": "TH_L1",
       "name": "\u039b_uniqueness",
-      "statement": "The Lutar Invariant \u039b_k as weighted geometric mean with Egyptian unit-fraction weights is unique given the four axioms",
-      "source_file": "lutar-lean/Lutar/Uniqueness.lean",
-      "maturity": "proven",
+      "statement": "Conjecture 1: the Lutar Invariant \u039b_k (weighted geometric mean with Egyptian unit-fraction weights) is the unique aggregator satisfying axioms A1-A5. NOT a theorem: unconditional uniqueness is FALSE under A1-A5 (machine-checked counterexample maxAgg_ne_Lambda; max-aggregator satisfies A1-A5 yet differs from \u039b at (4,1)). The conditional theorem lambda_unique_of_factors (uniqueness GIVEN factorization \u03a6 x = \u220f x_i^\u03b1_i) IS fully proved; unconditional uniqueness closes only under a declared bisymmetry axiom A6 (Kolmogorov-Nagumo-Aczel).",
+      "source_file": "lutar-lean/Lutar/Round13/Lambda_Uniqueness.lean",
+      "maturity": "conjectured",
       "citation": "https://doi.org/10.5281/zenodo.20053148"
     },
     {
@@ -129,7 +129,8 @@
       "source_line": 27,
       "latex": "\\mathcal{S} = \\langle R, A, E, \\Lambda, \\rho, W \\rangle",
       "context": "ith a doctrine-locked runtime** as a category-defining primitive for verifiable agency. We define the system as a tuple \\( \\mathcal{S} = \\langle R, A, E, \\Lambda, \\rho, W \\rangle \\) over an eight-regi",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0002",
@@ -137,7 +138,8 @@
       "source_line": 229,
       "latex": "\\mathtt{szl\\text{-}trust}",
       "context": "d system.  - \\(A\\) \u2014 the set of **named actors**. Every actor in \\(A\\) carries a stable identity resolvable to a key in \\(\\mathtt{szl\\text{-}trust}\\). No edge in \\(E\\) may originate from or terminate ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0003",
@@ -145,7 +147,8 @@
       "source_line": 231,
       "latex": "e \\in E",
       "context": "and resolvable \u2014 unidentified actors are structurally excluded.  - \\(E\\) \u2014 the set of **receipt-bound edges**. An edge \\(e \\in E\\) is a tuple \\((a_{\\text{src}},\\; r_{\\text{src}},\\; r_{\\text{dst}},\\; \\",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0004",
@@ -153,7 +156,8 @@
       "source_line": 231,
       "latex": "(a_{\\text{src}},\\; r_{\\text{src}},\\; r_{\\text{dst}},\\; \\varepsilon)",
       "context": "ntified actors are structurally excluded.  - \\(E\\) \u2014 the set of **receipt-bound edges**. An edge \\(e \\in E\\) is a tuple \\((a_{\\text{src}},\\; r_{\\text{src}},\\; r_{\\text{dst}},\\; \\varepsilon)\\) where \\(",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0005",
@@ -161,7 +165,8 @@
       "source_line": 231,
       "latex": "a_{\\text{src}} \\in A",
       "context": "d edges**. An edge \\(e \\in E\\) is a tuple \\((a_{\\text{src}},\\; r_{\\text{src}},\\; r_{\\text{dst}},\\; \\varepsilon)\\) where \\(a_{\\text{src}} \\in A\\), \\(r_{\\text{src}}, r_{\\text{dst}} \\in R\\), and \\(\\varep",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0006",
@@ -169,7 +174,8 @@
       "source_line": 231,
       "latex": "r_{\\text{src}}, r_{\\text{dst}} \\in R",
       "context": "E\\) is a tuple \\((a_{\\text{src}},\\; r_{\\text{src}},\\; r_{\\text{dst}},\\; \\varepsilon)\\) where \\(a_{\\text{src}} \\in A\\), \\(r_{\\text{src}}, r_{\\text{dst}} \\in R\\), and \\(\\varepsilon\\) is the receipt enve",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0007",
@@ -177,7 +183,8 @@
       "source_line": 231,
       "latex": "\\varepsilon",
       "context": "src}},\\; r_{\\text{dst}},\\; \\varepsilon)\\) where \\(a_{\\text{src}} \\in A\\), \\(r_{\\text{src}}, r_{\\text{dst}} \\in R\\), and \\(\\varepsilon\\) is the receipt envelope defined in \u00a73.3. No message may traverse",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0008",
@@ -185,7 +192,8 @@
       "source_line": 231,
       "latex": "\\varepsilon",
       "context": "repsilon\\) is the receipt envelope defined in \u00a73.3. No message may traverse a region boundary unless it carries a valid \\(\\varepsilon\\).  - \\(\\Lambda\\) \u2014 the **composable axis-gating function**. Forma",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0009",
@@ -193,7 +201,8 @@
       "source_line": 233,
       "latex": "\\Lambda",
       "context": "ceipt envelope defined in \u00a73.3. No message may traverse a region boundary unless it carries a valid \\(\\varepsilon\\).  - \\(\\Lambda\\) \u2014 the **composable axis-gating function**. Formally, \\(\\Lambda : [0,",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0010",
@@ -201,7 +210,8 @@
       "source_line": 233,
       "latex": "\\Lambda : [0,1]^k \\to \\{0,1\\}",
       "context": "boundary unless it carries a valid \\(\\varepsilon\\).  - \\(\\Lambda\\) \u2014 the **composable axis-gating function**. Formally, \\(\\Lambda : [0,1]^k \\to \\{0,1\\}\\) for \\(k \\geq 9\\), defined as the conjunctive A",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0011",
@@ -209,7 +219,8 @@
       "source_line": 233,
       "latex": "k \\geq 9",
       "context": "varepsilon\\).  - \\(\\Lambda\\) \u2014 the **composable axis-gating function**. Formally, \\(\\Lambda : [0,1]^k \\to \\{0,1\\}\\) for \\(k \\geq 9\\), defined as the conjunctive AND:  \\[ \\Lambda(\\mathbf{x}) = 1 \\iff \\",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0012",
@@ -217,7 +228,8 @@
       "source_line": 239,
       "latex": "\\mathbf{x}",
       "context": "bilityHonesty}} \\geq 0.95 \\]    The composability property states that for any two independently evaluated axis vectors \\(\\mathbf{x}\\) and \\(\\mathbf{y}\\), their composed gate \\(\\Lambda(\\mathbf{x} \\wed",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0013",
@@ -225,7 +237,8 @@
       "source_line": 239,
       "latex": "\\mathbf{y}",
       "context": "q 0.95 \\]    The composability property states that for any two independently evaluated axis vectors \\(\\mathbf{x}\\) and \\(\\mathbf{y}\\), their composed gate \\(\\Lambda(\\mathbf{x} \\wedge \\mathbf{y})\\) is",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0014",
@@ -233,7 +246,8 @@
       "source_line": 239,
       "latex": "\\Lambda(\\mathbf{x} \\wedge \\mathbf{y})",
       "context": "rty states that for any two independently evaluated axis vectors \\(\\mathbf{x}\\) and \\(\\mathbf{y}\\), their composed gate \\(\\Lambda(\\mathbf{x} \\wedge \\mathbf{y})\\) is equivalent to \\(\\Lambda(\\mathbf{x})",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0015",
@@ -241,7 +255,8 @@
       "source_line": 239,
       "latex": "\\Lambda(\\mathbf{x}) \\wedge \\Lambda(\\mathbf{y})",
       "context": "ctors \\(\\mathbf{x}\\) and \\(\\mathbf{y}\\), their composed gate \\(\\Lambda(\\mathbf{x} \\wedge \\mathbf{y})\\) is equivalent to \\(\\Lambda(\\mathbf{x}) \\wedge \\Lambda(\\mathbf{y})\\) \u2014 gate composition does not w",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0016",
@@ -249,7 +264,8 @@
       "source_line": 239,
       "latex": "\\Lambda",
       "context": "\u2014 gate composition does not weaken the invariant. The `lutar-lean` skeleton repository contains the Lean 4 statement of \\(\\Lambda\\) uniqueness: given the four axioms (A1 monotonicity, A2 homogeneity, ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "conjectured"
     },
     {
       "id": "F0017",
@@ -257,7 +273,8 @@
       "source_line": 239,
       "latex": "\\Lambda",
       "context": "ment of \\(\\Lambda\\) uniqueness: given the four axioms (A1 monotonicity, A2 homogeneity, A3 Egyptian-exact, A4 bounded), \\(\\Lambda\\) is the *unique* function satisfying them. The uniqueness theorem and",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "conjectured"
     },
     {
       "id": "F0018",
@@ -265,7 +282,8 @@
       "source_line": 241,
       "latex": "\\rho(e)",
       "context": "arget is zero.  - \\(\\rho\\) \u2014 the **dual-witness closure relation**. For any edge \\(e\\) carrying execution result \\(v\\), \\(\\rho(e)\\) holds iff two independent witnesses \\(w_1, w_2 \\in W\\) each produce ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0019",
@@ -273,7 +291,8 @@
       "source_line": 241,
       "latex": "w_1, w_2 \\in W",
       "context": "closure relation**. For any edge \\(e\\) carrying execution result \\(v\\), \\(\\rho(e)\\) holds iff two independent witnesses \\(w_1, w_2 \\in W\\) each produce byte-identical output on the same input, and the",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0020",
@@ -281,7 +300,8 @@
       "source_line": 251,
       "latex": "\\mathcal{S}",
       "context": "uroboros` core + 4 `a11oy` covenant), while the full upstream runtime suite registers 218/218 passing tests.  The tuple \\(\\mathcal{S}\\) is **doctrine-locked**: any runtime configuration in which (a) a",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0021",
@@ -289,7 +309,8 @@
       "source_line": 251,
       "latex": "\\Lambda",
       "context": "which (a) a region is unnamed, (b) an actor is not in \\(A\\), (c) an edge is produced without a receipt envelope, or (d) \\(\\Lambda\\) is evaluated below threshold does not constitute a valid instantiati",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0022",
@@ -297,7 +318,8 @@
       "source_line": 251,
       "latex": "\\mathcal{S}",
       "context": "ithout a receipt envelope, or (d) \\(\\Lambda\\) is evaluated below threshold does not constitute a valid instantiation of \\(\\mathcal{S}\\).  ---  ## The 8-Region Anatomy  The eight canonical regions of \\",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0023",
@@ -305,7 +327,8 @@
       "source_line": 257,
       "latex": "\\mathcal{S}",
       "context": "of \\(R\\) are enumerated below. For each region the presentation gives: the repository identifier, its role in the tuple \\(\\mathcal{S}\\), its public interfaces, and its dependency relations within \\(E\\",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0024",
@@ -313,7 +336,8 @@
       "source_line": 265,
       "latex": "\\mathcal{S}",
       "context": "released 2026-05-13; concept DOI `10.5281/zenodo.19944926`, v11 paper DOI `10.5281/zenodo.20119582`)  **Formal role in \\(\\mathcal{S}\\):** The Brain Stem is the runtime kernel that evaluates \\(\\Lambda\\",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0025",
@@ -321,7 +345,8 @@
       "source_line": 265,
       "latex": "\\Lambda",
       "context": "DOI `10.5281/zenodo.20119582`)  **Formal role in \\(\\mathcal{S}\\):** The Brain Stem is the runtime kernel that evaluates \\(\\Lambda\\) and emits receipts. Every edge in \\(E\\) that crosses a region bounda",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0026",
@@ -329,7 +354,8 @@
       "source_line": 268,
       "latex": "\\Lambda",
       "context": "bda(axes: number[9|10]) \u2192 Receipt` \u2014 evaluates the conjunctive AND gate and returns a signed receipt with the composite \\(\\Lambda\\) score, Bekenstein budget, and dual-witness closure status. - `build_",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "conjectured"
     },
     {
       "id": "F0027",
@@ -337,7 +363,8 @@
       "source_line": 274,
       "latex": "\\Lambda",
       "context": "chain root for third-party verification.  **Dependencies:** - Depends on: `lutar-lean` (Skeleton) \u2014 the axiom set that \\(\\Lambda\\) is required to satisfy is formally stated there; the Brain Stem is th",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0028",
@@ -345,7 +372,8 @@
       "source_line": 277,
       "latex": "\\Lambda_9",
       "context": "utbound edge must call `evaluate_lambda` before the edge enters \\(E\\).  The gate composition benchmark for v6.3.0 shows \\(\\Lambda_9\\) base p50 = 3.12 \u00b5s and composed p50 = 3.29 \u00b5s; with the Platform v",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0029",
@@ -353,7 +381,8 @@
       "source_line": 285,
       "latex": "\\mathcal{S}",
       "context": "a continuous supply-chain security posture.  ---  ### Heart \u2014 `a11oy`  **Repo:** `szl-holdings/a11oy`  **Formal role in \\(\\mathcal{S}\\):** The Heart is the covenant policy engine and the agent approva",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0030",
@@ -361,7 +390,8 @@
       "source_line": 285,
       "latex": "\\mathcal{S}",
       "context": "\\):** The Heart is the covenant policy engine and the agent approval queue. It governs the *authorization* dimension of \\(\\mathcal{S}\\): while the Brain Stem answers \"does this action score above \\(\\L",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0031",
@@ -369,7 +399,8 @@
       "source_line": 285,
       "latex": "\\Lambda",
       "context": "It governs the *authorization* dimension of \\(\\mathcal{S}\\): while the Brain Stem answers \"does this action score above \\(\\Lambda\\)?\", the Heart answers \"is this action permitted under the active cove",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0032",
@@ -377,7 +408,8 @@
       "source_line": 285,
       "latex": "r_{\\text{dst}} \\notin R",
       "context": "this action permitted under the active covenant?\". No action may exit the body graph \u2014 i.e., no edge in \\(E\\) may have \\(r_{\\text{dst}} \\notin R\\) \u2014 without a Heart pulse. The covenant is a named, ver",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0033",
@@ -385,39 +417,44 @@
       "source_line": 293,
       "latex": "\\Lambda",
       "context": "Stem's chain.  **Dependencies:** - Depends on: `ouroboros` (Brain Stem) \u2014 covenant evaluation results are sealed with a \\(\\Lambda\\)-gated receipt; a covenant check that fails \\(\\Lambda\\) is itself a g",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0034",
       "source_file": "thesis.md",
       "source_line": 293,
       "latex": "\\Lambda",
-      "context": "os` (Brain Stem) \u2014 covenant evaluation results are sealed with a \\(\\Lambda\\)-gated receipt; a covenant check that fails \\(\\Lambda\\) is itself a gate-level violation. - Depends on: `sentra` (Wires) \u2014 t",
-      "source_id": "thesis_session"
+      "context": "os` (Brain Stem) \u2014 covenant evaluation results are sealed with a \\(\\Lambda\\)-gated receipt; a covenant check that fails \\(\\Lambda\\) is itself a gate-level violation. - Depends on: `safety-gate layer` (safety wires) \u2014 t",
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0035",
       "source_file": "thesis.md",
       "source_line": 305,
       "latex": "\\mathcal{S}",
-      "context": "but a verifiable, chain-linked artifact.  ---  ### Wires \u2014 `sentra`  **Repo:** `szl-holdings/sentra`  **Formal role in \\(\\mathcal{S}\\):** The Wires are the attribution trail \u2014 the afferent channel tha",
-      "source_id": "thesis_session"
+      "context": "but a verifiable, chain-linked artifact.  ---  ### safety wires \u2014 `safety-gate layer`  **Repo:** `szl-holdings/safety-gate layer`  **Formal role in \\(\\mathcal{S}\\):** The safety wires are the attribution trail \u2014 the afferent channel tha",
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0036",
       "source_file": "thesis.md",
       "source_line": 305,
       "latex": "\\text{attr}: E \\to A",
-      "context": "rent channel that carries signals inward and records *who observed what and when*. Formally, Wires maintain the mapping \\(\\text{attr}: E \\to A\\), ensuring that every edge in \\(E\\) is attributable to a",
-      "source_id": "thesis_session"
+      "context": "rent channel that carries signals inward and records *who observed what and when*. Formally, safety wires maintain the mapping \\(\\text{attr}: E \\to A\\), ensuring that every edge in \\(E\\) is attributable to a",
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0037",
       "source_file": "thesis.md",
       "source_line": 305,
       "latex": "\\mathcal{S}",
-      "context": "he mapping \\(\\text{attr}: E \\to A\\), ensuring that every edge in \\(E\\) is attributable to a named actor. Without Wires, \\(\\mathcal{S}\\) degrades: edges carry receipts but not attributions, making the ",
-      "source_id": "thesis_session"
+      "context": "he mapping \\(\\text{attr}: E \\to A\\), ensuring that every edge in \\(E\\) is attributable to a named actor. Without safety wires, \\(\\mathcal{S}\\) degrades: edges carry receipts but not attributions, making the ",
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0038",
@@ -425,31 +462,35 @@
       "source_line": 308,
       "latex": "a \\in A",
       "context": "egal-accountability sense.  **Public interfaces:** - `observe(edge, actor_id) \u2192 AttributionRecord` \u2014 records that actor \\(a \\in A\\) produced or consumed edge \\(e\\). - `attribution_trail(region, time_r",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0039",
       "source_file": "thesis.md",
       "source_line": 325,
       "latex": "\\mathcal{S}",
-      "context": "aft-morrow-sogomonian-exec-outcome-attest`.  ---  ### Spine \u2014 `amaru`  **Repo:** `szl-holdings/amaru`  **Formal role in \\(\\mathcal{S}\\):** The Spine is the append-only coordination and protocol bridge",
-      "source_id": "thesis_session"
+      "context": "aft-morrow-sogomonian-exec-outcome-attest`.  ---  ### reasoning spine \u2014 `reasoning core`  **Repo:** `szl-holdings/reasoning core`  **Formal role in \\(\\mathcal{S}\\):** The reasoning spine is the append-only coordination and protocol bridge",
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0040",
       "source_file": "thesis.md",
       "source_line": 325,
       "latex": "\\langle e_1, e_2, \\ldots, e_n \\rangle \\subseteq E",
-      "context": "ordered, hash-verified record of every state transition across the body graph. Formally, `amaru` maintains the sequence \\(\\langle e_1, e_2, \\ldots, e_n \\rangle \\subseteq E\\) ordered by timestamp, with",
-      "source_id": "thesis_session"
+      "context": "ordered, hash-verified record of every state transition across the body graph. Formally, `reasoning core` maintains the sequence \\(\\langle e_1, e_2, \\ldots, e_n \\rangle \\subseteq E\\) ordered by timestamp, with",
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0041",
       "source_file": "thesis.md",
       "source_line": 339,
       "latex": "O(\\log n)",
-      "context": "(identified in the runtime roadmap) would upgrade the Spine's linear hash-chain to a directed acyclic graph supporting \\(O(\\log n)\\) subset inclusion proofs \u2014 enabling privacy-preserving audits for re",
-      "source_id": "thesis_session"
+      "context": "(identified in the runtime roadmap) would upgrade the reasoning spine's linear hash-chain to a directed acyclic graph supporting \\(O(\\log n)\\) subset inclusion proofs \u2014 enabling privacy-preserving audits for re",
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0042",
@@ -457,7 +498,8 @@
       "source_line": 347,
       "latex": "\\mathcal{S}",
       "context": "nce in the enterprise segment.  ---  ### Skeleton \u2014 `lutar-lean`  **Repo:** `szl-holdings/lutar-lean`  **Formal role in \\(\\mathcal{S}\\):** The Skeleton is the formal scaffold \u2014 the Lean 4 axioms and M",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0043",
@@ -465,7 +507,8 @@
       "source_line": 347,
       "latex": "\\{A1, A2, A3, A4\\}",
       "context": "es not execute at runtime; it is the *proof that the runtime is correct*. Formally, `lutar-lean` provides the axiom set \\(\\{A1, A2, A3, A4\\}\\) and the derived theorems (\u039b uniqueness, Bound theorem) th",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "conjectured"
     },
     {
       "id": "F0044",
@@ -473,7 +516,8 @@
       "source_line": 347,
       "latex": "\\Lambda",
       "context": "A2, A3, A4\\}\\) and the derived theorems (\u039b uniqueness, Bound theorem) that constitute a machine-checked certificate for \\(\\Lambda\\). If the Skeleton's `sorry` count is zero, the gate the Brain Stem en",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "conjectured"
     },
     {
       "id": "F0045",
@@ -481,7 +525,8 @@
       "source_line": 351,
       "latex": "\\Lambda",
       "context": "statements of A1 (monotonicity), A2 (homogeneity), A3 (Egyptian-exact), A4 (bounded). - `Uniqueness.lean` \u2014 Theorem 1: \\(\\Lambda\\) is the unique function satisfying A1\u2013A4; proof scaffold with tracked ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "conjectured"
     },
     {
       "id": "F0046",
@@ -489,7 +534,8 @@
       "source_line": 367,
       "latex": "\\mathcal{S}",
       "context": "*Repos:** `szl-holdings/counsel` (governance UI), `szl-holdings/terra` (dashboards and visualization)  **Formal role in \\(\\mathcal{S}\\):** The Hands are the tooling and visualization surfaces \u2014 the co",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0047",
@@ -497,7 +543,8 @@
       "source_line": 371,
       "latex": "\\Lambda",
       "context": "as an interactive SVG, streaming live receipt counts via SSE from `/api/chain/stream`; node colors reflect the current \\(\\Lambda\\) score band (green \u2265 0.95, amber 0.90\u20130.95, red < 0.90). The planned \"",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0048",
@@ -505,7 +552,8 @@
       "source_line": 386,
       "latex": "\\mathcal{S}",
       "context": "*is* the system.  ---  ### Full Body \u2014 `ouroboros-thesis`  **Repo:** `szl-holdings/ouroboros-thesis`  **Formal role in \\(\\mathcal{S}\\):** The Full Body is the public-record thesis \u2014 the DOI-pinned, ve",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0049",
@@ -513,7 +561,8 @@
       "source_line": 386,
       "latex": "\\mathcal{S}",
       "context": "l Body is the public-record thesis \u2014 the DOI-pinned, versioned document that constitutes the canonical specification of \\(\\mathcal{S}\\). Formally, `ouroboros-thesis` defines the normative description ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0050",
@@ -521,7 +570,8 @@
       "source_line": 405,
       "latex": "\\mathcal{S}",
       "context": "d identity anchoring), `szl-holdings/szl-cookbook` (reference implementations / developer onboarding)  **Formal role in \\(\\mathcal{S}\\):** The Vessels and Chakras collectively form the trust mesh and ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0051",
@@ -529,7 +579,8 @@
       "source_line": 421,
       "latex": "\\varepsilon",
       "context": "eue under the covenant pack schema.  ---  ## Cross-Region Contracts  Every edge in \\(E\\) carries a **receipt envelope** \\(\\varepsilon\\). The envelope is a typed, signed, content-addressed record that ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0052",
@@ -537,7 +588,8 @@
       "source_line": 421,
       "latex": "\\Lambda",
       "context": "es a **receipt envelope** \\(\\varepsilon\\). The envelope is a typed, signed, content-addressed record that provides: the \\(\\Lambda\\) score vector, the dual-witness closure status (\\(\\rho\\)), the actor ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0053",
@@ -545,7 +597,8 @@
       "source_line": 479,
       "latex": "\\Lambda",
       "context": "_lambda(axes) \u2192 Receipt` \u2014 any MCP-compatible client (Claude Desktop, Cursor, enterprise agent frameworks) can call the \\(\\Lambda\\) gate as a typed tool and receive a signed receipt in the tool respon",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0054",
@@ -553,7 +606,8 @@
       "source_line": 507,
       "latex": "\\mathcal{S}",
       "context": "the 8-Region Model Structurally Surpasses the Leaders  Each leading framework or protocol is a partial instantiation of \\(\\mathcal{S}\\). The gap is structural: the missing region is not a feature that",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0055",
@@ -561,7 +615,8 @@
       "source_line": 515,
       "latex": "\\Lambda_9",
       "context": "l engineering pattern, but skills are *files*, not services with receipts. A Brain Stem can issue a decision that fails \\(\\Lambda_9\\) moralGrounding; in the Managed Agents architecture there is no mec",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0056",
@@ -569,7 +624,8 @@
       "source_line": 515,
       "latex": "\\mathcal{S}",
       "context": "fails \\(\\Lambda_9\\) moralGrounding; in the Managed Agents architecture there is no mechanism to detect or block it. In \\(\\mathcal{S}\\), that decision never exits the Brain Stem.  **Mastra** (22K+ GitH",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0057",
@@ -577,7 +633,8 @@
       "source_line": 517,
       "latex": "\\Lambda",
       "context": "ource agent framework in the TypeScript ecosystem. Mastra has no Skeleton: there are no Lean 4 proofs. It has no formal \\(\\Lambda\\) gate \u2014 behavioral constraints are implemented as runtime checks with",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0058",
@@ -585,7 +642,8 @@
       "source_line": 567,
       "latex": "\\lambda_1",
       "context": "l(\\lambda_1(c),\\, \\lambda_2(c),\\, \\ldots,\\, \\lambda_9(c)\\bigr) \\in [0,1]^9 \\]  The nine axes are defined as follows.  **\\(\\lambda_1\\): moralGrounding.** Measures the degree to which a proposed action ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0059",
@@ -593,7 +651,8 @@
       "source_line": 567,
       "latex": "\\lambda_1",
       "context": "nce policies, and principal hierarchies that the operator has encoded in the agent's governing covenant. Operationally, \\(\\lambda_1\\) is the normalized cosine similarity between the action's intent em",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0060",
@@ -601,7 +660,8 @@
       "source_line": 567,
       "latex": "[0,1]",
       "context": "mbedding and a reference \"moral anchor\" embedding, averaged over the operator's registered covenant clauses, clamped to \\([0,1]\\). The floor constraint \\(\\lambda_1 \\geq 0.95\\) is a hard asymptote: an ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0061",
@@ -609,7 +669,8 @@
       "source_line": 567,
       "latex": "\\lambda_1 \\geq 0.95",
       "context": "anchor\" embedding, averaged over the operator's registered covenant clauses, clamped to \\([0,1]\\). The floor constraint \\(\\lambda_1 \\geq 0.95\\) is a hard asymptote: an agent that is even marginally mo",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0062",
@@ -617,7 +678,8 @@
       "source_line": 569,
       "latex": "\\lambda_2",
       "context": "even marginally morally misaligned fails the gate irrespective of how perfectly calibrated the other eight axes are.  **\\(\\lambda_2\\): measurabilityHonesty.** Measures whether an action's declared eff",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0063",
@@ -625,7 +687,8 @@
       "source_line": 571,
       "latex": "\\lambda_3",
       "context": "ine clause \"no hallucinations no bandaids; test test test\" by making measurement-honesty a prerequisite for passage.  **\\(\\lambda_3\\): epistemicHumility.** Scores the agent's acknowledgment of its own",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0064",
@@ -633,7 +696,8 @@
       "source_line": 571,
       "latex": "\\lambda_3 = 1 - \\mathbb{E}[|\\text{conf}(c) - \\text{acc}(c)|]",
       "context": "sparse scores low on this axis. The scoring function penalizes unjustified confidence using a calibration-error analog: \\(\\lambda_3 = 1 - \\mathbb{E}[|\\text{conf}(c) - \\text{acc}(c)|]\\) where \\(\\text{c",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0065",
@@ -641,7 +705,8 @@
       "source_line": 571,
       "latex": "\\text{conf}(c)",
       "context": "ied confidence using a calibration-error analog: \\(\\lambda_3 = 1 - \\mathbb{E}[|\\text{conf}(c) - \\text{acc}(c)|]\\) where \\(\\text{conf}(c)\\) is the agent's stated confidence and \\(\\text{acc}(c)\\) is the",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0066",
@@ -649,7 +714,8 @@
       "source_line": 571,
       "latex": "\\text{acc}(c)",
       "context": "da_3 = 1 - \\mathbb{E}[|\\text{conf}(c) - \\text{acc}(c)|]\\) where \\(\\text{conf}(c)\\) is the agent's stated confidence and \\(\\text{acc}(c)\\) is the empirically measured accuracy over a calibration set.  ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0067",
@@ -657,7 +723,8 @@
       "source_line": 573,
       "latex": "\\lambda_4",
       "context": "is the agent's stated confidence and \\(\\text{acc}(c)\\) is the empirically measured accuracy over a calibration set.  **\\(\\lambda_4\\): counterfactualAwareness.** Measures whether the agent has consider",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0068",
@@ -665,7 +732,8 @@
       "source_line": 575,
       "latex": "\\lambda_5",
       "context": "res 0.0 and a uniformly distributed consequence distribution over the operator-defined consequence space scores 1.0.  **\\(\\lambda_5\\): temporalConsistency.** Measures the stability of the gate verdict",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0069",
@@ -673,7 +741,8 @@
       "source_line": 575,
       "latex": "t + \\Delta",
       "context": "Measures the stability of the gate verdict under repeated evaluation on the same input at two different times \\(t\\) and \\(t + \\Delta\\). Let \\(v_t\\) and \\(v_{t+\\Delta}\\) denote the \u039b\u2089 composite scores ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0070",
@@ -681,7 +750,8 @@
       "source_line": 575,
       "latex": "v_{t+\\Delta}",
       "context": "te verdict under repeated evaluation on the same input at two different times \\(t\\) and \\(t + \\Delta\\). Let \\(v_t\\) and \\(v_{t+\\Delta}\\) denote the \u039b\u2089 composite scores at the two evaluation times. The",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0071",
@@ -689,7 +759,8 @@
       "source_line": 581,
       "latex": "\\lambda_5 = 1.0",
       "context": "Then:  \\[ \\lambda_5 = \\max\\!\\Bigl(0,\\; 1 - 4\\,\\bigl(v_t - v_{t+\\Delta}\\bigr)^2\\Bigr) \\]  A zero-drift evaluation scores \\(\\lambda_5 = 1.0\\). A drift of 0.05 in the composite score yields \\(\\lambda_5 =",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0072",
@@ -697,7 +768,8 @@
       "source_line": 581,
       "latex": "\\lambda_5 = 0.99",
       "context": "ta}\\bigr)^2\\Bigr) \\]  A zero-drift evaluation scores \\(\\lambda_5 = 1.0\\). A drift of 0.05 in the composite score yields \\(\\lambda_5 = 0.99\\). A drift of 0.25 yields \\(\\lambda_5 = 0.75\\), below the \u2265 0",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0073",
@@ -705,7 +777,8 @@
       "source_line": 581,
       "latex": "\\lambda_5 = 0.75",
       "context": "scores \\(\\lambda_5 = 1.0\\). A drift of 0.05 in the composite score yields \\(\\lambda_5 = 0.99\\). A drift of 0.25 yields \\(\\lambda_5 = 0.75\\), below the \u2265 0.90 conjunctive floor. This axis operationaliz",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0074",
@@ -713,7 +786,10 @@
       "source_line": 583,
       "latex": "\\lambda_6",
       "context": "-identical replay guarantee: a system that cannot reproduce its own gate verdict is not operating deterministically.  **\\(\\lambda_6\\): evidenceProvenance.** Measures whether every empirical claim embe",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined",
+      "puriq_ref": "F1",
+      "lean_ref": "f1_replay_fold_deterministic"
     },
     {
       "id": "F0075",
@@ -721,7 +797,8 @@
       "source_line": 585,
       "latex": "\\lambda_7",
       "context": "ertions score at most 0.50. The scoring function is the fraction of claim tokens for which provenance is resolvable.  **\\(\\lambda_7\\): actorIdentity.** Measures the definiteness of the acting agent's ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0076",
@@ -729,7 +806,8 @@
       "source_line": 587,
       "latex": "\\lambda_8",
       "context": "ting under delegated authority \u2014 the score decays as a function of delegation depth to penalize opaque proxy chains.  **\\(\\lambda_8\\): axiomConsistency.** Measures whether the proposed action is inter",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0077",
@@ -737,7 +815,8 @@
       "source_line": 589,
       "latex": "\\lambda_9",
       "context": "Lean 4 formalization: it enforces, at runtime, the constraints that are statically verified at theorem-proving time.  **\\(\\lambda_9\\): coherence.** Measures the multi-step logical coherence of the age",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0078",
@@ -745,7 +824,8 @@
       "source_line": 589,
       "latex": "A_1, A_2, \\ldots, A_k",
       "context": "-step logical coherence of the agent's plan across the action sequence, not just for the current step in isolation. Let \\(A_1, A_2, \\ldots, A_k\\) denote the \\(k\\) preceding actions in the current sess",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0079",
@@ -753,7 +833,8 @@
       "source_line": 589,
       "latex": "(A_i, A_{i+1})",
       "context": "e the \\(k\\) preceding actions in the current session. The coherence score is the proportion of consecutive action-pairs \\((A_i, A_{i+1})\\) for which the precondition of \\(A_{i+1}\\) is satisfied by the",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0080",
@@ -761,7 +842,8 @@
       "source_line": 589,
       "latex": "A_{i+1}",
       "context": "ion. The coherence score is the proportion of consecutive action-pairs \\((A_i, A_{i+1})\\) for which the precondition of \\(A_{i+1}\\) is satisfied by the postcondition of \\(A_i\\), under the operator's p",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0081",
@@ -769,7 +851,8 @@
       "source_line": 589,
       "latex": "\\lambda_9 = 1.0",
       "context": "ied by the postcondition of \\(A_i\\), under the operator's precondition/postcondition schema. For the base case \\(k=0\\), \\(\\lambda_9 = 1.0\\).  ### The conjunctive gate condition  The \u039b\u2089 gate passes if ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0082",
@@ -777,7 +860,8 @@
       "source_line": 599,
       "latex": "\\lambda_1 = 0.50",
       "context": "for the following reason. A single composite score \u2014 even a geometric mean \u2014 can mask localized failures. An agent with \\(\\lambda_1 = 0.50\\) (severely morally misaligned) and all remaining axes at \\(1",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0083",
@@ -785,7 +869,8 @@
       "source_line": 599,
       "latex": "\\prod_{i}^{1/9} = 0.50^{1/9} \\approx 0.926",
       "context": "with \\(\\lambda_1 = 0.50\\) (severely morally misaligned) and all remaining axes at \\(1.0\\) achieves a geometric mean of \\(\\prod_{i}^{1/9} = 0.50^{1/9} \\approx 0.926\\), which would pass a \u2265 0.90 single-",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0084",
@@ -793,7 +878,8 @@
       "source_line": 599,
       "latex": "\\lambda_1",
       "context": "gle-score gate. The conjunctive AND structure prevents this: every axis is a blocking veto. The two elevated floors for \\(\\lambda_1\\) and \\(\\lambda_2\\) add a second layer of asymmetry \u2014 these are the ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0085",
@@ -801,7 +887,8 @@
       "source_line": 599,
       "latex": "\\lambda_2",
       "context": "e conjunctive AND structure prevents this: every axis is a blocking veto. The two elevated floors for \\(\\lambda_1\\) and \\(\\lambda_2\\) add a second layer of asymmetry \u2014 these are the axes most directly",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0086",
@@ -809,7 +896,8 @@
       "source_line": 605,
       "latex": "m \\in \\{0,1\\}^9",
       "context": "to the receipt structure. Rather than publishing the raw nine (or ten) axis scores, the receipt carries a bitfield mask \\(m \\in \\{0,1\\}^9\\) in which \\(m_i = 1\\) if and only if \\(\\lambda_i\\) was evalua",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0087",
@@ -817,7 +905,8 @@
       "source_line": 605,
       "latex": "m_i = 1",
       "context": "her than publishing the raw nine (or ten) axis scores, the receipt carries a bitfield mask \\(m \\in \\{0,1\\}^9\\) in which \\(m_i = 1\\) if and only if \\(\\lambda_i\\) was evaluated and passed its floor. The",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0088",
@@ -825,7 +914,8 @@
       "source_line": 605,
       "latex": "\\lambda_i",
       "context": "nine (or ten) axis scores, the receipt carries a bitfield mask \\(m \\in \\{0,1\\}^9\\) in which \\(m_i = 1\\) if and only if \\(\\lambda_i\\) was evaluated and passed its floor. The raw scores are withheld fro",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0089",
@@ -833,7 +923,8 @@
       "source_line": 611,
       "latex": "\\theta_i = 0.95",
       "context": "ity profile of the agent. Formally, the mask is computed as:  \\[ m_i = \\mathbf{1}[\\lambda_i(c) \\geq \\theta_i] \\]  where \\(\\theta_i = 0.95\\) for \\(i \\in \\{1,2\\}\\) and \\(\\theta_i = 0.90\\) otherwise. The",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0090",
@@ -841,7 +932,8 @@
       "source_line": 611,
       "latex": "i \\in \\{1,2\\}",
       "context": ". Formally, the mask is computed as:  \\[ m_i = \\mathbf{1}[\\lambda_i(c) \\geq \\theta_i] \\]  where \\(\\theta_i = 0.95\\) for \\(i \\in \\{1,2\\}\\) and \\(\\theta_i = 0.90\\) otherwise. The gate passes iff \\(\\sum_",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0091",
@@ -849,7 +941,8 @@
       "source_line": 611,
       "latex": "\\theta_i = 0.90",
       "context": "s computed as:  \\[ m_i = \\mathbf{1}[\\lambda_i(c) \\geq \\theta_i] \\]  where \\(\\theta_i = 0.95\\) for \\(i \\in \\{1,2\\}\\) and \\(\\theta_i = 0.90\\) otherwise. The gate passes iff \\(\\sum_i m_i = 9\\) (or 10 und",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0092",
@@ -857,7 +950,8 @@
       "source_line": 611,
       "latex": "\\sum_i m_i = 9",
       "context": "eq \\theta_i] \\]  where \\(\\theta_i = 0.95\\) for \\(i \\in \\{1,2\\}\\) and \\(\\theta_i = 0.90\\) otherwise. The gate passes iff \\(\\sum_i m_i = 9\\) (or 10 under \u039b\u2081\u2080). The mask is committed via SHA-256 and incl",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0093",
@@ -865,7 +959,8 @@
       "source_line": 627,
       "latex": "\\textit{parent\\_hash}",
       "context": "\\textit{timestamp},\\; \\vec{\\lambda},\\; \\rho\\_\\textit{witness\\_set},\\; \\textit{signature}\\bigr) \\]  The fields are:  - **\\(\\textit{parent\\_hash}\\)**: The SHA-256 digest of receipt \\(r_{i-1}\\). For the ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0094",
@@ -873,7 +968,8 @@
       "source_line": 627,
       "latex": "r_{i-1}",
       "context": "s\\_set},\\; \\textit{signature}\\bigr) \\]  The fields are:  - **\\(\\textit{parent\\_hash}\\)**: The SHA-256 digest of receipt \\(r_{i-1}\\). For the genesis receipt, this is the SHA-256 of a protocol-specifie",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0095",
@@ -881,7 +977,8 @@
       "source_line": 628,
       "latex": "\\textit{content\\_digest}",
       "context": "this is the SHA-256 of a protocol-specified null seed. This field creates the backward-pointing link of the chain. - **\\(\\textit{content\\_digest}\\)**: The SHA-256 of the canonical JSON serialization o",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0096",
@@ -889,7 +986,8 @@
       "source_line": 629,
       "latex": "\\textit{actor}",
       "context": "fore any side-effectful execution. This binds the gate verdict irrevocably to the specific input that triggered it. - **\\(\\textit{actor}\\)**: The identifier of the acting agent as registered in the pr",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0097",
@@ -897,7 +995,8 @@
       "source_line": 629,
       "latex": "\\lambda_7",
       "context": "t. - **\\(\\textit{actor}\\)**: The identifier of the acting agent as registered in the principal registry. Corresponds to \\(\\lambda_7\\) (actorIdentity). - **\\(\\textit{timestamp}\\)**: A monotonic timesta",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0098",
@@ -905,7 +1004,8 @@
       "source_line": 630,
       "latex": "\\textit{timestamp}",
       "context": "entifier of the acting agent as registered in the principal registry. Corresponds to \\(\\lambda_7\\) (actorIdentity). - **\\(\\textit{timestamp}\\)**: A monotonic timestamp in milliseconds since the Unix e",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0099",
@@ -913,7 +1013,8 @@
       "source_line": 631,
       "latex": "\\vec{\\lambda}",
       "context": ": A monotonic timestamp in milliseconds since the Unix epoch, drawn from a pinned, non-forgeable source (see \u00a74.6). - **\\(\\vec{\\lambda}\\)**: The full nine-dimensional \u039b vector, or the `lambda9_mask` b",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     },
     {
       "id": "F0100",
@@ -921,7 +1022,8 @@
       "source_line": 632,
       "latex": "\\rho\\_\\textit{witness\\_set}",
       "context": "vec{\\lambda}\\)**: The full nine-dimensional \u039b vector, or the `lambda9_mask` bitfield under the \u039b\u2081\u2080 privacy variant. - **\\(\\rho\\_\\textit{witness\\_set}\\)**: The set of co-witnesses whose signatures are ",
-      "source_id": "thesis_session"
+      "source_id": "thesis_session",
+      "maturity": "defined"
     }
   ],
   "definitions": [],
@@ -1583,5 +1685,1067 @@
     "10.5281/zenodo.20053163",
     "10.5281/zenodo.20119582",
     "10.5281/zenodo.20162352"
-  ]
+  ],
+  "proof_summary": {
+    "locked_proven": 5,
+    "locked_ids": [
+      "F1",
+      "F11",
+      "F12",
+      "F18",
+      "F19"
+    ],
+    "experimental_sorry_free": 21,
+    "axiom_gated": 3,
+    "axiom_gated_detail": {
+      "f13_tamper_evident": "hash_collision_resistant",
+      "f14_dsse_verifiable": "ecdsa_unforgeable",
+      "f15_inclusion_binding": "h2_collision_resistant"
+    },
+    "conjecture": [
+      "F23"
+    ],
+    "note": "Locked kernel proven=5; experimental scope Lutar/Puriq/Formulas has 21 sorry-free (excluded from locked count); F23 = Conjecture 1, NOT a theorem.",
+    "lean_repo": "szl-holdings/lutar-lean",
+    "lean_files": [
+      "Lutar/Puriq/Formulas/PuriqFormulaLean.lean",
+      "Lutar/Puriq/Formulas/F23_Uniqueness.lean"
+    ],
+    "verification": "bare `lean` 4.13.0, 0 errors, 1 sorry (F23 only); #print axioms shows no sorryAx in any proved theorem.",
+    "source_report": "team/PROOFS_WAVE2_REPORT.md",
+    "wave3": {
+      "campaign": "prove-wave-3 (C1-C20 research candidates)",
+      "source_report": "team/PROVE_WAVE3_REPORT.md",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "commit_proofs": "775093f0f8ef7f530272c38d513c28fdaec3366b",
+      "commit_root_wiring": "02e44c30657c9986475ff7373113728f4ba38f67",
+      "lean_files": [
+        "Lutar/Wave3/Consensus.lean",
+        "Lutar/Wave3/MerkleKraft.lean",
+        "Lutar/Wave3/InfoEstim.lean",
+        "Lutar/Wave3/Tier1Mathlib.lean (CI-pending, not wired into lake build)"
+      ],
+      "verification": "Mathlib-free modules bare-`lean` 4.13.0 verified sorry-free (0 errors); #print axioms ledger shows no sorryAx. Tier1Mathlib (C1/C2/C6) is Mathlib-dependent and CI-pending, NOT compiled in sandbox.",
+      "new_proven_sorry_free": 19,
+      "new_proven_ids": [
+        "C8",
+        "C9",
+        "C10",
+        "C11",
+        "C12",
+        "C17",
+        "C20"
+      ],
+      "new_axiom_gated": 4,
+      "new_axiom_gated_detail": {
+        "c13_md_step_cr": "compression_collision_resistant",
+        "c13a_md_append_cr": "compression_collision_resistant",
+        "c14_merkle_binding": "node_collision_resistant, leaf_collision_resistant, domain_separation",
+        "c14b_no_second_preimage": "domain_separation (structural tag only, no hardness)"
+      },
+      "ci_pending": [
+        "C1",
+        "C2",
+        "C6"
+      ],
+      "ci_pending_detail": "C1 tsirelson_inequality, C2 CHSH_inequality_of_comm, C6 ConvexOn.map_sum_le re-exports; Mathlib-dependent, awaiting green lake build.",
+      "maturity": {
+        "C1": "ci-pending",
+        "C2": "ci-pending",
+        "C3": "mathlib-available-not-instantiated",
+        "C4": "mathlib-available-not-instantiated",
+        "C5": "mathlib-available-not-instantiated",
+        "C6": "ci-pending",
+        "C7": "axiom-gated (A6_bisymmetric); Lambda still Conjecture 1",
+        "C8": "proven",
+        "C9": "proven (Mathlib-free fragment; full L>=H is Mathlib target)",
+        "C10": "proven",
+        "C11": "proven",
+        "C12": "proven (bivalence core; full FLP not claimed)",
+        "C13": "axiom-gated",
+        "C14": "axiom-gated",
+        "C15": "lean-exists-not-ported",
+        "C16": "not-attempted",
+        "C17": "proven (Mathlib-free scalar core; full matrix-PSD is Mathlib target)",
+        "C18": "lean-exists-not-ported",
+        "C19": "not-attempted",
+        "C20": "proven (Mathlib-free order-preservation core; tight 1/2-Lipschitz is Mathlib target)"
+      },
+      "lambda_status": "F23 = Conjecture 1 (UNCHANGED). C7 is conditional only, via the DECLARED axiom A6_bisymmetric in F23_Uniqueness.lean; unconditional uniqueness is FALSE under A1-A5 (maxAgg_ne_Lambda).",
+      "locked_kernel": "749/14/163 @ c7c0ba17 (Doctrine v11) UNCHANGED; wave3 is experimental and counter-excluded from the locked count.",
+      "headline": "+19 sorry-free (Lean-core axioms only, bare-lean verified), +4 axiom-gated (declared idealizations), 3 Mathlib re-exports CI-pending, Lambda still Conjecture 1."
+    },
+    "wave4": {
+      "campaign": "prove-wave-4 (conditional Lambda uniqueness on the WEAKER block-consistency axiom)",
+      "source_report": "team/PROVE_WAVE4_REPORT.md",
+      "candidate_research": "team/RESEARCH_WAVE4/CANDIDATE_FORMULAS_V4.md",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "commit_final": "043c3df4bcbe55c60f1ce2d5c59b91284a7cc1d4",
+      "commit_ci_green_lambda": "52d9bf542bcb1adb8a0a5a5de694f2ca96bf9b68",
+      "lean_files": [
+        "Lutar/Wave4/LambdaBlockConsistency.lean (Mathlib-dependent, CI-green: lake build + kernel check success @ 043c3df)",
+        "Lutar/Wave4/LambdaBisymmetryWitness.lean (bare-`lean` 4.13.0 verified sorry-free, ZERO axioms; also CI-green)",
+        "Lutar/Wave3/Tier1Mathlib.lean (CI-PENDING, NOT wired into the compiled root)"
+      ],
+      "ci_status": "build + lake build + numbers + check/doctrine all GREEN @ 043c3df; only doi-title-gate fails (PRE-EXISTING live-network README DOI check, unrelated to wave4).",
+      "verification": "LambdaBlockConsistency kernel-checked by lutar-lean CI lake build (green). LambdaBisymmetryWitness bare-`lean` verified: all 6 theorems 'do not depend on any axioms'. Every theorem carries #print axioms.",
+      "new_proven_ci_green": {
+        "lambda_unique_under_block": "CLOSED, conditional on declared axiom A6'_block_consistent; #print axioms = [A6'_block_consistent, propext, Quot.sound, Classical.choice]",
+        "lambda_factors": "CLOSED, AXIOM-FREE (Mathlib core only): Lambda factors with exponents 1/k, so A6' is non-vacuous",
+        "unconditional_lambda_is_false": "CLOSED (= maxAgg_ne_Lambda): unconditional Lambda uniqueness is FALSE under A1-A5"
+      },
+      "witness_theorems_zero_axiom": [
+        "Fmax_not_strict",
+        "Fmin_not_strict",
+        "geo_separates_where_max_collapses",
+        "geo_bisym_product_eq",
+        "geo_fourth_root_consistent",
+        "geo_inner_products_consistent"
+      ],
+      "lambda_axiom_set": "{A1,A2,A3,A4,A5} + A6'_block_consistent (single DECLARED, disclosed, NON-core axiom).",
+      "lambda_weakest_axiom": "Cleanest published: Aczel-Saaty 1983 (doi:10.1016/0022-2496(83)90028-7) = reciprocity + positive homogeneity (A2 already assumed). Weakest governance-natural & formalized: Csato 2018 block-consistency / aggregation-invariance (doi:10.1007/s10726-018-9589-3, arXiv:1706.07256), WEAKER than the prior A6_bisymmetric.",
+      "lambda_status": "F23 = Conjecture 1 (UNCHANGED, unconditional). Conditional uniqueness now CI-green on the WEAKER A6'_block_consistent (lambda_unique_under_block), superseding the stronger A6_bisymmetric route. Unconditional uniqueness FALSE (maxAgg_ne_Lambda). NEVER conflated.",
+      "ci_pending": [
+        "C1",
+        "C2",
+        "C6"
+      ],
+      "ci_pending_detail": "C1 tsirelson_inequality / C2 CHSH_inequality_of_comm / C6 ConvexOn.map_sum_le re-exports. Signatures verified VERBATIM vs pinned Mathlib d731765, but wiring Tier1Mathlib into the compiled root reproducibly red-lights lake build (bisected: a4299fb/52d9bf5 un-wired = green). Exact error not retrievable (CI log download proxy-blocked). File stays in-tree, NOT imported; NOT claimed proven.",
+      "locked_kernel": "749/14/163 @ c7c0ba17 UNCHANGED",
+      "locked_proven": 5,
+      "canonical_numbers": {
+        "declarations": 1182,
+        "axioms_raw": 20,
+        "axioms_unique": 19,
+        "new_axiom": "A6'_block_consistent (declared, disclosed, NON-core, NOT in locked kernel)",
+        "sorries_raw": 308,
+        "sorries_noncomment": 256,
+        "drift_gate": "PASS"
+      },
+      "citations": [
+        "Aczel 1948",
+        "Aczel-Saaty 1983 doi:10.1016/0022-2496(83)90028-7",
+        "Csato 2018 doi:10.1007/s10726-018-9589-3 arXiv:1706.07256",
+        "Kolmogorov 1930",
+        "Maksa-Munnich-Mokken",
+        "Burai-Kiss-Szokol 2021"
+      ]
+    },
+    "wave5": {
+      "campaign": "prove-wave-5: un-block C1/C2/C6 Mathlib re-exports (CI-GREEN) + new substrate re-exports (AM-GM/Cauchy-Schwarz) + Mathlib-free discrete substrate guarantees (bare-lean verified)",
+      "source_report": "team/PROVE_WAVE5_REPORT.md",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "branch": "prove-wave5/c1c2c6-rewire-plus-amgm-cs",
+      "pull_request": "https://github.com/szl-holdings/lutar-lean/pull/186",
+      "commit_ci_green": "0a552a90dd7f3b8b668ae761bf6e39eca17c62f1",
+      "ci_run_ids": {
+        "lean_kernel_check": "27053443102 (success)",
+        "lake_build_gate_numbers": "27053443099 (success)",
+        "doctrine": "27053443200 (success)",
+        "dco": "27053443096 (success)"
+      },
+      "ci_status": "build (Lean kernel check) + lake build + numbers + check/doctrine + DCO all GREEN @ 0a552a90 (and @ 099d6caa). Only doi-title-gate + PR-title-lint fail (PRE-EXISTING / cosmetic, unrelated to proofs).",
+      "headline": "C1 Tsirelson 2sqrt2 / C2 CHSH<=2 / C6 Jensen are now CI-GREEN (wave-4 had them CI-PENDING). Root cause fixed: dropped the non-load-bearing c1a_tsirelson_constant numeric remark and its two extra SpecialFunctions imports, minimizing Tier1Mathlib's build closure to exactly the two modules that define the instantiated theorems.",
+      "ci_green_mathlib_dependent": {
+        "Wave3.Tier1.c1_lutar_omega_tsirelson_ceiling": "C1 Tsirelson 2sqrt2 ceiling (tsirelson_inequality) \u2014 PROVEN, CI-green. EPR-Bell governance diagnostic (entangled-agent ceiling).",
+        "Wave3.Tier1.c2_lutar_omega_classical_ceiling": "C2 CHSH classical ceiling <=2 (CHSH_inequality_of_comm) \u2014 PROVEN, CI-green. Local/independent-prior agent ceiling.",
+        "Wave3.Tier1.c6_jensen_forecaster": "C6 finite Jensen (ConvexOn.map_sum_le) \u2014 PROVEN, CI-green. Active-inference ELBO-direction conservative forecaster.",
+        "Wave5.MathlibCore.w5_1_lambda_le_arith_mean": "W5-1 weighted AM-GM (Real.geom_mean_le_arith_mean_weighted) \u2014 PROVEN, CI-green. Lambda (geometric-mean aggregator) <= arithmetic mean: no-inflation guarantee.",
+        "Wave5.MathlibCore.w5_1b_lambda2_le_arith_mean": "W5-1b two-point weighted AM-GM \u2014 PROVEN, CI-green. Pairwise consensus diagnostic.",
+        "Wave5.MathlibCore.w5_2_trust_inner_le_norm": "W5-2 Cauchy-Schwarz (real_inner_le_norm) \u2014 PROVEN, CI-green. Trust-vector similarity bound (cosine in [-1,1])."
+      },
+      "proven_mathlib_free_bare_lean": {
+        "Wave5.DiscreteSubstrate.w5_3a_miscover_le_total": "miscoverage<=sample size. axioms=[propext]. killinchu conformal coverage.",
+        "Wave5.DiscreteSubstrate.w5_3b_cover_miscover_partition": "covered+miscovered=total. axioms=[propext, Quot.sound]. coverage=1-miscoverage conservation.",
+        "Wave5.DiscreteSubstrate.w5_3c_threshold_count_mono": "stricter threshold selects fewer. axioms=[propext, Quot.sound]. a11oy threshold monotonicity.",
+        "Wave5.DiscreteSubstrate.w5_4_collision_of_image_dup": "image-duplicate => hash collision (pigeonhole). axioms=[propext, Classical.choice, Quot.sound]. UDS forgery-detection.",
+        "Wave5.DiscreteSubstrate.w5_5_no_early_stop_deflation": "monotone optional-stopping anti-deflation. ZERO axioms. UDS receipt-stream anti-gaming."
+      },
+      "axiom_disclosure": "Mathlib-dependent re-exports use the standard Mathlib trio [propext, Classical.choice, Quot.sound] (NO sorryAx, NO declared Lutar axioms); their #print axioms are emitted in the CI build log (blob log download proxy-blocked here, but the build is green and they are pure term-mode instantiations of axiom-clean Mathlib theorems). Mathlib-free theorems' #print axioms pasted verbatim in PROVE_WAVE5_REPORT.md section 3 (bare lean 4.13.0, exit 0).",
+      "not_available_at_pinned_mathlib": "C3 Hoeffding / C4 Azuma (Mathlib.Probability.Moments.SubGaussian) and C5 KL>=0 (Mathlib.InformationTheory.KullbackLeibler.Basic) modules DO NOT EXIST at the pinned rev d7317655 (v4.13.0) \u2014 verified HTTP 404. They cannot be re-exported on this toolchain; deferred to a future Mathlib bump. Honestly NOT claimed.",
+      "lambda_status": "Lambda (F23) STAYS Conjecture 1 unconditionally. W5-1 AM-GM is a building block Lambda relies on; it does NOT prove uniqueness. Unconditional uniqueness remains FALSE (wave-4 counterexample in-tree).",
+      "locked_kernel": "749/14/163 @ c7c0ba17 UNCHANGED. locked_proven=5 UNCHANGED. All wave-5 work is experimental scope (counter-excluded).",
+      "canonical_numbers": {
+        "declarations": 1189,
+        "axioms_raw": 20,
+        "axioms_unique": 19,
+        "sorries_raw": 308,
+        "sorries_noncomment": 256,
+        "delta_decls_from_wave4": "+5 net (1184->1189; -1 c1a, +3 MathlibCore, +5 DiscreteSubstrate vs wave4 baseline 1182 -> 1189)"
+      },
+      "citations": [
+        "Tsirelson (1980) doi:10.1007/BF00417500",
+        "CHSH (1969) doi:10.1103/PhysRevLett.23.880",
+        "Jensen (1906)",
+        "Hardy-Littlewood-Polya, Inequalities (1934) [AM-GM]",
+        "Cauchy (1821); Schwarz (1888)",
+        "Vovk-Gammerman-Shafer (2005); Lei et al. (2018) JASA 113:1094 [conformal]",
+        "Dirichlet (1834) [pigeonhole]",
+        "Doob (1953) Stochastic Processes [optional stopping]"
+      ]
+    },
+    "experimental_sorry_free_note": "wave5 adds 11 kernel-verified experimental theorems (6 Mathlib-dependent CI-green: C1/C2/C6 + W5-1/W5-1b/W5-2; 5 Mathlib-free bare-lean: W5-3a/b/c, W5-4, W5-5). Prior experimental_sorry_free baseline was 21 (wave-2 F-pack ceiling).",
+    "wave5_proven_count": {
+      "mathlib_dependent_ci_green": 6,
+      "mathlib_free_bare_lean": 5,
+      "total_new": 11
+    },
+    "wave6": {
+      "campaign": "prove-wave-6 (graph substrate)",
+      "pull_request": "https://github.com/szl-holdings/lutar-lean/pull/189",
+      "commit_ci_green": "dc7ae26d",
+      "ci_status": "GREEN (Lean kernel check + lake build+numbers + doctrine + DCO)",
+      "count": 11,
+      "axioms": "0 new",
+      "new_proven_ids": [
+        "F-G1",
+        "F-G2",
+        "F-G3",
+        "F-G4",
+        "F-G5",
+        "F-G6"
+      ],
+      "headline": "Frechet/Kuratowski embedding core, GNN<=1-WL ceiling, spectral contraction, Lambda-graph iso-invariance, bounded-frontier DAG termination, relabel-invariance",
+      "maturity": "experimental-CI-green",
+      "locked_kernel": "749/14/163 @ c7c0ba17 UNCHANGED; experimental scope"
+    },
+    "wave7": {
+      "campaign": "prove-wave-7",
+      "pull_request": "https://github.com/szl-holdings/lutar-lean/pull/190",
+      "commit_ci_green": "d6a232ba",
+      "ci_status": "GREEN",
+      "count": 10,
+      "axioms": "0 new",
+      "new_proven_ci_green": [
+        "W7-1a",
+        "W7-1",
+        "W7-5a",
+        "W7-5b",
+        "W7-5"
+      ],
+      "new_proven_bare_lean": [
+        "W7-4a",
+        "W7-4b",
+        "W7-4c",
+        "W7-6a",
+        "W7-6"
+      ],
+      "headline": "conformal rank-count/p-value + Doob two-sided audit envelope + degree-sum iso-invariance + PAC-Bayes routing envelope",
+      "maturity": "experimental-CI-green",
+      "locked_kernel": "749/14/163 @ c7c0ba17 UNCHANGED; experimental scope"
+    },
+    "agentic_loop": {
+      "campaign": "prove-agentic-loop (the governed RAG->MCP->kernel->receipt loop, proven as a SYSTEM)",
+      "pull_request": "https://github.com/szl-holdings/lutar-lean/pull/188",
+      "commit_ci_green": "2ede47a2",
+      "ci_status": "GREEN",
+      "namespace": "Lutar.Agentic.Pipeline (EXPERIMENTAL_SCOPES; NOT imported into Lutar.lean)",
+      "theorems": 28,
+      "axiom_free": 14,
+      "lean_core_only": 10,
+      "axiom_gated": 4,
+      "declared_axiom": "hashFn_collision_resistant (P5 only; NIST FIPS 180-4)",
+      "properties": {
+        "P1": "receipt-completeness",
+        "P2": "gate-soundness",
+        "P3": "non-interference (Goguen-Meseguer 1982, axiom-free core)",
+        "P4": "replay-determinism (axiom-free)",
+        "P5": "tamper-evidence (axiom-gated)",
+        "P6": "monotone auditability"
+      },
+      "headline": "the RAG->MCP->kernel loop is proven end-to-end; P3 (poisoned input can't flip the verdict) is the Cannonico bullseye",
+      "maturity": "experimental-CI-green (P5 axiom-gated)",
+      "locked_kernel": "749/14/163 @ c7c0ba17 UNCHANGED; experimental scope"
+    },
+    "coder_formulas": {
+      "campaign": "prove-coder (a11oy Code governed coder formulas)",
+      "pull_request": "https://github.com/szl-holdings/lutar-lean/pull/193",
+      "commit_ci_green": "29e33534",
+      "ci_status": "GREEN (bare-lean sorry-free + CI build/numbers/doctrine/DCO)",
+      "theorems": 27,
+      "axiom_free": 5,
+      "lean_core_only": 23,
+      "axiom_gated": 1,
+      "declared_axiom": "codeHash_collision_resistant (1 only; standard, disclosed)",
+      "areas": {
+        "CS1": "sandbox containment (extends P2)",
+        "CS2": "bounded exec/termination (extends F-G5)",
+        "CR3": "router envelope + argmin stability (W7-5/C20)",
+        "CV4": "consensus/Byzantine majority (C10)",
+        "CC5": "conformal code-confidence <1 (W5-3/W7-4)",
+        "CK6": "receipt-log compression (Kraft/Shannon C8/C9)",
+        "NI7": "code-context non-interference (extends P3) \u2014 poisoned dependency can't flip DENY->ALLOW"
+      },
+      "headline": "27 theorems innovated for the governed coder; kernel-verified two ways",
+      "maturity": "experimental-CI-green (1 axiom-gated)",
+      "locked_kernel": "749/14/163 @ c7c0ba17 UNCHANGED; experimental scope"
+    },
+    "lambda_setalpha_setdelta": {
+      "campaign": "lambda-uniqueness Set alpha + Set delta (conditional uniqueness within strengthened axiom classes)",
+      "pull_request": "https://github.com/szl-holdings/lutar-lean/pull/192",
+      "commit_ci_green": "5f0bb5ee",
+      "ci_status": "GREEN (build + lake+numbers + doctrine + DCO)",
+      "results": 22,
+      "headline_theorems_approx": 12,
+      "declared_bridge_axioms": [
+        "setAlpha_cauchy",
+        "KS_theorem_1_1",
+        "setDelta_stage2"
+      ],
+      "impostor_deaths_axiom_free": 10,
+      "what_proven": "Lambda (geometric mean) is UNIQUE within Set alpha {A1,A2,A3,A4,A5' multiplicativity} (cond. on setAlpha_cauchy) and within Set delta {d1..d4,d5' multiplicativity} (cond. on KS_theorem_1_1+setDelta_stage2). All 10 impostor-deaths AXIOM-FREE.",
+      "what_NOT_claimed": "NOT unconditional uniqueness under original A1-A5 (machine-checked FALSE: Round13.maxAgg_ne_Lambda). Lambda STAYS Conjecture 1.",
+      "maturity": "conditional (axiom-gated bridge); Lambda = Conjecture 1 unconditionally",
+      "locked_kernel": "749/14/163 @ c7c0ba17 UNCHANGED; locked_proven STAYS 5"
+    },
+    "mathlib_bump_c3c4c5": {
+      "campaign": "Mathlib v4.18 bump \u2014 concentration/KL re-exports C3/C4/C5",
+      "pull_request": "https://github.com/szl-holdings/lutar-lean/pull/187",
+      "ci_status": "PROVEN on the Mathlib-v4.18 bump branch (CI-green), PENDING MERGE to main",
+      "ids": [
+        "C3",
+        "C4",
+        "C5"
+      ],
+      "status_honest": "proven on bump branch (PR#187), pending merge to main \u2014 NOT on-main, NOT blocked",
+      "maturity": "branch-pending"
+    },
+    "unify_governed_run_sound": {
+      "campaign": "unify governance substrate meta-theorem (monoid-action spine unifying P1/P4/P6 + coder corpus)",
+      "pull_request": "https://github.com/szl-holdings/lutar-lean/pull/194",
+      "commit_ci_green": "9f9c1bbd",
+      "artifact": "Lutar/Unify/GovernanceSubstrate.lean (EXPERIMENTAL scope; NOT wired into Lutar.lean)",
+      "spine": "run is a left monoid action of the free monoid (List Hop,++,[]) on St; run_append homomorphism is the unifier",
+      "theorems": [
+        "run_nil (axiom-free)",
+        "run_append",
+        "run_singleton (axiom-free)",
+        "completeness_additive",
+        "determinism_composes",
+        "chainEnd_append (axiom-free)",
+        "auditability_multiplicative",
+        "governed_run_sound"
+      ],
+      "headline": "every compositional corpus guarantee is a corollary of one homomorphism; a synthesis (unification) theorem, not new deep pure math",
+      "maturity": "experimental-CI-green",
+      "locked_kernel": "749/14/163 @ c7c0ba17 UNCHANGED; experimental scope"
+    },
+    "maturity_legend": [
+      "locked",
+      "experimental-CI-green",
+      "branch-pending",
+      "axiom-gated",
+      "conditional",
+      "conjecture"
+    ],
+    "experimental_total_note": "LOCKED proven = exactly 5 {F1,F11,F12,F18,F19} @ c7c0ba17 (749/14/163), UNCHANGED. PLUS 80+ experimental kernel-verified theorems (all CI-green, never folded into the locked 5): wave5 (11, PR#186), wave6 (11, PR#189), wave7 (10, PR#190), agentic-loop P1-P6 (28, PR#188), coder formulas (27, PR#193), Lambda Set alpha/delta (22 results / ~12 theorems, PR#192), unify governed_run_sound (PR#194). C3/C4/C5 proven on the Mathlib-v4.18 bump branch (PR#187), pending merge to main. Lambda = Conjecture 1 unconditionally (uniqueness machine-checked FALSE) + PROVEN conditionally under declared strengthened Set alpha/delta axioms (PR#192).",
+    "experimental_count_min": 80
+  },
+  "puriq_formulas": [
+    {
+      "id": "F1",
+      "name": "Replay-Hash Determinism",
+      "statement": "Deterministic step-fold replay: equal logs replay to equal final state; folded state equals last of the explicit replay trace.",
+      "maturity": "proven",
+      "lean_ref": "f1_replay_fold_deterministic",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean",
+      "locked_kernel": true
+    },
+    {
+      "id": "F2",
+      "name": "Scheduler Liveness",
+      "statement": "Fair round-robin scheduler: every ready organ eventually ticks (strictly-decreasing Nat ranking measure reaches 0).",
+      "maturity": "proven",
+      "lean_ref": "f2_scheduler_liveness",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean"
+    },
+    {
+      "id": "F3",
+      "name": "Organ Boot-Gate Soundness",
+      "statement": "If the boot gate permits an organ, its genome is valid (decidable implication).",
+      "maturity": "proven",
+      "lean_ref": "f3_genome_gate_sound",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean"
+    },
+    {
+      "id": "F4",
+      "name": "Receipt-Chain Acyclicity",
+      "statement": "Appending the new largest-index node preserves DAG acyclicity (backward-edge invariant).",
+      "maturity": "proven",
+      "lean_ref": "f4_khipu_dag_acyclic",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean"
+    },
+    {
+      "id": "F5",
+      "name": "Unay Receipt Recall",
+      "statement": "Insert-then-lookup on the same receipt key returns the inserted value (exact-key recall correctness).",
+      "maturity": "proven",
+      "lean_ref": "f5_unay_recall_correct",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean"
+    },
+    {
+      "id": "F6",
+      "name": "LMDB Durability",
+      "statement": "Commit-then-restart-then-read returns the committed value; uncommitted writes are lost on crash (WAL model).",
+      "maturity": "proven",
+      "lean_ref": "f6_lmdb_durability",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean"
+    },
+    {
+      "id": "F7",
+      "name": "Chaski FIFO Ordering",
+      "statement": "Enqueue-batch-then-drain yields send order; head is the oldest message (true FIFO, no tautology).",
+      "maturity": "proven",
+      "lean_ref": "f7_chaski_fifo",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean"
+    },
+    {
+      "id": "F8",
+      "name": "Wallpa OSS-Only Safety",
+      "statement": "Governed-voice admission gate admits only OSS sources; no humanClone or synthetic config is ever admitted.",
+      "maturity": "proven",
+      "lean_ref": "f8_wallpa_oss_only",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean"
+    },
+    {
+      "id": "F9",
+      "name": "Wasi-Rikuq Non-Interference",
+      "statement": "Advisory non-interference (Goguen-Meseguer 1982): the low view is unchanged by high inputs.",
+      "maturity": "proven",
+      "lean_ref": "f9_wasi_rikuq_noninterference",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean"
+    },
+    {
+      "id": "F10",
+      "name": "Hatun MCP Idempotency",
+      "statement": "MCP request normalizer is idempotent: normalizing twice equals normalizing once.",
+      "maturity": "proven",
+      "lean_ref": "f10_hatun_mcp_idempotent",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean"
+    },
+    {
+      "id": "F11",
+      "name": "Ayni Reciprocity Conservation",
+      "statement": "Event-sourcing replay invariant: balance reciprocity is conserved; tit-for-tat parity (Axelrod-Hamilton).",
+      "maturity": "proven",
+      "lean_ref": "f11_ayni_reciprocity_conservation",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean",
+      "locked_kernel": true
+    },
+    {
+      "id": "F12",
+      "name": "Kuramoto Phase-Coupling Boundedness",
+      "statement": "Discrete additive coupling is bounded and superposes over an organ set. CAVEAT: additive fragment only, NOT nonlinear Kuramoto synchronisation.",
+      "maturity": "proven",
+      "lean_ref": "f12_kuramoto_superposition",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean",
+      "locked_kernel": true
+    },
+    {
+      "id": "F13",
+      "name": "Wayra Hash-Chain Verification",
+      "statement": "Hash-chain verification is sound by induction: a verified chain has every link consistent.",
+      "maturity": "proven",
+      "lean_ref": "f13_wayra_chain_verified",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean",
+      "declared_axiom": "hash_collision_resistant (tamper-evidence f13_tamper_evident)"
+    },
+    {
+      "id": "F14",
+      "name": "Signature Verifiable Attribution",
+      "statement": "A signature-envelope signature that verifies attributes the message to the key. AXIOM-GATED on declared `ecdsa_unforgeable`.",
+      "maturity": "axiom-gated",
+      "lean_ref": "f14_dsse_verifiable",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean",
+      "declared_axiom": "ecdsa_unforgeable"
+    },
+    {
+      "id": "F15",
+      "name": "Rekor Merkle Inclusion",
+      "statement": "Merkle inclusion checker is sound (structural). Binding form (equal roots => equal leaves) is AXIOM-GATED on declared `h2_collision_resistant`.",
+      "maturity": "proven",
+      "lean_ref": "f15_rekor_inclusion",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean",
+      "declared_axiom": "h2_collision_resistant (binding form f15_inclusion_binding)"
+    },
+    {
+      "id": "F16",
+      "name": "Safety-Gate Coverage Completeness",
+      "statement": "Immune cross-cut completeness: 8 gates cover all 8 enumerated threats; gate set is exhaustive.",
+      "maturity": "proven",
+      "lean_ref": "f16_safegate_immune_complete",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean"
+    },
+    {
+      "id": "F17",
+      "name": "Three-Vertical Isolation",
+      "statement": "The three verticals are pairwise disjoint (isolation by construction).",
+      "maturity": "proven",
+      "lean_ref": "f17_three_vertical_isolation",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean"
+    },
+    {
+      "id": "F18",
+      "name": "Reed-Solomon RS(10,6) Recovery",
+      "statement": "RS(10,6) parity arithmetic: data is recoverable iff at least 6 of 10 shards survive (tolerates 4 erasures).",
+      "maturity": "proven",
+      "lean_ref": "f18_reed_solomon_parity_count",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean",
+      "locked_kernel": true
+    },
+    {
+      "id": "F19",
+      "name": "Bekenstein Entropy Budget",
+      "statement": "Entropy budget is additive and monotone over a region partition; each region <= total. CAVEAT: additive scaffolding only, NOT the full Bekenstein bound S <= 2*pi*k*R*E/(hbar*c).",
+      "maturity": "proven",
+      "lean_ref": "f19_budget_total_cons",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean",
+      "locked_kernel": true
+    },
+    {
+      "id": "F20",
+      "name": "Mobile Input Equivalence",
+      "statement": "Touch and pointer inputs are equivalent under the normalization map (decidable and sound).",
+      "maturity": "proven",
+      "lean_ref": "f20_mobile_input_equiv",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean"
+    },
+    {
+      "id": "F21",
+      "name": "Genome Validator Totality",
+      "statement": "The genome validator is total over Fin 16: every organ validates.",
+      "maturity": "proven",
+      "lean_ref": "f21_all_organs_valid",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean"
+    },
+    {
+      "id": "F22",
+      "name": "Receipt Emit Monotonicity",
+      "statement": "Emit appends to the sequence log with strictly increasing sequence numbers (monotone emit).",
+      "maturity": "proven",
+      "lean_ref": "f22_khipu_emit_monotone",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/PuriqFormulaLean.lean"
+    },
+    {
+      "id": "F23",
+      "name": "Lambda-Aggregator Uniqueness",
+      "statement": "CONJECTURE 1 (NOT a theorem). Unconditional uniqueness is FALSE under A1-A5 (maxAgg counterexample). Conditional `lambda_unique_of_factors` IS proved; unconditional uniqueness closes only under declared axiom A6_bisymmetric.",
+      "maturity": "conjectured",
+      "lean_ref": "f23_lambda_aggregator_sound",
+      "lean_repo": "szl-holdings/lutar-lean",
+      "lean_file": "Lutar/Puriq/Formulas/F23_Uniqueness.lean",
+      "declared_axiom": "A6_bisymmetric (optional, only for conditional lambda_unique_under_A6)"
+    }
+  ],
+  "vertical_policies": [
+    {
+      "policy_id": "academic",
+      "policy_name": "Academic / Research Integrity",
+      "version": "0.3.0",
+      "regulations": [
+        "NIH NOT-OD-23-149",
+        "NSF PAPPG Chapter II.E",
+        "ORI Standards",
+        "COPE Guidelines"
+      ],
+      "required_attestors": [
+        "principal_investigator",
+        "research_integrity_officer"
+      ],
+      "lambda_floors": {
+        "measurabilityHonesty": 1.0,
+        "constructiveTransparency": 1.0,
+        "informationIntegrity": 0.99,
+        "temporalConsistency": 0.99
+      },
+      "forbidden_inputs": [
+        "undisclosed_ai_authored_content",
+        "missing_doi_citation"
+      ],
+      "required_output_formats": [
+        "zenodo_deposit",
+        "json_receipt",
+        "orcid_linked_artifact"
+      ],
+      "retention_days": "3650",
+      "primitives_applicable": [
+        "A5",
+        "A8",
+        "A12",
+        "T5",
+        "T10",
+        "TH2"
+      ],
+      "acv_range_usd": {
+        "low": 10000.0,
+        "mid": 50000.0,
+        "high": 200000.0
+      }
+    },
+    {
+      "policy_id": "capital_markets",
+      "policy_name": "Capital Markets / Quant / Hedge Funds",
+      "version": "0.3.0",
+      "regulations": [
+        "SEC Rule 17a-4",
+        "MiFID II RTS 6",
+        "FINRA Rule 4370",
+        "Reg SCI 17 CFR 242"
+      ],
+      "required_attestors": [
+        "chief_compliance_officer",
+        "quant_review_committee",
+        "external_auditor"
+      ],
+      "lambda_floors": {
+        "moralGrounding": 0.97,
+        "measurabilityHonesty": 1.0,
+        "temporalConsistency": 1.0,
+        "economicGrounding": 1.0,
+        "constructiveTransparency": 0.99,
+        "informationIntegrity": 0.99
+      },
+      "forbidden_inputs": [
+        "non_sec_registered_model",
+        "missing_algo_documentation"
+      ],
+      "required_output_formats": [
+        "sec_17a4_compliant_log",
+        "json_receipt",
+        "worm_storage_manifest"
+      ],
+      "retention_days": "2190",
+      "primitives_applicable": [
+        "A5",
+        "A6",
+        "A10",
+        "A12",
+        "A14",
+        "T5",
+        "T9",
+        "TH2"
+      ],
+      "acv_range_usd": {
+        "low": 500000.0,
+        "mid": 2000000.0,
+        "high": 10000000.0
+      }
+    },
+    {
+      "policy_id": "critical_infrastructure",
+      "policy_name": "Critical Infrastructure / Utilities",
+      "version": "0.3.0",
+      "regulations": [
+        "NERC CIP-013-2",
+        "IEC 62443-3-3",
+        "TSA Pipeline Security Directive SD-02C",
+        "NIST CSF 2.0"
+      ],
+      "required_attestors": [
+        "system_security_officer",
+        "control_systems_engineer",
+        "incident_commander"
+      ],
+      "lambda_floors": {
+        "moralGrounding": 0.99,
+        "actionReversibility": 0.99,
+        "scopeContainment": 1.0,
+        "informationIntegrity": 0.99,
+        "adversarialRobustness": 0.99,
+        "temporalConsistency": 0.99
+      },
+      "forbidden_inputs": [
+        "unauthenticated_control_commands",
+        "non_air_gapped_ot_data"
+      ],
+      "required_output_formats": [
+        "ics_audit_log",
+        "json_receipt",
+        "nerc_compliance_report"
+      ],
+      "retention_days": "1825",
+      "primitives_applicable": [
+        "A4",
+        "A5",
+        "A6",
+        "A10",
+        "A13",
+        "T5",
+        "T9",
+        "T10",
+        "TH1"
+      ],
+      "acv_range_usd": {
+        "low": 1000000.0,
+        "mid": 5000000.0,
+        "high": 20000000.0
+      }
+    },
+    {
+      "policy_id": "defense",
+      "policy_name": "Defense / DoD",
+      "version": "0.3.0",
+      "regulations": [
+        "NIST SP 800-53 Rev 5",
+        "CMMC 2.0",
+        "FedRAMP High",
+        "DISA STIGs"
+      ],
+      "required_attestors": [
+        "authorizing_official",
+        "system_owner",
+        "security_control_assessor"
+      ],
+      "lambda_floors": {
+        "moralGrounding": 0.99,
+        "measurabilityHonesty": 0.99,
+        "actionReversibility": 0.95,
+        "scopeContainment": 0.99,
+        "informationIntegrity": 0.99,
+        "consentBoundary": 0.95
+      },
+      "forbidden_inputs": [
+        "unclassified_cui_without_marking",
+        "foreign_national_data"
+      ],
+      "required_output_formats": [
+        "json_audit_log",
+        "nist_oscal"
+      ],
+      "retention_days": "7300",
+      "primitives_applicable": [
+        "A1",
+        "A4",
+        "A5",
+        "A6",
+        "A8",
+        "A9",
+        "A12",
+        "A13",
+        "T5",
+        "T9",
+        "T10",
+        "TH1"
+      ],
+      "acv_range_usd": {
+        "low": 500000.0,
+        "mid": 2000000.0,
+        "high": 5000000.0
+      }
+    },
+    {
+      "policy_id": "financial_services",
+      "policy_name": "Financial Services / Banking",
+      "version": "0.3.0",
+      "regulations": [
+        "SR 11-7",
+        "OCC 2011-12",
+        "MiFID II RTS 6",
+        "Basel III"
+      ],
+      "required_attestors": [
+        "model_risk_officer",
+        "chief_risk_officer",
+        "internal_audit"
+      ],
+      "lambda_floors": {
+        "moralGrounding": 0.97,
+        "measurabilityHonesty": 0.99,
+        "temporalConsistency": 0.99,
+        "informationIntegrity": 0.99,
+        "economicGrounding": 1.0
+      },
+      "forbidden_inputs": [
+        "insider_information",
+        "unregistered_model_version"
+      ],
+      "required_output_formats": [
+        "csv_model_log",
+        "json_receipt",
+        "pdf_board_report"
+      ],
+      "retention_days": "2190",
+      "primitives_applicable": [
+        "A1",
+        "A5",
+        "A6",
+        "A8",
+        "A9",
+        "A14",
+        "T5",
+        "T9",
+        "T10",
+        "TH1",
+        "TH2"
+      ],
+      "acv_range_usd": {
+        "low": 200000.0,
+        "mid": 800000.0,
+        "high": 2000000.0
+      }
+    },
+    {
+      "policy_id": "healthcare",
+      "policy_name": "Healthcare / Clinical AI",
+      "version": "0.3.0",
+      "regulations": [
+        "HIPAA 45 CFR Part 164",
+        "FDA 21 CFR Part 11",
+        "FDA SaMD Guidance Q3 2023"
+      ],
+      "required_attestors": [
+        "licensed_clinician",
+        "clinical_informatics_officer",
+        "hipaa_privacy_officer"
+      ],
+      "lambda_floors": {
+        "moralGrounding": 0.99,
+        "measurabilityHonesty": 0.99,
+        "consentBoundary": 0.99,
+        "informationIntegrity": 0.99,
+        "causalSeparability": 0.99
+      },
+      "forbidden_inputs": [
+        "plaintext_phi",
+        "deidentification_not_verified"
+      ],
+      "required_output_formats": [
+        "hl7_fhir_audit",
+        "json_receipt",
+        "pdf_clinical_audit"
+      ],
+      "retention_days": "2190",
+      "primitives_applicable": [
+        "A1",
+        "A4",
+        "A5",
+        "A8",
+        "A9",
+        "A11",
+        "A12",
+        "T5",
+        "T7",
+        "T10",
+        "TH1"
+      ],
+      "acv_range_usd": {
+        "low": 150000.0,
+        "mid": 600000.0,
+        "high": 2000000.0
+      }
+    },
+    {
+      "policy_id": "insurance",
+      "policy_name": "Insurance",
+      "version": "0.3.0",
+      "regulations": [
+        "NAIC Model Law 881",
+        "NY DFS Circular Letter 7 (2022)",
+        "NAIC AI Principles (2020)"
+      ],
+      "required_attestors": [
+        "chief_actuary",
+        "ai_ethics_board",
+        "compliance_officer"
+      ],
+      "lambda_floors": {
+        "moralGrounding": 0.97,
+        "measurabilityHonesty": 0.99,
+        "informationIntegrity": 0.99,
+        "constructiveTransparency": 0.99,
+        "economicGrounding": 0.97
+      },
+      "forbidden_inputs": [
+        "prohibited_rating_factors",
+        "non_actuarially_justified_proxies"
+      ],
+      "required_output_formats": [
+        "csv_underwriting_log",
+        "json_receipt",
+        "pdf_state_filing"
+      ],
+      "retention_days": "1825",
+      "primitives_applicable": [
+        "A1",
+        "A5",
+        "A8",
+        "A9",
+        "A12",
+        "A14",
+        "T6",
+        "T9",
+        "T10"
+      ],
+      "acv_range_usd": {
+        "low": 200000.0,
+        "mid": 750000.0,
+        "high": 2000000.0
+      }
+    },
+    {
+      "policy_id": "legal",
+      "policy_name": "Legal / e-Discovery",
+      "version": "0.3.0",
+      "regulations": [
+        "FRCP 26",
+        "FRCP 34",
+        "FRE 902(13)",
+        "FRE 902(14)",
+        "ABA Model Rule 1.1"
+      ],
+      "required_attestors": [
+        "supervising_attorney",
+        "records_custodian"
+      ],
+      "lambda_floors": {
+        "moralGrounding": 0.97,
+        "measurabilityHonesty": 0.99,
+        "informationIntegrity": 0.99,
+        "constructiveTransparency": 0.99,
+        "actionReversibility": 0.95
+      },
+      "forbidden_inputs": [
+        "privileged_attorney_client_without_waiver"
+      ],
+      "required_output_formats": [
+        "json_chain_of_custody",
+        "pdf_court_exhibit"
+      ],
+      "retention_days": "2555",
+      "primitives_applicable": [
+        "A5",
+        "A6",
+        "A8",
+        "A12",
+        "T5",
+        "T8",
+        "T10",
+        "TH2"
+      ],
+      "acv_range_usd": {
+        "low": 75000.0,
+        "mid": 300000.0,
+        "high": 1000000.0
+      }
+    },
+    {
+      "policy_id": "pharma",
+      "policy_name": "Pharma / Life Sciences R&D",
+      "version": "0.3.0",
+      "regulations": [
+        "FDA 21 CFR Part 11",
+        "EMA Annex 11",
+        "ICH E6(R3) GCP",
+        "GxP"
+      ],
+      "required_attestors": [
+        "qualified_person",
+        "gxp_compliance_officer",
+        "computational_scientist"
+      ],
+      "lambda_floors": {
+        "moralGrounding": 0.97,
+        "measurabilityHonesty": 1.0,
+        "informationIntegrity": 1.0,
+        "temporalConsistency": 0.99,
+        "constructiveTransparency": 1.0
+      },
+      "forbidden_inputs": [
+        "non_gxp_validated_software_output",
+        "unversioned_model"
+      ],
+      "required_output_formats": [
+        "ectd_submission_package",
+        "json_audit_trail",
+        "csv_gxp_log"
+      ],
+      "retention_days": "3650",
+      "primitives_applicable": [
+        "A5",
+        "A6",
+        "A8",
+        "A10",
+        "A12",
+        "T5",
+        "TH2"
+      ],
+      "acv_range_usd": {
+        "low": 500000.0,
+        "mid": 2000000.0,
+        "high": 10000000.0
+      }
+    },
+    {
+      "policy_id": "public_sector",
+      "policy_name": "Public Sector / Civic AI",
+      "version": "0.3.0",
+      "regulations": [
+        "EU AI Act Annex III",
+        "NYC Local Law 144 (2023)",
+        "NIST AI RMF 1.0",
+        "OMB M-24-10"
+      ],
+      "required_attestors": [
+        "agency_ai_officer",
+        "civil_rights_officer",
+        "inspector_general"
+      ],
+      "lambda_floors": {
+        "moralGrounding": 0.99,
+        "measurabilityHonesty": 0.99,
+        "stakeholderAlignment": 0.99,
+        "constructiveTransparency": 1.0,
+        "adversarialRobustness": 0.95
+      },
+      "forbidden_inputs": [
+        "biometric_data_without_explicit_consent",
+        "prohibited_social_scoring"
+      ],
+      "required_output_formats": [
+        "json_public_audit_log",
+        "csv_bias_audit",
+        "pdf_annual_report"
+      ],
+      "retention_days": "3650",
+      "primitives_applicable": [
+        "A1",
+        "A5",
+        "A8",
+        "A12",
+        "A13",
+        "T6",
+        "T10",
+        "TH1",
+        "TH3"
+      ],
+      "acv_range_usd": {
+        "low": 300000.0,
+        "mid": 1200000.0,
+        "high": 5000000.0
+      }
+    }
+  ],
+  "instill_wave": "build-wave (locked 5 + wave3 19 sorry-free/4 axiom-gated + wave5 6 Mathlib-CI-green/5 bare-lean + conditional Lambda)"
 }