DistinctProductCircuit.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.BitArithmetic.occursLater line 22
Source documentation
Equality is tested on runtime word values, not on network syntax.
```
def occursLater {k n : ℕ} (p : BooleanNetwork k n) (ps : List (BooleanNetwork k n)) :
    BooleanNetwork k 1 := any (ps.map (fun q=>(p.pair q).comp (wordEq n)))
```
Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.BitArithmetic.wordEq
lemma OAI.ExactQuantumFactoring.BitArithmetic.occursLater_value line 25
def OAI.ExactQuantumFactoring.BitArithmetic.distinctProductNet line 38
Source documentation
A quadratic comparison scan counts every runtime prime only once. No sorting primitive or mathematical finset operation is used by the circuit.
```
def distinctProductNet {k n : ℕ} (value : BooleanNetwork k n→BooleanNetwork k n) :
    List (BooleanNetwork k n)→BooleanNetwork k n
  | []=>wordConstant 1
  | p::ps=>(wordMux (occursLater p ps) (wordConstant 1) (value p)).pair
      (distinctProductNet value ps) |>.comp (mul n)
```
Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.BitArithmetic.wordConstant, OAI.ExactQuantumFactoring.BitArithmetic.wordMux, OAI.ExactQuantumFactoring.BitArithmetic.occursLater, OAI.ExactQuantumFactoring.BitArithmetic.mul
lemma OAI.ExactQuantumFactoring.BitArithmetic.distinctProductNet_value line 44
lemma OAI.ExactQuantumFactoring.BitArithmetic.occursLater_count line 62
lemma OAI.ExactQuantumFactoring.BitArithmetic.distinctProductNet_count line 75