Basic.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

inductive OAI.ExactQuantumFactoring.Primitive line 12
Source documentation
The five primitive gates exactly as in Section 2.
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:12 (same declaration text).
```
inductive Primitive where
…
```
def OAI.ExactQuantumFactoring.Primitive.arity line 16
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:16 (same declaration text).
def OAI.ExactQuantumFactoring.Primitive.code line 21
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:21 (same declaration text).
structure OAI.ExactQuantumFactoring.Gate line 26
Source documentation
An inverse and/or one added control. This is a fixed set of 20 gate names, not an unbounded-control or arbitrary-angle gate model.
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:26 (same declaration text).
```
structure Gate where
…
```
def OAI.ExactQuantumFactoring.Gate.arity line 32
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:32 (same declaration text).

def OAI.ExactQuantumFactoring.Primitive.matrix line 36

Source documentation

Matrix entries are indexed by lists in wire order (row first, column second). Entries on ill-sized lists are irrelevant and set to zero.

Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:36 (same declaration text).

noncomputable def Primitive.matrix : Primitive → List Bool → List Bool → ℂ
  | .not, [a], [b] => if a = !b then 1 else 0
  | .cnot, [a,b], [c,d] => if a = c ∧ b = Bool.xor c d then 1 else 0
  | .toffoli, [a,b,c], [d,e,f] =>
      if a = d ∧ b = e ∧ c = Bool.xor f (d && e) then 1 else 0
  | .hadamard, [a], [b] =>
      (if a && b then -1 else 1) / (Real.sqrt 2 : ℂ)
  | .phase, [a], [b] => if a = b then (if b then Complex.I else 1) else 0
  | _, _, _ => 0

Mentions: OAI.ExactQuantumFactoring.Primitive

def OAI.ExactQuantumFactoring.Gate.baseMatrix line 46
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:46 (same declaration text).
def OAI.ExactQuantumFactoring.Gate.matrix line 49
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:49 (same declaration text).
structure OAI.ExactQuantumFactoring.Instruction line 59
Source documentation
A primitive is placed on distinct actual wires, with no operation of unbounded arity hidden in a circuit instruction.
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:59 (same declaration text).
```
structure Instruction (q : ℕ) where
…
```
abbrev OAI.ExactQuantumFactoring.Basis line 64
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:64 (same declaration text).
abbrev OAI.ExactQuantumFactoring.State line 65
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:65 (same declaration text).
def OAI.ExactQuantumFactoring.Instruction.matrix line 67
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:67 (same declaration text).
structure OAI.ExactQuantumFactoring.Circuit line 75
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:75 (same declaration text).
def OAI.ExactQuantumFactoring.Circuit.apply line 79
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:79 (same declaration text).
def OAI.ExactQuantumFactoring.inputBasis line 83
Source documentation
Input wires are first, least significant bit first; all other wires start zero.
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:83 (same declaration text).
```
def inputBasis (q ℓ N : ℕ) : Basis q :=
…
```
Mentions: OAI.ExactQuantumFactoring.Basis
def OAI.ExactQuantumFactoring.Circuit.outputState line 86
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:86 (same declaration text).
def OAI.ExactQuantumFactoring.paddedLength line 91
Source documentation
The cutoff and padding are the standing parameters in Section 2.
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:91 (same declaration text).
```
def paddedLength (ℓ : ℕ) : ℕ := max 128 ℓ
```
def OAI.ExactQuantumFactoring.readBit line 93
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:93 (same declaration text).
def OAI.ExactQuantumFactoring.outputList line 97
Source documentation
n entries of n bits each, in the n² wires immediately after the input.
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:97 (same declaration text).
```
def outputList {q : ℕ} (ℓ : ℕ) (x : Basis q) : List ℕ :=
…
```
Mentions: OAI.ExactQuantumFactoring.Basis
def OAI.ExactQuantumFactoring.CorrectEncoding line 104
Source documentation
Complete nondecreasing prime factorization, multiplicities included, padded by zeros, as in Section 6. There is no primality oracle in the circuit.
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:104 (same declaration text).
```
def CorrectEncoding (N n : ℕ) (xs : List ℕ) : Prop :=
…
```
def OAI.ExactQuantumFactoring.Circuit.correctProbability line 110
Source documentation
Unnormalized Born sum on correct outputs; success is exactly one, not positivity, postselection, or a limiting high probability.
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:110 (same declaration text).
```
noncomputable def Circuit.correctProbability (c : Circuit) (ℓ N : ℕ) : ℝ := by
…
```
Mentions: OAI.ExactQuantumFactoring.Circuit
def OAI.ExactQuantumFactoring.natWord line 118
Source documentation
Unary natural words with delimiters make the circuit description explicit. Unary wire addresses cause at most polynomial overhead when width is polynomial.
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:118 (same declaration text).
```
def natWord (k : ℕ) : List Bool := List.replicate k true ++ [false]
```
def OAI.ExactQuantumFactoring.Instruction.encode line 120
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:120 (same declaration text).
def OAI.ExactQuantumFactoring.Circuit.encode line 124
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:124 (same declaration text).
def OAI.ExactQuantumFactoring.Uniform line 131
Source documentation
A single finite-alphabet classical generator receives only the INPUT LENGTH. All stack alphabets, states and labels are finite: no large-integer unit-cost oracle is hidden in TM2 push/branch functions.
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:131 (same declaration text).
```
def Uniform (family : ℕ → Circuit) : Prop :=
…
```
Mentions: OAI.ExactQuantumFactoring.Circuit
def OAI.ExactQuantumFactoring.PolynomialResources line 136
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:136 (same declaration text).
def OAI.ExactQuantumFactoring.MainTheorem line 143
Source documentation
Literal main endpoint: one length-uniform family, exact output for EVERY binary integer N≥2, and worst-case polynomial gates AND qubits.
Also declared: ComparatorChallenges/ExactQuantumFactoring.lean:143 (same declaration text).
```
def MainTheorem : Prop :=
…
```