Proof Methodology
Three axioms used across the proof corpus: Core-SVP hardness assumption, Ring-LWE to SVP reduction, and BKZ cost model. All other results are proven from first principles.
Coq Proofs
14 machine-checked proofs compiled with Coq 8.18+. Zero admitted statements.
| Proof | Property Verified |
|---|---|
| KElimination | Exact overflow recovery in RNS division |
| GSOFHE | Depth management correctness for encrypted circuits |
| CRTShadowEntropy | Shadow entropy statistical independence from computation inputs |
| OrderFinding | Multiplicative order detection in modular groups |
| MQReLU | Integer activation function preserves FHE noise bounds |
| IntegerSoftmax | Exact integer softmax summation correctness |
| MontgomeryPersistent | Montgomery form persistence across chained operations |
| MobiusInt | Mobius function integer arithmetic roundtrip |
| CyclotomicPhase | Cyclotomic polynomial phase evaluation correctness |
| PadeEngine | Pade approximant identity and zero properties |
| ExactCoefficient | Exact polynomial coefficient extraction |
| StateCompression | Compressed state preserves computation integrity |
| SideChannelResistance | Constant-time operation execution verification |
| EncryptedQuantum | Quantum operation simulation in encrypted domain |
Lean4 Core Proofs
Core formal proofs built on Lean 4 with Mathlib. Zero sorry statements.
| Proof | Property Verified |
|---|---|
| Basic | Core algebraic definitions and axioms |
| ShadowEntropy | NIST SP 800-22 statistical test compliance |
| ZMod | Modular arithmetic foundations and inverses |
| AHOP/Algebra | Post-quantum algebraic structure properties |
| AHOP/Hardness | Hardness assumption formalization |
| AHOP/Parameters | Parameter instantiation at 128-bit security |
| Lattice/CRT | Chinese Remainder Theorem over lattice structures |
| Montgomery | Montgomery multiplication correctness |
| GSOFHE | Encrypted circuit depth bound proofs |
| MQReLU | Integer ReLU noise bound preservation |
| IntegerSoftmax | Integer softmax summation exactness |
| OrderFinding | Modular order detection correctness |
| PadeEngine | Rational approximation identities |
| MobiusInt | Integer Mobius function properties |
| CyclotomicPhase | Phase polynomial evaluation |
| ExactCoefficient | Coefficient extraction exactness |
| SideChannel | Timing-independent operation proofs |
| EncryptedQuantum | Encrypted quantum gate simulation |
| StateCompression | State compression integrity |
Innovation Proofs
24 additional Lean4 proofs cover per-innovation mathematical correctness across the full innovation stack, including persistent Montgomery arithmetic, integer neural networks, binary GCD, PLMG rails, GSO depth management, MANA acceleration, Clockwork Prime, bootstrap-free FHE, and real-time FHE operations.
NIST Compliance
14 dedicated proof files cover NIST compliance: AHOP security reductions, IND-CPA game formalization, ring definitions, homomorphic security, K-Elimination soundness, security lemmas, and the complete security argument.
Verification Summary
Coq
Verified
- 14 proofs
- 0 admitted statements
- Coq 8.18+
Lean4
Verified
- 55+ proof files
- 0 sorry statements
- Lean 4.x + Mathlib
Axioms
3 Used
- Core-SVP hardness assumption
- Ring-LWE to SVP reduction
- BKZ cost model
External Audit
Pending
- Third-party review in progress
- Results will be published upon completion