Materials (Quechua Q'allariy — "the first") is SZL's verifiable
alloy & crystal discovery surface. The field competes on accuracy; SZL competes on
verifiability — every verdict below is a real endpoint call signed into the
shared Khipu chain, re-verifiable by any judge. Three live capabilities:
a signed crystal novelty certificate (isometry-invariant PDD fingerprint, answering the GNoME
duplicate scandal), a PAC-Bayes generalization certificate, and Immune dual-use screening.
Honest labels throughout: PDD injectivity = ROADMAP; McAllester Lean proof = SORRY;
Λ = Conjecture 1; Khipu = Conjecture 2; Neyman–Pearson immune gate =
proven-backing. Locked-proven set unchanged at EXACTLY 8 @ kernel c7c0ba17;
trust is never 100%; effectors simulated; no fabricated data.
Submit a crystal (lattice a,b,c,α,β,γ in Å/degrees + fractional atom
sites). The endpoint computes an isometry-invariant Pointwise-Distance-Distribution fingerprint
(Widdowson–Kurlin PDD), compares it against an append-only registry, and signs a Khipu receipt
(SZL.Materials.NoveltyCert.v1). Prefilled with the Al-FCC example.
Fingerprint INJECTIVITY is ROADMAP / CONJECTURE — not proven.
Compute the McAllester PAC-Bayes bound "with prob ≥ 1−δ, population risk ≤ bound"
+ a signed certificate. The bound computation is exact; the
McAllester Lean proof is a tracked SORRY (proven-on-paper) —
Lutar/Materials/PACBayesMaterials.lean.
Screen a materials-inference input through the Neyman–Pearson-optimal, fail-closed Immune gate
(dual-use / safety). Returns allow / deny + signals + a signed receipt. Falls back to
/api/a11oy/v1/immune/verdict if /screen is not yet live.
Immune gate Lean backing is PROVEN (not folded into locked-8).
Claiming more than is real is the only unacceptable outcome. Each capability is labeled with its
exact Lean reference. The locked machine-checked proven set is EXACTLY 8
{F1,F4,F7,F11,F12,F18,F19,F22} at kernel c7c0ba17 — none of the materials capabilities are
folded into it.
| Capability | Status | Lean reference | Live endpoint |
|---|---|---|---|
| Crystal novelty fingerprint + signed Khipu receipt (computation + chain) | PROVEN by construction | Lutar/Wave8/HashChain.lean |
/materials/novelty |
| PDD fingerprint injectivity (distinct crystals ⇒ distinct PDD) | ROADMAP | Lutar/Materials/PDDInjective.lean (sorry) |
/materials/novelty |
| PAC-Bayes (McAllester) bound — computation | EXACT / PROVEN-on-paper | szl_formulas.pac_bayes_mcallester |
/materials/certify |
| McAllester bound — Lean proof (materials specialization) | ROADMAP (SORRY) | Lutar/Materials/PACBayesMaterials.lean (sorry) |
/materials/certify |
| Λ-aggregator uniqueness (geometric mean is unique) | CONJECTURE 1 | Lutar/Uniqueness.lean:215 (sorry) |
aggregated trust label |
| Khipu receipt ordering + energy-measurement methodology | CONJECTURE 2 | Lutar/Khipu/SummationInvariant.lean |
all /materials/* receipts |
| Neyman–Pearson-optimal, fail-closed Immune egress gate | PROVEN-backing | Lutar/Wave11/ImmuneNeymanPearsonOpt.lean |
/materials/screen → /immune/verdict |
| Receipt cryptographic signature | DSSE_PLACEHOLDER | Sigstore not wired into CI (chain integrity is real) | all receipts |
sorry) @ c7c0ba17 or peer-reviewed ·
CONJECTURE = formally stated, not yet machine-checked ·
ROADMAP = scaffolded statement with an explicit tracked sorry.
The two new Lutar/Materials/*.lean files are NOT imported by Lutar.lean (not in lake build) and are NOT in the locked-8.
Trust is never 100%.