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