Apoth3osis

Epiplexity

Machine-checked Lean 4 formalization of Finzi et al.'s Epiplexity framework. Time-bounded complexity via MDL decomposition: S_T(X) measures code length (structure), H_T(X) measures cross-entropy (noise). CSPRNG indistinguishability implies high epiplexity. One-way permutation implies factorization hardness. 23 modules, 0 sorry.

23
Lean 4 Modules
80+
Theorems
0
Sorry Count
S_T, H_T, MDL_T
Key Concepts
CSPRNG + OWP
Security Proofs
1
C Files
4/4
Rust Tests
3
Archives
>_VERIFICATION.SEAL
FORMALLY VERIFIED • LEAN 4 • MACHINE-CHECKED • APOTH3OSIS∀∃⊢→∧∨¬≡QED80 theorems • 0 sorry23 modules0 SORRY

Formal Verification Certificate

Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.

80 THEOREMS VERIFIED23 MODULES0 SORRY

Epiplexity • Lean 4 + Mathlib • Apoth3osis Labs

✓KERNEL-CHECKED23 modules · 80+ theorems · 0 sorry

Key Mathematics

MDL Decomposition

MDLT(X)=ST(X)+HT(X)ST=code length,HT=cross-entropy\text{MDL}_T(X) = S_T(X) + H_T(X) \qquad S_T = \text{code length}, \quad H_T = \text{cross-entropy}

Lean: OptimalProg.MDLT, MDLT_eq_mdlCost

CSPRNG → High Epiplexity

CSPRNG(X)  ⟹  ST(X)≥threshold(indistinguishable  ⟹  incompressible)\text{CSPRNG}(X) \implies S_T(X) \geq \text{threshold} \qquad \text{(indistinguishable} \implies \text{incompressible)}

Lean: csprng_high_epiplexity via PRFHighEpiplexity

OWP Factorization Hardness

OWP(f)  ⟹  ST(f−1(X))>ST(f(X))(inversion harder than forward)\text{OWP}(f) \implies S_T(f^{-1}(X)) > S_T(f(X)) \qquad \text{(inversion harder than forward)}

Lean: owp_factorization_hardness

Paper ↔ Proof Correspondence

ClaimTheoremStatus
MDL decomposition: MDL_T = S_T + H_TMDLT_eq_mdlCost✓
Epiplexity is nonnegST_nonneg✓
Cross-entropy is nonnegHT_nonneg✓
CSPRNG implies high epiplexitycsprng_high_epiplexity✓
OWP implies factorization hardnessowp_factorization_hardness✓
Optimal program is MDL-minimalOptimalProg.optimal✓
View on GitHubLean ProofsVerified CSafe Rust
← All PPC ProjectsResearch Page →