SZL Holdings is a governed decision-intelligence substrate for regulated enterprises — a Λ-axis audit-closure operator, proved in Lean 4 (Mathlib v4.13.0), running at sub-millisecond overhead, emitting a SHA-pinned receipt for every decision.
Org page: github.com/szl-holdings
| Metric | Count | Source |
|---|---|---|
| Named Lean theorems | 76 | lutar-lean |
| Lake-verified proofs | 134 | Mathlib v4.13.0 |
| GREEN Lean modules | 30 / 30 | CI · lutar-lean |
| HF Spaces (live) | 19 | SZLHOLDINGS |
| Zenodo DOIs | 7 | concept + v18 master + v18 software + v17/v16/v15/v14 |
| Thesis versions published | 18 | v1 → v18 · ouroboros-thesis |
| Org repos | 19 | szl-holdings |
Thesis v18.0 — published 2026-05-29.
- Master DOI:
10.5281/zenodo.20434276 - Software DOI:
10.5281/zenodo.20434308 - Concept DOI (always latest):
10.5281/zenodo.19944926
Warhacker 2026 (June 16–20) — SZL Governance Receipts on UDS. k3d + uds-cli + Pepr DSSE receipt policy. Tracked in szl-holdings/platform (Warhacker deployment branch).
AIMS@COLM26 — T4 / T13 extended abstracts queued in ouroboros-thesis/aims_colm26/ (in-progress).
Runtime overhead — ≤ 0.59 ms median per request. Measured across 24,800 paired HTTP calls (v11 bench, 10.5281/zenodo.20119582).
Six repos pinned in GitHub UI. Pin them at github.com/stephenlutar2-hash:
| Repo | What it is |
|---|---|
szl-holdings/a11oy |
Brand orchestration + AI governance surface |
szl-holdings/lutar-lean |
Lean 4 + Mathlib kernel proofs · 30 GREEN modules |
szl-holdings/ouroboros |
Bounded-recursion runtime · Λ-gate · receipt emission |
szl-holdings/ouroboros-thesis |
DOI-pinned thesis substrate · v1 → v18 |
szl-holdings/uds-mesh |
UDS span schemas + governance receipts |
szl-holdings/sentra |
Cyber-resilience command surface |
flowchart TD
classDef research fill:#28251D,stroke:#C8B26A,color:#F7F6F2;
classDef kernel fill:#1F3B73,stroke:#2D5BB9,color:#F7F6F2;
classDef runtime fill:#1B474D,stroke:#01696F,color:#F7F6F2;
classDef platform fill:#01696F,stroke:#C8B26A,color:#F7F6F2;
classDef surface fill:#0a0a0f,stroke:#00d4ff,color:#e0e8ef;
T["Ouroboros Thesis<br/>v1 → v18 published<br/>concept DOI 10.5281/zenodo.19944926"]:::research
L["Lutar-Lean<br/>Lean 4 + Mathlib v4.13.0<br/>30 GREEN modules · 76 theorems"]:::kernel
R["Ouroboros Runtime<br/>Λ-gate · receipt bus · Bekenstein<br/>≤ 0.59 ms median overhead"]:::runtime
P["SZL Holdings Platform<br/>19 public repos · 7 vertical surfaces"]:::platform
A["A11oy"]:::surface
S["Sentra"]:::surface
AM["Amaru"]:::surface
V["Vessels"]:::surface
TE["Terra"]:::surface
C["Counsel"]:::surface
CJ["Carlota Jo"]:::surface
T --> L
T --> R
L -.bit-exact JSON.-> R
R --> P
P --> A & S & AM & V & TE & C & CJ
18 published versions. Every claim terminates in a DOI, a commit SHA, a Lean theorem, or a CI run.
| Version | Title | DOI |
|---|---|---|
| v18.0 | Λ-Axis Substrate for Verifiable Agentic AI — doctrine v6, 11 axioms, 30 GREEN modules | 10.5281/zenodo.20434276 |
| v18.0.0 (software) | Reference runtime + Lean kernel for v18 | 10.5281/zenodo.20434308 |
| v17 | 10.5281/zenodo.20431181 |
|
| v16 | 10.5281/zenodo.20424996 |
|
| v15 | 10.5281/zenodo.20424995 |
|
| v14 | 10.5281/zenodo.20424992 |
|
| v11 | APPLIED-Λ — Measured per-request overhead | 10.5281/zenodo.20119582 |
| v10 | EXHAUSTIVE-AUDIT — Λ₁₀ audit closure | 10.5281/zenodo.20053163 |
| v9 | UNIFIED-OPERATIONAL — Lutar family + Bianchi closure | 10.5281/zenodo.20053148 |
| v3 | The Lutar Invariant — axiomatic trust aggregator | 10.5281/zenodo.19983066 |
| v2 | Empirical companion — A11oy / Sentra / Amaru | 10.5281/zenodo.19934129 |
| v1 | Position paper — bounded looped computation | 10.5281/zenodo.19867281 |
Concept DOI (always latest): 10.5281/zenodo.19944926
- Lean-kernel proof that
Λ_k(x) = (∏ xᵢ)^(1/k)is the unique aggregator satisfying axioms A1–A4 (monotone · homogeneous · Egyptian-exact · bounded). Source. - Bit-exact reproduction of Λ₉ on published golden vectors across three production runtimes (a11oy / amaru / sentra) and the Lean Float implementation. Reference vectors.
- Measured per-request overhead across 24,800 paired HTTP calls (v11 paper,
10.5281/zenodo.20119582). - Not a quantum computer. Quantum modules use quantum-analogy math to derive bounds on classical hardware.
- Not a free-energy device. "Free-energy" is Friston variational FEP, not thermodynamic free energy.
Languages: TypeScript · Python · Lean 4 · Bash Runtime: Node.js 24 · pnpm 10 · React · Vite Data: PostgreSQL (Neon) · Drizzle ORM · Redis · pgvector Cloud: Hetzner · Cloudflare · Sigstore · Zenodo Quality: Vitest · Playwright · CodeQL · Trivy · Gitleaks · OpenSSF Scorecard · Lean kernel Observability: OpenTelemetry · Pino · PM2
| Metric | Value |
|---|---|
| Today's commits across szl-holdings | see workflow |
| Active PRs | see workflow |
| Latest thesis DOI | 10.5281/zenodo.20434276 (v18.0) |
Stephen P. Lutar Jr. — Founder & CEO, SZL Holdings
stephen@szlholdings.com |
|
| ORCID | 0009-0001-0110-4173 |
| stephen-l-279315240 | |
| HF | huggingface.co/betterwithage · org SZLHOLDINGS |
| Zenodo | zenodo.org/communities/szl-holdings |
| Web | szlholdings.com |
| Security | security@szlholdings.com · security policy |
© 2026 Stephen P. Lutar Jr. — Code: Apache-2.0. Research: CC BY 4.0. Every test count and DOI on this page is verifiable; see linked audit logs and reference-vectors.json. Profile auto-refreshed by update-stats.yml.



