RetrospectiveSlots.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.residueUsable line 18
Source documentation
The usable-slot test is just range plus Euclidean gcd, not an order oracle.
```
def residueUsable (a m : ℕ) : Prop := a < m ∧ a.Coprime m
```
lemma OAI.ExactQuantumFactoring.residueUsable_iff line 19
def OAI.ExactQuantumFactoring.dataOrderPassed line 25
Source documentation
Test the same completed order slot using the later supplied node record. Unusable list entries (including out-of-range words) use the source dummy test.
```
noncomputable def dataOrderPassed {n : ℕ} (data : FactorData) (a m : Basis n)
    (r : OrderSlots.Result n) : Prop := by
…
```
Mentions: OAI.ExactQuantumFactoring.FactorData, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.OrderSlots.Result
lemma OAI.ExactQuantumFactoring.dataOrderPassed_correct line 37
def OAI.ExactQuantumFactoring.dataSplitPassed line 55
lemma OAI.ExactQuantumFactoring.dataSplitPassed_correct line 65
Source documentation
All list/order/retention decisions are on the actual retained raw block. The record may be that of any actual node whose label is divisible by m.
```
lemma dataSplitPassed_correct {M n : ℕ} (hM : 0<M) (m : Basis n)
    (hm : 2 ≤ (bitsValue m).toNat) (hd : (bitsValue m).toNat∣M) (hn : 0<n)
    (r : UniversalSplit.Raw n) :
    dataSplitPassed (trueData M) m hn r ↔ UniversalSplit.passed m r := by
…
```
Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.UniversalSplit.Raw, OAI.ExactQuantumFactoring.dataSplitPassed, OAI.ExactQuantumFactoring.trueData, OAI.ExactQuantumFactoring.UniversalSplit.passed