SZLHOLDINGS/a11oy-verifiable-corpus

<!-- SZL-ESTATE-CARD:v2:START --> <p align="center"><a href="https://a-11-oy.com/"><img src="https://huggingface.co/spaces/SZLHOLDINGS/README/resolve/main/assets/estate-banner-v2.svg" alt="SZL Holdings — governed, receipted, verifiable" width="100%"></a></p> <p align="center"> <a href="https://github.com/szl-holdings/.github/tree/main/doctrine"><img src="https://img.shields.io/badge/doctrine-v11%20LOCKED-0B1F3A?style=flat-square" alt="doctrine v11"></a> <a href="https://a-11-oy.com/"><img src="https://img.shields.io/badge/evidence%20wall-LIVE%20%C2%B7%20verify%20in%20browser-3AF4C8?style=flat-square" alt="live evidence wall"></a> <a href="https://huggingface.co/datasets/SZLHOLDINGS/szl-lake"><img src="https://img.shields.io/badge/szl--lake-offline%20verifiable-C9B787?style=flat-square" alt="szl-lake offline verifiable"></a> <a href="https://huggingface.co/spaces/SZLHOLDINGS/holographic"><img src="https://img.shields.io/badge/estate%20map-holographic-5B8DEE?style=flat-square" alt="holographic estate map"></a> </p> <p align="center">_{Part of the <a href="https://huggingface.co/SZLHOLDINGS">SZL Holdings</a> governed estate — claims are designed to carry checkable receipts. Verification proves integrity &amp; origin, never accuracy or performance.}</p> <!-- SZL-ESTATE-CARD:v2:END -->

<div align="center"> <p>

  

</p> </div>

a11oy — Verifiable Corpus · verify it yourself

This dataset publishes a11oy's signed receipts and proof surface so that anyone can independently verify them — no trust in SZL Holdings required. Every receipt here carries the full cryptographic material needed to check its signature offline; every proof claim is copied verbatim from its kernel-checked source.

It is produced by the append-only, content-addressed `szl_hf_bucket` client and published by szl_corpus_publish.py. Records are append-only and idempotent: re-publishing the same logical record dedups to a single stored entry; a genuine change lands as a new record, so the history is preserved.

Honesty first. This corpus deliberately does not overstate anything. See Honesty & scope before drawing conclusions.

Layout

receipts/<YYYY-MM-DD>.ndjson   receipts/head.json     # signed DSSE receipts + verification data
theorems/<YYYY-MM-DD>.ndjson   theorems/head.json     # kernel-verified theorem list (verbatim)
formulas/<YYYY-MM-DD>.ndjson   formulas/head.json     # formula registry + proof_status (verbatim)
lake/<YYYY-MM-DD>.ndjson       lake/head.json         # archival lake receipt records

Each *.ndjson is one JSON record per line. Each line is a bucket envelope:

{ "schema": "szl.hf.bucket.record/v1", "id": "<sha256>", "ts": "...",
  "source": "a11oy", "kind": "receipt|theorem|formula", "payload": { ... } }

The id is content-addressed over {source, kind, content} — not the timestamp — which is what makes re-publishing idempotent. head.json is the chain-state (count / last id / shards). The asset record lives under payload (payload.schema == "szl.a11oy.corpus.record/v1").

Load it

Four configs are declared: receipts, theorems, formulas, and lake:

from datasets import load_dataset

# signed DSSE receipts (default working config)
receipts = load_dataset("SZLHOLDINGS/a11oy-verifiable-corpus", "receipts", split="train")
print(receipts[0])

# the other three configs
theorems = load_dataset("SZLHOLDINGS/a11oy-verifiable-corpus", "theorems", split="train")
formulas = load_dataset("SZLHOLDINGS/a11oy-verifiable-corpus", "formulas", split="train")
lake = load_dataset("SZLHOLDINGS/a11oy-verifiable-corpus", "lake", split="train")

Every raw NDJSON row is the szl.hf.bucket.record/v1 envelope above. Because the archival lake stream contains heterogeneous payload schemas, its config exposes payload as JSON text; use json.loads(row["payload"]). Verify content-addressed IDs against the raw NDJSON. Lake rows can be signed, honestly unsigned, or non-DSSE, so inclusion is not proof of cryptographic verification.

The verify-it-yourself snippets below apply to records in the receipts config.

