BitEncoding.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.bitsValue line 13
Source documentation
Little-endian computational wires, with the same bit ordering as the manuscript and input/output interface.
```
def bitsValue : {b : ℕ} → (Fin b → Bool) → BitVec b
  | 0, _ => 0
  | b+1, x => BitVec.cons (x (Fin.last b)) (bitsValue (fun i => x i.castSucc))
```
lemma OAI.ExactQuantumFactoring.bitsValue_bit line 17
lemma OAI.ExactQuantumFactoring.bitsValue_bits line 28
def OAI.ExactQuantumFactoring.bitsEquiv line 34
lemma OAI.ExactQuantumFactoring.bitsValue_quarter line 41
Source documentation
The exact integer in the two most significant wires is the quarter-bin.
```
lemma bitsValue_quarter (b : ℕ) (x : Fin (b+2) → Bool) :
    (bitsValue x).toNat / 2^b =
      2*(x (Fin.last (b+1))).toNat + (x ((Fin.last b).castSucc)).toNat := by
…
```
Mentions: OAI.ExactQuantumFactoring.bitsValue