Epiplexity Program
The Central Question
How complex does a distribution look to a computationally bounded observer? Epiplexity answers this by decomposing the observer's optimal description into structure (code length S_T) and noise (cross-entropy H_T). A CSPRNG output has maximum epiplexity — no efficient observer can distinguish it from uniform, so all its information looks like noise. Conversely, one-way permutations create asymmetric complexity: easy to compute forward, hard to invert.
Original Researchers
Scientific Context
Classical Kolmogorov complexity measures the shortest program that produces a given string — but is uncomputable. Epiplexity introduces a time bound T, restricting to programs that run in at most T steps. This makes the measure computable (though potentially intractable) and connects it to cryptographic hardness assumptions.
The MDL decomposition: For any T-bounded program P describing distribution X, the total cost is MDL_T(X) = S_T(X) + H_T(X). The optimal program minimizes this total cost, with ties broken by code length. S_T measures extractable structure; H_T measures residual noise.
What formalization provides: Every theorem in the paper — nonnegativity bounds, CSPRNG security reduction, OWP factorization hardness — is machine-checked. The formalization also extends to emergence detection: a sharp drop in epiplexity signals that new structure has become computationally accessible.
Project Phases
Complete formalization across 23 modules: MDL cost, optimal programs, epiplexity S_T, time-bounded entropy H_T, nonnegativity bounds, CSPRNG security reduction, OWP factorization hardness, and emergence detection.
- ▸MDLT_eq_mdlCost: MDL_T = S_T + H_T
- ▸ST_nonneg, HT_nonneg: nonnegativity bounds
- ▸csprng_high_epiplexity: CSPRNG → high S_T
- ▸owp_factorization_hardness: OWP → asymmetric S_T
Faithful translation to verified C (gcc -Wall -Wextra -Werror: 0 warnings) and safe Rust (cargo test: 4/4 pass). Prog struct, MDL cost, and security property checks faithfully translated.
- ▸gcc -std=c11 -Wall -Wextra -Werror: PASS
- ▸cargo build: 0 warnings
- ▸cargo test: 4/4 pass
- ▸Prog struct matches Lean OptimalProg specification
All artifacts content-addressed and pinned to IPFS. Lean proofs, verified C, safe Rust archives with CIDv1 identifiers.
- ▸Lean archive: 6 key source files (20.9KB)
- ▸C archive: 1 translation unit (1.1KB)
- ▸Rust archive: 1 source file + Cargo.toml (1KB)
- ▸SHA-256 content hashes for all archives
Resources
MENTAT Contribution Certificates
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerEpiplexity: Time-Bounded Complexity via MDL Decomposition
Contributor
Jonathan Finzi, Chris Olah, Neel Nanda
Anthropic / Google DeepMind
Core conceptual insight: the complexity of a distribution can be decomposed into structure (code length S_T) and noise (cross-entropy H_T) under a time bound T. Epiplexity S_T(X) measures how much structure a T-bounded observer can extract — high epiplexity means the distribution looks random to any efficient observer. This connects information theory, cryptography, and computational complexity.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerFull MDL Framework: Programs, Distributions, Security Reductions
Contributor
Jonathan Finzi, Chris Olah, Neel Nanda
Anthropic / Google DeepMind
Full mathematical framework: (1) Programs with code length and distribution output, (2) Feasibility under time bound T, (3) MDL cost as code length + cross-entropy, (4) Optimal programs with tie-breaking by code length, (5) CSPRNG security reduction — computationally indistinguishable from uniform implies high epiplexity, (6) OWP factorization — one-way permutations create asymmetric epiplexity.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Lean 4 Formalization — 23 Modules, 80+ Theorems, 0 Sorry
Contributor
Apoth3osis Labs
R&D Division
Machine-checked Lean 4 formalization of the Epiplexity framework. 23 modules covering MDL cost, optimal programs, epiplexity S_T, time-bounded entropy H_T, nonnegativity bounds, CSPRNG security reduction, OWP factorization hardness, and emergence detection. All theorems proved without sorry/admit.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
Epiplexity Verified Kernel — C & Rust Transpilation
Contributor
Apoth3osis Labs
R&D Division
Verified C and safe Rust transpilations of the core Epiplexity modules. C: gcc -std=c11 -Wall -Wextra -Werror, 0 warnings. Rust: cargo build 0 warnings, cargo test 4/4 pass. Prog struct, mdl_cost, epiplexity_st, csprng_implies_high_epiplexity, and owp_factorization_hardness faithfully translated.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026