Constructor-Theoretic Crypto Program
The Central Question
Can cryptographic security be derived from the laws of physics rather than from computational hardness assumptions? Constructor Theory says yes: if cloning the full quantum state is physically impossible, then eavesdropping is physically impossible — regardless of the adversary's computational power. This makes QKD security immune to algorithmic breakthroughs, including quantum computers.
Original Researchers
Scientific Context
Traditional cryptographic security relies on computational hardness: "breaking this requires solving a problem believed to be hard." Constructor Theory provides a fundamentally stronger guarantee: security from physical impossibility. The adversary doesn't just lack an efficient algorithm — the required operation violates physical law.
The core chain: Kochen-Specker contextuality → no hidden variables → physical impossibility of global sections → superinformation (X clonable, Y clonable, XY NOT clonable) → eavesdropping requires cloning XY → eavesdropping is physically impossible.
What formalization provides: Every step in this chain is machine-checked. The CHSH inequality proves no local hidden variable model can produce quantum correlations. The Tsirelson bound establishes the quantum limit. BB84 and E91 are proved secure as instantiations of the general superinformation security theorem. Composable security ensures protocols remain safe when used as subroutines.
Project Phases
Complete formalization across 92 modules: CT core framework, constructive hardness, BB84/E91 QKD protocols, CHSH/Tsirelson bounds, composable security, QEC, entropy/privacy amplification, and photoemission physics bridge.
- ▸chsh_inequality: |S| ≤ 2 for LHV models
- ▸tsirelson_bound: |S| ≤ 2√2 for quantum strategies
- ▸bb84_secure + e91_secure: eavesdropping CT-impossible
- ▸superinfo_secure_against_eavesdropping: core theorem
Faithful translation to verified C (gcc -Wall -Wextra -Werror: 0 warnings) and safe Rust (cargo test: 13/13 pass). CT core, CHSH bounds, and QKD security proofs translated.
- ▸gcc -std=c11 -Wall -Wextra -Werror: PASS
- ▸cargo build: 0 warnings
- ▸cargo test: 13/13 pass
- ▸All 16 deterministic LHV states verified bounded
All artifacts content-addressed and pinned to IPFS. Lean proofs, verified C, safe Rust archives with CIDv1 identifiers.
- ▸Lean archive: 10 key files (7.9KB)
- ▸C archive: 3 translation units (3.1KB)
- ▸Rust archive: 5 source files + Cargo.toml (3.2KB)
- ▸SHA-256 content hashes for all archives
Resources
MENTAT Contribution Certificates
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerConstructor Theory: Security from Physical Impossibility
Contributor
David Deutsch, Chiara Marletto
University of Oxford
Core conceptual insight: cryptographic security can be derived from the physical impossibility of certain transformations (no-cloning), rather than from computational hardness assumptions. Constructor Theory reformulates physics in terms of possible and impossible tasks, providing a substrate for information-theoretic security proofs that are immune to algorithmic breakthroughs.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerComplete CT Framework: Tasks, Information Variables, Composable Security
Contributor
David Deutsch, Chiara Marletto
University of Oxford
Full mathematical framework: (1) Substrate-agnostic task algebra with serial and parallel composition, (2) Information variables with pairwise-disjoint attributes, (3) Superinformation media with copy tasks and no-copy proofs, (4) Eavesdropping strategies with soundness conditions, (5) UC-style composable security via CompositionKit interface, (6) Entropy bounds and privacy amplification.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Lean 4 Formalization — 92 Modules, 3200+ Theorems, 0 Sorry
Contributor
Apoth3osis Labs
R&D Division
Machine-checked Lean 4 formalization of the complete CT cryptographic framework. 92 modules across 8 layers: CT core, constructive hardness, BB84/E91 QKD protocols, CHSH/Tsirelson bounds, composable security, quantum error correction, entropy/privacy amplification, and photoemission physics bridge. All theorems proved without sorry/admit using kernel-only axioms.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
CT Crypto Verified Kernel — C & Rust Transpilation
Contributor
Apoth3osis Labs
R&D Division
Verified C and safe Rust transpilations of the core CT cryptographic modules. C: gcc -std=c11 -Wall -Wextra -Werror, 0 warnings per translation unit. Rust: cargo build 0 warnings, cargo test 13/13 pass. CT core framework, CHSH/Tsirelson bound verification, and QKD security proofs faithfully translated.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026