RetrospectiveResidues.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.recordFirst line 21
Source documentation
The distinguished component is selected from the supplied record, not by factoring the requested integer a second time.
```
def recordFirst (f : FactorRecord) : ℕ :=
…
```
Mentions: OAI.ExactQuantumFactoring.FactorRecord
lemma OAI.ExactQuantumFactoring.recordFirst_factorization line 24
lemma OAI.ExactQuantumFactoring.component_two_le line 35
lemma OAI.ExactQuantumFactoring.equivPi_natCast line 39
lemma OAI.ExactQuantumFactoring.unitCRT_natCast line 43
def OAI.ExactQuantumFactoring.dataResidueGood line 49
lemma OAI.ExactQuantumFactoring.data_component_order line 56
lemma OAI.ExactQuantumFactoring.dataResidueGood_correct line 66
Source documentation
The retrospective favorable test is a scan of supplied prime-power factors and prime-stripping computations. It agrees with the CRT event on every actual requested cofactor, including those below a node of the auxiliary tree.
```
lemma dataResidueGood_correct {M m n a : ℕ} (hM : 0<M) (hm : 2 ≤ m) (hb : m < 2^n)
    (hd : m∣M) (u : (ZMod m)ˣ) (ha : a=(u : ZMod m).val) :
    dataResidueGood (trueData M) a m ↔
      FavorableUnit (by omega) hb (UniversalSplit.firstComponent hm) u := by
…
```
Mentions: OAI.ExactQuantumFactoring.dataResidueGood, OAI.ExactQuantumFactoring.trueData, OAI.ExactQuantumFactoring.FavorableUnit, OAI.ExactQuantumFactoring.UniversalSplit.firstComponent
def OAI.ExactQuantumFactoring.dataCanonicalResidue line 99
Source documentation
Checking the uniquely specified CRT residue needs only congruences against the supplied prime powers; no CRT search is hidden in the guess validator.
```
noncomputable def dataCanonicalResidue (data : FactorData) (a m : ℕ) : Prop :=
…
```
Mentions: OAI.ExactQuantumFactoring.FactorData
lemma OAI.ExactQuantumFactoring.canonical_component_val line 104
lemma OAI.ExactQuantumFactoring.dataCanonicalResidue_correct line 122