BoundedAKS.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ExactQuantumFactoring.BitArithmetic.aks_constants_fit line 19
Source documentation
All static search parameters and constants fit polynomial-width words.
```
lemma aks_constants_fit {n : ℕ} (hn : 128 ≤ n) : 8*n^8 < 2^(rootWidth n) := by
…
```
Mentions: OAI.ExactQuantumFactoring.BitArithmetic.rootWidth
def OAI.ExactQuantumFactoring.BitArithmetic.allCongruences line 28
lemma OAI.ExactQuantumFactoring.BitArithmetic.allCongruences_value line 31
lemma OAI.ExactQuantumFactoring.BitArithmetic.allCongruences_count line 47
def OAI.ExactQuantumFactoring.BitArithmetic.aksBranch line 58
Source documentation
The auxiliary modulus branch. The bounded small-divisor test is performed before the congruences. Evaluating every modulus is a polynomial unrolling of (the first qualifying modulus in) the manuscript's bounded search.
```
def aksBranch (n s : ℕ) [NeZero s] : BooleanNetwork (rootWidth n) 1 :=
…
```
Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.BitArithmetic.rootWidth
lemma OAI.ExactQuantumFactoring.BitArithmetic.aksBranch_sound line 63
lemma OAI.ExactQuantumFactoring.BitArithmetic.aksBranch_complete line 86
def OAI.ExactQuantumFactoring.BitArithmetic.aksStaticBranch line 112
Source documentation
The condition is on the compile-time parameter s≤n^8, not on the possibly exponentially large input integer. Decidable primality here is a finite bounded search; its generation-cost proof is separate from circuit size.
```
def aksStaticBranch (n s : ℕ) : BooleanNetwork (rootWidth n) 1 :=
…
```
Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.BitArithmetic.rootWidth
def OAI.ExactQuantumFactoring.BitArithmetic.primalityNet line 118
theorem OAI.ExactQuantumFactoring.BitArithmetic.primalityNet_correct line 123
Source documentation
Full exact bounded AKS primality circuit, not an assumed decision procedure.
```
theorem primalityNet_correct {n : ℕ} (hn : 128 ≤ n) (x : Basis (rootWidth n))
    (hm : 2 ≤ (bitsValue x).toNat) (hmb : (bitsValue x).toNat < 2^n) :
    (primalityNet n).eval x 0=true ↔ (bitsValue x).toNat.Prime := by
…
```
Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.BitArithmetic.rootWidth, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.BitArithmetic.primalityNet