Constructor-Theoretic Cryptography

Machine-checked Lean 4 formalization of Deutsch & Marletto's Constructor Theory applied to quantum cryptographic security. No-cloning implies eavesdropping impossibility. CHSH inequality, Tsirelson bound, BB84/E91 protocol security, composable QKD, quantum error correction. 92 modules, 3,200+ theorems, zero sorry.

Lean 4 Modules

3,200+

Theorems

Sorry Count

kernel only

Axioms

BB84, E91

Key Protocols

Fully Proven

CHSH Status

C Files

13/13

Rust Tests

✓

KERNEL-CHECKED92 modules · 3,200+ theorems · 0 sorry · kernel-only axioms · gcc -Werror 0 warnings · cargo test 13/13

Key Mathematics

CHSH Inequality — Local Hidden Variable Bound

\text{CHSH inequality:} \quad |S| = |E(a_0, b_0) + E(a_0, b_1) + E(a_1, b_0) - E(a_1, b_1)| \leq 2

Lean: chsh_inequality · Proved via triangle inequality over LHV averages

Tsirelson Bound — Quantum Limit

\text{Tsirelson bound:} \quad |S|_{\text{quantum}} \leq 2\sqrt{2} \approx 2.828

Lean: tsirelson_bound · Via parallelogram law + Cauchy-Schwarz

Security Theorem — No-Cloning → Eavesdropping Impossibility

\forall E.\; (\text{possible}(E.\text{intercept}) \Rightarrow \text{possible}(\text{copy}_{XY})) \Rightarrow \text{impossible}(E.\text{intercept})

Lean: superinfo_secure_against_eavesdropping · Core CT security pattern

Superinformation Medium — The No-Cloning Condition

X \text{ clonable} \;\wedge\; Y \text{ clonable} \;\wedge\; X \otimes Y \text{ NOT clonable}

Lean: bb84Superinfo, e91Superinfo · The foundation of CT cryptographic security

Paper ↔ Proof Correspondence

Paper Claim	Lean Theorem	Status
No-cloning implies eavesdropping impossibility	superinfo_secure_against_eavesdropping	✓
CHSH inequality: \|S\| ≤ 2 for any LHV model	chsh_inequality	✓
Tsirelson bound: \|S\| ≤ 2√2 for quantum correlations	tsirelson_bound	✓
BB84 is secure against eavesdropping	bb84_secure	✓
E91 is secure against eavesdropping	e91_secure	✓
Intercept-resend is CT-impossible	intercept_resend_impossible	✓
Security composes under UC framework	uc_composition	✓
Repetition code corrects single X-errors	repetitionCode3_corrects_single_X	✓

Proof Blueprint (Key Modules)

CHSH Inequality — |S| ≤ 2 for Local Hidden VariablesE91.DI.CHSH.CHSHInequality

theorem chsh_inequality :
    |chshQuantity (M.toCorrelator)| ≤ (2 : ℝ) := by
  classical
  -- Expand S as an average of deterministic values.
  have hS :
      chshQuantity (M.toCorrelator) =
        Finset.univ.sum (fun l => M.pmf l * M.detCHSH l) := by ...
  -- Triangle inequality + |detCHSH| ≤ 2 closes the proof.
  rw [hS]
  exact abs_sum_le_sum_abs_pmf M

Tsirelson Bound — |S| ≤ 2√2 for Quantum StrategiesE91.DI.Tsirelson.TsirelsonBound

theorem tsirelson_bound :
    |chshQuantity S.toCorrelator| <= 2 * Real.sqrt 2 := by
  have hrewrite := S.chsh_rewrite
  calc
    |chshQuantity S.toCorrelator|
        = |inner ℝ S.a0 (S.b0 + S.b1) + inner ℝ S.a1 (S.b0 - S.b1)| := ...
    _ ≤ ‖S.a0‖ * ‖S.b0 + S.b1‖ + ‖S.a1‖ * ‖S.b0 - S.b1‖ := ...
    _ ≤ 2 * Real.sqrt 2 := ... -- via parallelogram law

BB84 Security — Eavesdropping is CT-ImpossibleQKD.BB84.Security

theorem bb84_secure :
    SecureAgainstEavesdropping BB84Substrate bb84TaskCT bb84Superinfo :=
  superinfo_secure_against_eavesdropping bb84TaskCT bb84Superinfo

theorem intercept_resend_impossible :
    bb84TaskCT.impossible interceptResendStrategy.intercept := by
  have hsec := bb84_secure
  refine hsec interceptResendStrategy ?_
  intro hPossible
  simpa [bb84Superinfo] using (intercept_resend_requires_copyAll hPossible)

Core Security Theorem — No-Cloning → SecurityConstructiveHardness.Security

theorem superinfo_secure_against_eavesdropping
    {σ : Type u} (CT : TaskCT σ) (M : TaskCT.SuperinformationMedium σ CT) :
    SecureAgainstEavesdropping σ CT M := by
  intro E hRequiresCloning hPossible
  have hCopyPossible : CT.possible M.copyXY := hRequiresCloning hPossible
  exact M.no_copyXY hCopyPossible

View on GitHub Research Project Page

Module Dependency Graph

Showing 9 key modules of 92 total · Full graph at GitHub

Verified C Transpilation

ct_core.cCT framework: substrates, tasks, constructors

104 lines

chsh_bounds.cCHSH inequality + Tsirelson bound verification

115 lines

qkd_security.cBB84/E91 security via superinformation no-cloning

108 lines

gcc -std=c11 -Wall -Wextra -Werror: 0 warnings per unit

Safe Rust Transpilation

Cargo.tomlZero-dependency crate

6 lines

lib.rsModule re-exports

3 lines

ct_core.rsCT framework types and operations

105 lines

chsh_bounds.rsCHSH/Tsirelson bounds with 4 test cases

120 lines

qkd_security.rsBB84/E91 security proofs, 5 tests

100 lines

cargo build: 0 warnings · cargo test: 13/13 pass

Provenance Chain

Paper: Deutsch & Marletto, Constructor Theory (2013-2024)

Lean 4: 92 modules, 3,200+ theorems, kernel-only axioms

Verified C: gcc -std=c11 -Wall -Wextra -Werror: PASS

Safe Rust: cargo test 13/13, 0 warnings

GitHub: Abraxas1010/ct-crypto-lean

Download Archives

Lean Proofs (7.9KB)Verified C (3.1KB)Safe Rust (3.2KB)

Key Lean 4 Modules

Module	Theorems	Lines	Description
Constructor.CT.Core	12	120	Substrates, variables, tasks, constructors
ConstructiveHardness.Security	3	52	No-cloning → eavesdropping impossibility
QKD.BB84.Security	3	44	BB84 protocol security (CT proof)
QKD.BB84.Superinfo	6	80	BB84 as superinformation medium
QKD.E91.DI.CHSH.CHSHInequality	8	140	CHSH inequality: \|S\| ≤ 2 for LHV
QKD.E91.DI.Tsirelson.TsirelsonBound	5	95	Tsirelson bound: \|S\| ≤ 2√2 for quantum
QKD.E91.Security	2	33	E91 protocol security (CT proof)
Composable.CompositionTheorem	3	39	UC-style composable security kit
QEC.Pauli.PauliGroup	8	65	Pauli group structure for QEC
QEC.Stabilizer.StabilizerCode	4	42	Stabilizer code framework

Showing 10 of 92 modules · Full list at GitHub repository

← All PPC Projects Research Page →