Org front door: Anthropic-style funnel to a-11-oy.com (one flagship, company-page-vs-product-console pattern)

README.md

@@ -8,137 +8,50 @@ pinned: true
 ---
 
 <!--
-  Hugging Face org card — SZLHOLDINGS/README. GENIUS REVAMP v2. Honesty doctrine LOCKED.
-  Edited FROM _hf_org_card.md + PROVEN_STATE_CANONICAL.md. YAML frontmatter preserved exactly.
-  Canonical: 749 decl / 14 unique axioms / 163 tracked proof placeholders · kernel c7c0ba17.
-  Locked-proven = EXACTLY 8 {F1,F4,F7,F11,F12,F18,F19,F22} (was 5; F4/F7 upgraded from vacuous placeholders to genuine non-vacuous proofs 2026-06-10, joining already-genuine F22; machine-enforced by no-axiom Lean theorem locked_count_eight). ~185 machine-checked theorems (Waves 11-22); CUT-1 closed on stated hyps.
-  Lambda-uniqueness = Conjecture 1 (unconditional FALSE; conditional Theorem U proven, axiom-free).
-  SLSA = L1 honest posture; L2 build-attestation present; L2-verified/L3/FedRAMP/Iron Bank/CMMC = roadmap.
-  Honest roles only. killinchu UDS Edition NOT affiliated with Defense Unicorns. best GOVERNED LLM (a11oy Code).
-  Hero image expected at: hero-hf.png
+  Hugging Face org card — SZLHOLDINGS/README. Minimal funnel front door v3 · Honesty doctrine v11 LOCKED.
+  Pattern: company front door (this card) is separate from the product console (a-11-oy.com) — it FUNNELS in,
+  it does NOT duplicate console content. YAML frontmatter preserved exactly (sdk: static).
+  Canonical: Locked-proven = EXACTLY 8 {F1,F4,F7,F11,F12,F18,F19,F22}.
+  Λ-uniqueness = Conjecture 1 (unconditional machine-checked FALSE; conditional Theorem U proven, axiom-free).
+  SLSA = L1 honest · L2 build-attested · L3 roadmap. No FedRAMP/ATO/CMMC without "roadmap".
+  KANCHAY palette only (void #080c14 · proof #3af4c8 · lattice #5b8dee · gold #d7b96b). No purple. No a11oy.net (sunset).
 -->
 
 <div align="center">
 
-<img src="https://raw.githubusercontent.com/szl-holdings/.github/main/profile/assets/hero-hf.png" alt="SZL Holdings — governed AI you can prove" width="100%" />
-
 # 🛡️ SZL Holdings
 
-### The only AI governance layer that hands you a *mathematical proof* instead of asking for your trust.
-
-</div>
-
-Every consequential AI decision becomes a **cryptographically signed, replayable, tamper-evident receipt** — verifiable on your own laptop, trusting no one. Two live products run on one signed substrate, and the trust math underneath is pinned in **Lean 4** and checked by a machine. That backbone is what the observability and AI-security incumbents don't have.
-
----
-
-## ▸ Two products, one substrate
-
-| Product | What it does | Open it |
-|---|---|---|
-| **a11oy — Command Platform** | One pane of glass for governed AI: ask-&-act with deny-by-default safety gates, trust scoring with confidence intervals, a live decision feed, readiness & compliance, forecasting, signed receipts, formal-proof status, a live CVE / KEV / MITRE threat library, and model routing. | **[→ a11oy](https://szlholdings-a11oy.hf.space/)** |
-| **killinchu — Drones & Vessels** | Autonomous-systems field tool for air and sea: live track board, multi-sensor fusion, maritime picture (sanctions screening + dark-vessel detection), engagement rules, autonomy governance, and **verify-it-yourself** signed engagement receipts. | **[→ killinchu](https://szlholdings-killinchu.hf.space/elite)** |
-| **anatomy — 3D substrate** | Walk the live governance substrate in 3D: the Λ-gate, the Khipu hash-chain DAG, and the bounded-recursion loop, rendered as explorable geometry. | **[→ anatomy](https://szlholdings-anatomy.static.hf.space)** |
-
-**a11oy is the orchestrator** — its **Reasoning**, **Policy**, and **Operator** capabilities are built in as one receipt-bound fabric, and it governs the field tool with the same trust scoring, consensus, and signed receipts. The field tool runs edge governance on a **Field Node** that keeps emitting signed receipts even when the link degrades.
-
-> **killinchu UDS Edition** packages for [UDS](https://github.com/defenseunicorns/uds-core) deployment but is **not affiliated with, endorsed by, or sponsored by Defense Unicorns.** UDS is referenced for interoperability only.
-
----
-
-## ▸ The thesis
-
-Modern AI gives you answers; it does not give you **accountability**. SZL turns governance into a *substrate* — a **Proof Chain** where each decision is policy-checked, evidence-bound, scored by a single aggregator **Λ**, and sealed into a DSSE receipt over a SHA-256 hash chain.
-
-```text
-   decision ──▶ POLICY ──▶ EVIDENCE ──▶ Λ score ──▶ DSSE receipt ──▶ hash-chained ledger
-               (gates)    (bound)      (trust)      (signed)         (replayable · tamper-evident)
-```
-
-a11oy Code is built to be the **best GOVERNED LLM** within its governed envelope — not a frontier-weights claim, a governance claim.
-
----
-
-## ▸ The math, explained — without a PhD
-
-Three honesty labels: **LOCKED-PROVEN** (sorry-free, kernel-checked, Lean-core axioms only — **exactly 8**) · **MACHINE-CHECKED** (kernel-checked by CI, experimental scope) · **CONJECTURE** (not a theorem; stated honestly).
+### Governed AI you can prove — every decision comes with a signed, verifiable receipt.
 
-The locked-proven set is **exactly 8** — `{F1, F4, F7, F11, F12, F18, F19, F22}` — itself machine-enforced by the no-axiom Lean theorem `locked_count_eight`. It was 5 `{F1, F11, F12, F18, F19}` until **2026-06-10**, when **F4** and **F7** were upgraded from vacuous placeholders to genuine, non-vacuous, sorry-free Lean-core proofs, joining the already-genuine **F22**.
+[![locked-proven](https://img.shields.io/badge/locked--proven-8%20formulas-3af4c8?style=flat-square)](https://github.com/szl-holdings/lutar-lean)
+[![Lean 4](https://img.shields.io/badge/Lean%204-machine--checked-5b8dee?style=flat-square)](https://github.com/szl-holdings/lutar-lean)
+[![Λ](https://img.shields.io/badge/%CE%9B-Conjecture%201%20(never%20green)-7e8aa3?style=flat-square)](https://github.com/szl-holdings/lutar-lean)
+[![SLSA](https://img.shields.io/badge/SLSA-L1%20honest%20%C2%B7%20L2%20attested%20%C2%B7%20L3%20roadmap-d7b96b?style=flat-square)](https://slsa.dev/spec/v1.0/levels)
 
-**The 8 locked-proven formulas:**
+<br/>
 
-| ID | Plain-language meaning |
-|---|---|
-| **F1** | **Replay is deterministic** — same log + same start ⇒ bit-identical trace. The basis of a *replayable* receipt. |
-| **F4** | **Khipu-DAG acyclicity is preserved** — any path strictly decreases the node index, so no node reaches itself (acyclic), and appending a fresh max node preserves acyclicity. *Genuine (2026-06-10) — replaces the prior vacuous placeholder.* |
-| **F7** | **Chaski FIFO order is preserved** — the drained reception order equals the send order (and positionally, the i-th received = i-th sent). *Genuine (2026-06-10) — replaces the prior tautology placeholder.* |
-| **F11** | **Reciprocity is conserved** — an append-only give/take ledger keeps its balance invariant. |
-| **F12** | **Coupling stays bounded** (additive fragment only — *not* full nonlinear Kuramoto). |
-| **F18** | **Erasure recovery** — `RS(10,6)`: recover the data iff ≥ 6 of 10 shards survive. |
-| **F19** | **Entropy budget is additive & monotone** (scaffolding only — *not* the full Bekenstein bound). |
-| **F22** | **Khipu emit is append-only monotone** — sequence numbers strictly increase with position on the append-only log. *Genuine (already held in a prior sprint).* |
+## [Enter a11oy →](https://a-11-oy.com)
 
-**Λ — the honest line on uniqueness:**
-
-- Unconditional uniqueness under A1–A5 is **machine-checked FALSE** (`max`/`min` satisfy A1–A5 yet aren't Λ) → stays **Conjecture 1**.
-- Conditional uniqueness given **slice-multiplicativity (separability)** is the **REAL** result — **Theorem U** (and corollaries U₁/U₂), **MACHINE-CHECKED, axiom-free** (`#print axioms` ⊆ {propext, Classical.choice, Quot.sound}).
-
-Separately from — and never folded into — the locked 8, there are across Waves 11–22 about **~185 machine-checked theorems** (no `sorry`, no new axiom), including the full **binary Pinsker inequality** and **CUT-1** (the Aczel quasi-arithmetic representation theorem), now **fully closed on its stated hypotheses**. Full table → [lutar-lean/PROVEN_FORMULAS.md](https://github.com/szl-holdings/lutar-lean/blob/main/PROVEN_FORMULAS.md).
-
----
-
-## ▸ Verify it yourself — trust nothing
-
-```bash
-curl -s https://szlholdings-killinchu.hf.space/cosign.pub -o cosign.pub
-curl -s https://szlholdings-killinchu.hf.space/api/killinchu/v1/receipt/export > receipt.json
-# verify the DSSE signature offline  ->  "Verified OK"
-# tamper a single byte and re-verify ->  "Verification failure"
-```
-
-That's the whole product in one command: confirm a decision happened, exactly as recorded, with zero trust in SZL.
-
----
-
-## ▸ Honest proof status
-
-| We claim | We do **not** claim |
-|---|---|
-| **8 formulas locked-proven** in Lean (sorry-free): `F1, F4, F7, F11, F12, F18, F19, F22`. | The rest as "proven" — newer waves are **experimental / CI-green**, labeled. |
-| **~185 machine-checked theorems**; **CUT-1 closed on stated hypotheses**. | These as part of the locked 8. |
-| **Λ-uniqueness = Conjecture 1**; conditional uniqueness (Theorem U) proven axiom-free. | Λ as an unconditional theorem (unconditional is machine-checked **false**). |
-| **SLSA L1 honest posture; L2 build-attestation present.** | **L2-verified, L3, FedRAMP, Iron Bank, CMMC** = **roadmap**. |
-| Receipts genuinely signed where a key is present; **honestly unsigned** otherwise. | Fabricated signatures or metrics — ever. |
-| Maritime AIS uses a labeled **sample / replay** dataset. | A live production AIS feed. |
-| **best GOVERNED LLM** (a11oy Code) within its envelope. | "best LLM" / frontier-weights. |
-
-**Canonical:** kernel `c7c0ba17` · **749** declarations / **14** unique axioms / **163** tracked proof placeholders (honest markers, *not* a quality claim) · `lake build` clean.
-
-> The locked count of 8 is the on-disk Lean source-of-truth ([lutar-lean/PROVEN_FORMULAS.md](https://github.com/szl-holdings/lutar-lean/blob/main/PROVEN_FORMULAS.md)) and is machine-enforced by the no-axiom theorem `locked_count_eight`. Honest note: final founder Lean-runner `#print axioms` verification is PENDING before all served surfaces flip.
-
-> **Fleet command demonstration:** governance loop is real; effector link is **simulated** — labeled honestly as a command *demonstration*.
+</div>
 
 ---
 
-## ▸ Deploy — one signed bundle
-
-```bash
-uds deploy oci://ghcr.io/szl-holdings/szl-mesh:0.4.0 --confirm
-```
+## Spaces
 
-Cosign-signed; each image carries a build attestation. SLSA: **L1 honest posture; L2 build-attestation present; L2-verified / L3 = roadmap.**
+| Space | What it is | Open |
+|---|---|---|
+| **a11oy** — flagship | Governed-AI Command Center: ask-and-act behind deny-by-default gates, a live decision feed, and a signed receipt for every action. | **[a-11-oy.com](https://a-11-oy.com)** |
+| **killinchu** | Counter-UAS & maritime command *demonstration* — multi-sensor fusion with signed engagement receipts (effector link is a labeled simulation). | [demo →](https://szlholdings-killinchu.hf.space/elite) |
+| **anatomy** | Living anatomy map — the locked-8 ladder and the four honesty tiers, visualized. | [view →](https://szlholdings-anatomy.hf.space) |
+| **energy** | a11oy energy surface — joules MEASURED when a GPU lung is reachable, honest SAMPLE otherwise. | [view →](https://szlholdings-energy.hf.space) |
+| **david-leads** | Sovereign insurance intelligence — audit-defensible lead intelligence from public data only. | [view →](https://szlholdings-david-leads.hf.space) |
 
 ---
 
-## ▸ Collaborate
+<div align="center">
 
-We want design partners, auditors, and contributors who care about *provable* governance. Run the kernel. Break our receipts. Claim the open Λ bounty.
+**8 formulas locked-proven · Λ = Conjecture 1, never green · honest by design · public data only.**
 
-📄 Thesis (concept DOI): [`10.5281/zenodo.19944926`](https://doi.org/10.5281/zenodo.19944926)
-🧪 Math: [lutar-lean](https://github.com/szl-holdings/lutar-lean)
-🏢 Org: [github.com/szl-holdings](https://github.com/szl-holdings)
-✉️ [stephen@szlholdings.com](mailto:stephen@szlholdings.com)
+<sub><a href="https://github.com/szl-holdings/lutar-lean">lutar-lean</a> · <a href="https://github.com/szl-holdings">github.com/szl-holdings</a> · No production ATO claimed · SLSA L1 honest / L2 attested / L3 roadmap · trust ceiling 0.97, never 100%</sub>
 
----
-
-Built by **Stephen P. Lutar Jr.** · Honest by design · Headed to **Defense Unicorns Warhacker 2026** (16–19 June, San Diego).
+</div>