FactorGuess.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.guessWords line 15
Source documentation
The specified sorted, zero-padded n²-bit root encoding.
```
def guessWords (n : ℕ) (x : Basis (n*n)) : List ℕ :=
…
```
Mentions: OAI.ExactQuantumFactoring.Basis
lemma OAI.ExactQuantumFactoring.guessWords_injective line 18
lemma OAI.ExactQuantumFactoring.guessWords_surjective_bounded line 29
theorem OAI.ExactQuantumFactoring.unique_good_guess line 49
Source documentation
Existence/uniqueness is a mathematical fact about the required output, not a factoring oracle used in the circuit.
```
theorem unique_good_guess {N n : ℕ} (hN : 2≤N) (hb : N<2^n) :
    ∃! x : Basis (n*n), CorrectEncoding N n (guessWords n x) := by
…
```
Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.CorrectEncoding, OAI.ExactQuantumFactoring.guessWords
def OAI.ExactQuantumFactoring.fairState line 58
lemma OAI.ExactQuantumFactoring.fairState_mass line 60
lemma OAI.ExactQuantumFactoring.fairState_normalized line 65
theorem OAI.ExactQuantumFactoring.fair_guess_mass line 73
Source documentation
The actual fair-bit guess contributes exactly 2^(-n²), not an input-dependent success probability.
```
theorem fair_guess_mass {N n : ℕ} (hN : 2≤N) (hb : N<2^n) :
    outcomeMass (fun x => CorrectEncoding N n (guessWords n x)) (fairState (n*n))=
      (2:ℝ)⁻¹^(n*n) := by
…
```
Mentions: OAI.ExactQuantumFactoring.CorrectEncoding, OAI.ExactQuantumFactoring.guessWords, OAI.ExactQuantumFactoring.fairState
def OAI.ExactQuantumFactoring.guessVerifier line 85
Source documentation
Concrete Boolean root-verification circuit with no run-time primality or factorization oracle. The integer input is retained separately from the guess.
```
def guessVerifier (n : ℕ) : BooleanNetwork (n+n*n) 1 :=
…
```
Mentions: OAI.ExactQuantumFactoring.BooleanNetwork
lemma OAI.ExactQuantumFactoring.guessVerifier_correct line 89
lemma OAI.ExactQuantumFactoring.guessVerifier_count line 105