1 · Receipts (receipts/)

payload.asset == "receipt". Two signature schemes appear, both real — the publisher never emits an unsigned or placeholder envelope:

payload.envelope is the complete DSSE envelope. payload.verify tells you exactly how to check it. payload.receipt_uid is the stable sha256 of the signed content (the PAE), independent of the publish time.

Verify an ecdsa-p256-dsse-pae receipt yourself

The signature is a DER-encoded ECDSA-P256 signature over the DSSE PAE:

PAE = b"DSSEv1 " + len(payloadType) + b" " + payloadType + b" " + len(payload) + b" " + payload

where payload is the base64-decoded envelope.payload. Verify against the published public key `szl-holdings/.github/cosign.pub`:

import base64, json, urllib.request
from cryptography.hazmat.primitives import hashes, serialization
from cryptography.hazmat.primitives.asymmetric import ec

# 1. take any receipt line from the dataset
line = open("receipts/2026-06-12.ndjson").readline()       # pick any shard
env  = json.loads(line)["payload"]["envelope"]

# 2. fetch the published public key (or paste the PEM below)
pub_pem = urllib.request.urlopen(
    "https://raw.githubusercontent.com/szl-holdings/.github/main/cosign.pub").read()
pub = serialization.load_pem_public_key(pub_pem)

# 3. reconstruct the DSSE PAE
pt   = env["payloadType"].encode()
body = base64.b64decode(env["payload"])
pae  = b"DSSEv1 " + str(len(pt)).encode() + b" " + pt + b" " + str(len(body)).encode() + b" " + body

# 4. verify every signature (raises cryptography.exceptions.InvalidSignature on tamper)
for s in env["signatures"]:
    pub.verify(base64.b64decode(s["sig"]), pae, ec.ECDSA(hashes.SHA256()))
    print("OK", s.get("keyid"))            # -> OK szlholdings-cosign

The same public key, for convenience (verify it matches the URL above):

-----BEGIN PUBLIC KEY-----
MFkwEwYHKoZIzj0CAQYIKoZIzj0DAQcDQgAE/Jlv9FnwJ13l4QIZpr4IbTBUtVZ2
i+O7Jai/s7xsdXvOjmZGYhd36VxNQQahTSjWoYpPrSNhXbt/n7lsgi61xA==
-----END PUBLIC KEY-----

A change to any byte of payload or payloadType changes the PAE and the verification fails — that is the point.

Verify a sigstore-keyless-dsse receipt yourself

These envelopes are self-contained: envelope._sigstore.bundle carries the full Sigstore bundle (Fulcio cert chain + Rekor inclusion proof). Verify with `cosign`:

# extract the bundle and the DSSE statement, then:
cosign verify-blob-attestation --bundle bundle.json --new-bundle-format \
  --certificate-identity-regexp 'github.com/szl-holdings/.*' \
  --certificate-oidc-issuer https://token.actions.githubusercontent.com statement.json

You can also look the entry up directly in the public Rekor transparency log.

2 · Theorems (theorems/)

payload.asset == "theorem". The kernel-verified theorem list, embedded verbatim from lutar-lean `VERIFIED_THEOREMS.md`:

• —payload.markdown — the file, byte-for-byte.
• —payload.content_sha256 — sha256 of the fetched bytes (cross-check against the source).
• —payload.summary — counts and the honesty markers the source itself asserts (no re-derivation).
• —payload.source_url — where it came from.

That file is auto-generated from a real `lake build`: every entry is a Lean theorem/lemma the kernel checks with zero `sorry`, with an axiom footprint inside {propext, Classical.choice, Quot.sound} plus the declared, cited repo axioms. To verify, clone lutar-lean and run the build yourself — or just confirm the embedded sha256 matches the live source.

3 · Formulas (formulas/)

payload.asset == "formula", one record per formula in a11oy's canonical registry (szl_formulas.py):

• —payload.name / payload.callable — the formula and its runtime function.
• —payload.proof_status — copied verbatim from the registry's PROOF_STATUS.

proof_status reflects the Lean kernel + Doctrine v11 honesty surface (PROVEN, AXIOM-gated, SORRY, REAL, CONJECTURE), not a marketing claim. Cross-check any PROVEN claim against the theorem list above and the lutar-lean source.

Honesty & scope

This corpus is governed by the same honesty doctrine (v11) as a11oy:

