SZLHOLDINGS/a11oy-v19-substrate

a11oy v19 Substrate — Governance Policy Model

⚠️ This is a governance policy/spec card — not a loadable model. It ships documentation, manifests, proofs, and an eval trace — there is no weights/config artifact to from_pretrained. For live governed inference, use the Space: https://huggingface.co/spaces/SZLHOLDINGS/a11oy

Doctrine v11 LOCKED. No marketing. Every number resolves to a CI log, a Lean proof, or a Zenodo DOI.

Governance policy model card for a11oy v19 — the governed execution fabric organ. Policy weights are DSSE-signed at training time and verified against the Lean kernel at lutar-lean@c7c0ba17. 9 packages, 248 unit assertions.

The model encodes the 44-formula anchor gate set as hard policy constraints. No agentic action passes without clearing all 44 anchor formula gates. RAE-1 protocol (a11oy#122) defines the authorization handshake sequence.

Live receipts: a11oy Space. DOI: 10.5281/zenodo.20431181.

Quickstart — consume this card

Honest scope: this repo is a docs / spec / proof bundle, not a Hugging Face Kernel Hub kernel. It ships no build.toml and no build/torch-universal/… package, so kernels.get_kernel("SZLHOLDINGS/a11oy-v19-substrate") does not apply here (it would fail). Consume the artifacts it does ship with huggingface_hub, and load the runtime governed kernels that enforce this policy from szl-kernels.

1) Fetch this card's artifacts (docs, DSSE-signed deploy manifests, proofs, eval trace):

pip install huggingface_hub

from huggingface_hub import snapshot_download, hf_hub_download

# Whole bundle (docs + payloads/deploy manifests + proofs + eval trace):
path = snapshot_download("SZLHOLDINGS/a11oy-v19-substrate")

# …or a single artifact — e.g. the sample eval trace and the metadata:
trace = hf_hub_download("SZLHOLDINGS/a11oy-v19-substrate", "EVAL_TRACE_SAMPLE.jsonl")
meta  = hf_hub_download("SZLHOLDINGS/a11oy-v19-substrate", "a11oy-metadata.json")

Output (not executed here): local filesystem paths to the cached snapshot / files. There is no weights/config artifact to from_pretrained — this card publishes documentation, signed deploy manifests, Lean-proof pointers, and a sample eval trace, not model weights.

2) Load the runtime kernels that enforce this policy (the loadable half of the estate):

pip install kernels

from kernels import get_kernel

# The loadable governed kernels live in the szl-kernels suite (universal, pure-Python):
suite = get_kernel("SZLHOLDINGS/szl-kernels", revision="main", trust_remote_code=True)

print(suite.selfcheck())   # one-shot CPU health probe for the runtime suite

For live governed inference, use the a11oy Space (this card is the policy/spec; the Space is the running organ).

State (live 2026-06-28)

Metric	Value	Verify
Lean declarations	749	lutar-lean@c7c0ba17
Lean axioms	15 (14 unique)	A1–A18 honest gap
Lean sorries	112 baseline + 51 Putnam = 163 total	lutar-lean@c7c0ba17
Locked proven	8 {F1, F4, F7, F11, F12, F18, F19, F22}	lutar-lean@c7c0ba17
Anchor formulas	44 specified	a11oy#114
Kernel green	Mathlib 4.13.0 d7317655	PR #106
HF Spaces	11	SZLHOLDINGS org
HF Datasets	27 (19 public + 8 private)	SZLHOLDINGS org
HF Models	8	SZLHOLDINGS org
Zenodo DOIs	6 release + 1 concept alias	10.5281/zenodo.20434276
RAE-1 protocol	merged	a11oy#122
Putnam honest	10/12	agi-forecast

Cross-references

• Thesis: Ouroboros Thesis v18 · DOI 10.5281/zenodo.20434276
• Lean companion: lutar-lean · DOI 10.5281/zenodo.20424992
• Receipts: MCP server · szlholdings-hatun-mcp.hf.space
• Test results: SZLHOLDINGS/test-results
• Catalog: SZLHOLDINGS on HuggingFace
• Source: szl-holdings/a11oy on GitHub

Provenance

Field	Value
Ecosystem stage	operational
Ecosystem stage matrix	SZLHOLDINGS org
MCP gateway	szlholdings-hatun-mcp.hf.space
Doctrine	v11 LOCKED (749/14/163 @ c7c0ba17) — no marketing language, every number resolves to a CI log or Zenodo DOI
Thesis DOI	10.5281/zenodo.20434276
Lean companion DOI	10.5281/zenodo.20424992
Author	Stephen Paul Lutar Jr. · ORCID 0009-0001-0110-4173

SZL Kernels Suite

This policy card sits alongside the szl-kernels governed-kernel suite (the loadable kernels that enforce the policy at runtime):

Repo	Lane
szl-kernels	hub — unified suite, cross-kernel UnifiedReceiptChain
szl-governed-norm	RMSNorm/LayerNorm + SHA3-256 receipts
szl-lambda-gate	advisory Λ gate (Conjecture 1, OPEN)
governed-inference-meter	MEASURED-joule energy accounting (NVML)
szl-govsign	signed governance attestation (DSSE / in-toto)
szl-blocked	honest-BLOCKED state + EU AI Act Annex IV DRAFT
szl-provctl	provenance-DAG verify + in-toto/SLSA interop

Live Spaces: a11oy · hatun-mcp.

Related — Governed Kernels collection: Governed Kernels — verifiable AI building blocks groups the whole family in one page. This card is a docs/showcase bundle (governance policy, proofs, eval trace) — not a loadable weights model. Live console: a11oy · a-11-oy.com · llm-router · receipt verifier · receipt spec (hub).

---

SZL Holdings · 11 Spaces / 27 datasets (19 public) / 8 models · Lean 749/14/163 @ c7c0ba17 · HF org · Doctrine v11 LOCKED
Signed-off-by: Stephen Lutar stephenlutar2@gmail.com

---

Citation

Part of the SZL Holdings Ouroboros Thesis — concept DOI 10.5281/zenodo.19944926 (Stephen P. Lutar, Jr., ORCID 0009-0001-0110-4173). Doctrine v11 LOCKED; Λ = Conjecture 1.

Signed-off-by: Stephen Lutar stephenlutar2@gmail.com