Three Theorems for a Quantum-Safe Identity

How the Sovereign Society Foundation Bound the LaBRADOR Lane to Lean4

Markus Maiwald, 2026

---

Cryptographic claims that cannot be machine-checked are aspirations. SKH v2 just stopped aspiring on three of them.

---

A quantum-safe DID is hard. A machine-checked one is rarer.

Decentralized identifiers are easy to draw on a whiteboard. Quantum-safe ones are harder. Quantum-safe ones whose cryptographic claims survive a hostile external reviewer are harder still. The Sovereign Key Helix – Libertaria’s hierarchical key derivation architecture for self-sovereign identity – has now bound its three LaBRADOR-style zero-knowledge proofs to machine-checked Lean4 theorems. This is not a position paper. It is a lake build that exits zero.

The three claims:

• Recovery. I own the ML-DSA-65 key behind this Persona. The user demonstrates ownership without revealing the secret. Used in the SKH passport recovery flow.
• Membership. My SoulKey is in the registered set. The user demonstrates membership in a published lattice accumulator without revealing which slot. Used for sybil-resistant gated participation.
• Derivation. This Persona was correctly derived from a valid DNAKey via Option C. The user demonstrates correct provenance without revealing the parent key or the (context, index) parameters.

Each is a single sentence in the SKH v0.2.0 specification. Each is now a single theorem in Libertaria.Identity. Each is a single statement an external reviewer can cite.

What landed

Phase C-4 of the SKH v2 proof roadmap shipped today as a single atomic commit on libertaria-proofs main. Nine theorems across three new files plus a centralized axiom layer.

Theorem	Reduction target	What it binds
recovery_proof_sound	M-SIS knowledge soundness	Verifier acceptance ⇒ extractable sk_MLDSA
recovery_proof_zk	Module-LWE	Recovery transcripts reveal nothing about the witness
recovery_proof_secure	M-SIS + Module-LWE	The composite Recovery security claim
membership_proof_sound	M-SIS	Verifier acceptance ⇒ SoulKey genuinely in the accumulator
membership_proof_zk	Module-LWE	Membership transcripts hide which slot the SoulKey occupies
membership_proof_secure	M-SIS + Module-LWE	The composite Membership security claim
derivation_proof_sound	M-SIS	Verifier acceptance ⇒ extractable (DNAKey, ctx, idx) witness
derivation_proof_zk	Composite (MLWE + M-SIS + BLAKE3 PRF) via addAdv3	Derivation transcripts hide the parent DNAKey and the derivation parameters
derivation_proof_secure	Composite	The headline arXiv v2 §5.4 claim

All under leanprover/lean4:v4.16.0 with mathlib4 v4.16.0. No sorry. No admit. No Classical.choice. The composite three-way negligibility for Derivation reuses isNegligible_add3, an existing lemma whose proof is two iterated applications of isNegligible_add – the kind of advantage-bookkeeping that gets sloppy in pen-and-paper arguments and Lean catches mechanically.

The architectural decision worth naming

The four new files do not mention the choice between Option C, Option A, or Option B as the LatticeHD Persona derivation construction. That choice lives one layer down, in the personaDerive opaque inside Types.lean. The C-4 theorems speak only about ML-DSA-65 keygen, lattice hardness, and a SoulKey accumulator – three abstractions invariant under the construction choice.

The payoff is immediate. The reference implementation persona.zig has been running Option C since April. The independent verification question of whether ePrint 2026/380 Construction~1 specifically proves Option C, Option A, or Option B is its own cryptanalytic workstream. None of that affects C-4. Whatever the answer eventually is, the three LaBRADOR theorems remain unchanged. The architecture absorbs the answer in one opaque, not in the security proofs above it.

This is what construction-agnosticism looks like when it is enforced by a type signature, not by convention.

What the Foundation has not proved

Honesty is the discipline. The proof line is bounded; reviewers must be able to see exactly where the boundary is.

• Concrete LaBRADOR reductions. Phase C-4 is axiomatic. The opaque LabradorTranscript, LabradorStatement, LabradorWitness, and LabradorRelation types describe the protocol’s structural surface only. Their concrete inductive forms arrive when the LaZer/LaBRADOR graft c lands – a separate sprint, estimated 20–40 hours, and the natural next step in the Janus advancement loop after that.
• Module-LWE and Module-SIS hardness themselves. These are open mathematics. Lean cannot prove them and the Foundation does not pretend to. The C-4 theorems are conditional: if Module-SIS is hard, Recovery is sound. The conditional is honestly displayed in every file’s Dependency Caveat.
• Concrete accumulator construction. The SoulKeyAccumulator opaque admits Merkle, polynomial-commitment, or Module-SIS vector-commitment realizations. Membership soundness reduces to Module-SIS regardless of which one ultimately ships.
• The argument that Option C is the right Persona derivation construction. That is an independent cryptanalytic question, deliberately out of scope for C-4.

Each gap is documented in the per-file Dependency Caveat. None is hidden.

The independence model

The Lean lane is not a Libertaria-runtime dependency. Libertaria nodes do not import Lean. Libertaria does not ship Lean. The aircraft does not carry the wind tunnel into battle.

The Foundation issues Proof Certificates that bind an SKH SPEC version to a specific Lean4 model. SKH evolves; certificates expire; re-certification is a Foundation deliverable. The Lean lane exists to be a recurring sovereignty service – grant-fundable, subscribable, auditable by hostile readers. Not a runtime burden, never a runtime dependency.

The toolchain is one lake build away. Sprint notes document each phase’s claims, gap statements, and trust boundaries.

Why this matters to you

If you build, audit, or argue against quantum-safe identity systems, the Foundation wants you. We need:

• Hostile readers. Read the proofs. Find the gaps. Break the model. The signed-off Dependency Caveats are an explicit invitation to attack the conditional, not the protocol.
• Lattice cryptanalysts. The reductions assume Module-LWE and Module-SIS hardness. If you can sharpen the hardness assumptions or surface a sub-exponential attack on a concrete parameterization, the SKH bound responds automatically.
• Proof engineers. Phase C-4 stages the LaBRADOR opaques for a future graft. When LaZer becomes a graft c target, the same theorems get re-derived against concrete transcripts. That is a clean, well-bounded sprint.
• DID protocol designers. The construction-agnostic framing is a transferable pattern. If your derivation hierarchy can be expressed as an opaque with structural axioms, your headline unlinkability theorem survives a construction pivot. We will publish the technique.

Closing

This is a checkpoint, not an arrival. The three LaBRADOR theorems are conditional on lattice hardness. Concrete reductions are deferred to the graft. The Construction~1 verification question is parallel cryptanalytic work, not a blocker. None of those gaps are hidden; all of them shrink one sprint at a time.

The C-series of SKH v2 proofs is now closed. Recovery, Membership, Derivation – machine-checked, single source of truth, ready for the LaBRADOR graft to make them concrete.

The lane is bound. The aircraft can fly.