a11oy.net pages: doctrine-honest proof state (Wave23 Khipu BFT=Conj2, codename->roles, SLSA L1/L2 roadmap) — byte-identical with GitHub

cathedral.html

@@ -264,8 +264,9 @@ footer{position:relative;z-index:10;border-top:1px solid var(--line);padding:40p
         <div class="metrics">
           <div class="metric reveal"><div class="n">5</div><div class="k">Locked proven formulas</div><div class="c">{F1, F11, F12, F18, F19} kernel-verified @ c7c0ba17 · machine-enforced count</div></div>
           <div class="metric reveal"><div class="n">28</div><div class="k">Kernel-verified loop theorems</div><div class="c">P1–P6 governed run loop — gate-sound, injection-resistant, auditable end-to-end</div></div>
-          <div class="metric reveal"><div class="n">1304 / 22</div><div class="k">Experimental decl / axioms</div><div class="c">waves 3–10 CI-green (~36–44 theorems) · excluded from the locked count</div></div>
-          <div class="metric warn reveal"><div class="n">Λ = Conj. 1</div><div class="k">Aggregator uniqueness</div><div class="c">a named conjecture, NOT a theorem — unconditional uniqueness machine-checked false</div></div>
+          <div class="metric reveal"><div class="n">~190</div><div class="k">Experimental CI-green theorems</div><div class="c">waves 11–23 · labelled experimental, excluded from the locked count · conditional Λ uniqueness IS proven axiom-free (Wave 22)</div></div>
+          <div class="metric warn reveal"><div class="n">Λ = Conj. 1</div><div class="k">Aggregator uniqueness</div><div class="c">a named conjecture, NOT a theorem — <em>unconditional</em> uniqueness machine-checked false; conditional uniqueness proven axiom-free</div></div>
+          <div class="metric warn reveal"><div class="n">Khipu BFT = Conj. 2</div><div class="k">Consensus safety</div><div class="c">Wave 23 <code>khipu_quorum_safety_conditional</code> proves <em>conditional</em> agreement / no split-brain under n ≥ 3f+1 + honest non-equivocation, axiom-clean — unconditional safety stays a named conjecture</div></div>
         </div>
       </div>
     </section>

pages/company.html

@@ -243,8 +243,8 @@ footer{border-top:1px solid var(--line);padding:54px 0 40px}
   <!-- FLAGSHIP LINEUP -->
   <section class="wrap" id="flagships">
     <div class="eyebrow">The Flagship Lineup</div>
-    <p class="lead">Five flagships. <em>One</em> proven primitive underneath.</p>
-    <p class="body">The same tamper-evident, offline-verifiable record of <em>why a machine did what it did</em> runs beneath everything SZL builds. Two flagships are live today; three are the frontier we are building toward — named as ambition, not achievement.</p>
+    <p class="lead">Two shipping products. <em>One</em> proven primitive underneath — and a frontier roadmap.</p>
+    <p class="body">The same tamper-evident, offline-verifiable record of <em>why a machine did what it did</em> runs beneath everything SZL builds. Two products are live today; the rest are the frontier roles we are building toward — named as ambition, not achievement.</p>
     <div class="cards">
       <div class="card proven">
         <div class="tag-row"><span class="code">a11oy</span><span class="pill pill-live">Live</span></div>
@@ -259,19 +259,19 @@ footer{border-top:1px solid var(--line);padding:54px 0 40px}
         <div class="meta">counter-UAS · signed verdicts</div>
       </div>
       <div class="card frontier">
-        <div class="tag-row"><span class="code">amaru</span><span class="pill pill-frontier">Frontier</span></div>
+        <div class="tag-row"><span class="code">provenance-anchor</span><span class="pill pill-frontier">Frontier</span></div>
         <h3>Provenance Anchor</h3>
         <p>Anchoring governance receipts to a public ledger, with post-quantum-hardened provenance, so a record's existence is independently witnessed beyond any single operator. Staged; not yet exercised live.</p>
         <div class="meta">ledger anchoring · PQ provenance</div>
       </div>
       <div class="card frontier">
-        <div class="tag-row"><span class="code">sentra</span><span class="pill pill-frontier">Frontier</span></div>
+        <div class="tag-row"><span class="code">policy</span><span class="pill pill-frontier">Frontier</span></div>
         <h3>Drift Detector</h3>
         <p>Continuous detection of behavioral drift — a system quietly diverging from its governed posture — on a dedicated observability axis. The research ambition is resilience that watches itself. Staged.</p>
         <div class="meta">drift observability · self-watch</div>
       </div>
       <div class="card frontier">
-        <div class="tag-row"><span class="code">rosie</span><span class="pill pill-frontier">Frontier</span></div>
+        <div class="tag-row"><span class="code">operator</span><span class="pill pill-frontier">Frontier</span></div>
         <h3>Receipt Orchestration</h3>
         <p>A control plane that manages, verifies, and routes proofs across an entire agentic fleet. The receipts it would orchestrate are real today; the orchestration layer itself is conceptual. Staged.</p>
         <div class="meta">fleet control plane · proof routing</div>
@@ -279,7 +279,7 @@ footer{border-top:1px solid var(--line);padding:54px 0 40px}
     </div>
     <div class="honest">
       <span class="tag">// the frontier rule</span>
-      <p>amaru, sentra and rosie are <strong>roadmap</strong>. The quantum and ledger language describes where the research is pointed, not capability you can run today. An investor doing technical due diligence will find exactly that — stated here first. The proven core is above; this is the upside, honestly drawn.</p>
+      <p>The Provenance Anchor, Policy and Operator roles are <strong>roadmap</strong>. The quantum and ledger language describes where the research is pointed, not capability you can run today. An investor doing technical due diligence will find exactly that — stated here first. The proven core is above; this is the upside, honestly drawn.</p>
     </div>
   </section>