• —Theorem U is REAL but CONDITIONAL (proven under its stated identifiability / factor assumptions) — not unconditionally proven.
• —Conjecture 1 (unconditional Λ-uniqueness, ∀ Φ, LutarAxioms Φ → Φ = Λ k) is OPEN and machine-checked FALSE under A1–A5 (maxAgg_ne_Lambda is an explicit counterexample). It can never appear as a proven theorem.
• —The locked-proven ladder is not collapsed to "all proven": only what the kernel actually proves is labelled proven; everything else keeps its honest EXPERIMENTAL / AXIOM-gated / CONJECTURE status.

What the `receipts` config intentionally excludes: demo-grade HMAC receipts and unsigned or placeholder DSSE envelopes. The separate archival lake config can contain signed, honestly unsigned, or non-DSSE records; inspect and verify each row rather than inferring cryptographic status from inclusion.

Provenance

• —Producer: `szl-holdings/a11oy` · szl_corpus_publish.py (real-time hook on the receipt signing path + a full-sync for formulas/theorems).
• —Theorem source: `szl-holdings/lutar-lean`.
• —Public key: `szl-holdings/.github/cosign.pub`.
• —License: Apache-2.0.

Read it live — the round trip

This corpus is not write-only — the live a11oy console reads it back, proving Hugging Face is the real backing store, not a one-way mirror.

• —Browse: <https://huggingface.co/datasets/SZLHOLDINGS/a11oy-verifiable-corpus>
• —Canonical trust center: <https://a-11-oy.com> — the a11oy console, receipt verifier & formula surfaces that read this corpus back (REPORTED live surfaces; verify status yourself).
• —Console read-back: the a11oy demo and the Space surface this dataset's committed state — receipt count, chain head, and the kernel-verified theorem count — via GET /api/a11oy/v1/corpus, with honest live / cached / unreachable labels. No count is upgraded into a stronger claim: Theorem U stays CONDITIONAL and Conjecture 1 stays OPEN.
• —Re-verify offline: re-check any receipt in this corpus against the open governed-receipt-spec with the dependency-free governed-receipt-verifier — no trust in the console required. Governed model routing with honest per-response provenance: llm-router.


Citation

Cite this. Part of the SZL Holdings Ouroboros Thesis (Governed Post-Determinism). Concept DOI (always-latest): 10.5281/zenodo.19944926. Author: Stephen P. Lutar Jr. · ORCID 0009-0001-0110-4173 · Dataset license: Apache-2.0; the cited program publication is CC-BY-4.0. Full DOI-pinned lineage (v1→v26) + the 8 papers: szl-papers PAPERS_INDEX. No artifact-specific DOI is minted for this dataset; the concept DOI above covers the program.

Honesty (Doctrine v11): Λ unconditional uniqueness is Conjecture 1 (machine-checked FALSE as stated) — never a theorem; conditional uniqueness is Theorem U (axiom-free). Locked-proven formulas = exactly 8 {F1,F4,F7,F11,F12,F18,F19,F22}; ~185 experimental theorems are a separate CI-green tier; Khipu BFT safety = Conjecture 2. Trust never 100%.

@misc{lutar_szl_ouroboros,
  author    = {Lutar, Stephen P., Jr.},
  title     = {SZL Holdings --- The Ouroboros Thesis (Governed Post-Determinism)},
  year      = {2026},
  publisher = {Zenodo},
  doi       = {10.5281/zenodo.19944926},
  url       = {https://doi.org/10.5281/zenodo.19944926},
  note      = {Concept DOI --- always resolves to the latest version. ORCID 0009-0001-0110-4173. CC-BY-4.0.}
}

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

<div align="center">

[🛡️ SZLHOLDINGS on Hugging Face →](https://huggingface.co/SZLHOLDINGS) · [a-11-oy.com →](https://a-11-oy.com) · [Estate hub — live →](https://szlholdings-szl-estate-live.static.hf.space)

Governed AI you can prove.

_{SLSA: L1 honest · L2 attested · L3 roadmap. Λ = Conjecture 1 (advisory, never a theorem). Trust ceiling 0.97 — never 100%. Labels honest by default: MEASURED / REPORTED / MODELED / HEURISTIC / UNKNOWN / UNAVAILABLE. locked-proven = exactly 8 {F1,F4,F7,F11,F12,F18,F19,F22}.}

</div>