DivisorData.lean`

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.recordPrimes line 21
Source documentation
Expand ONLY the supplied exponent record. No factoring operation is hidden in the list used by the retrospective controller.
```
def recordPrimes (f : FactorRecord) : List ℕ :=
…
```
Mentions: OAI.ExactQuantumFactoring.FactorRecord
lemma OAI.ExactQuantumFactoring.recordPrimes_prime line 24
lemma OAI.ExactQuantumFactoring.recordPrimes_prod line 32
lemma OAI.ExactQuantumFactoring.recordPrimes_length line 38
def OAI.ExactQuantumFactoring.divisorPrimes line 46
Source documentation
Divide a subfactor from the parent's prime list, in bounded time: there is at most one division per prime occurrence in the already supplied list.
```
def divisorPrimes : ℕ→List ℕ→List ℕ
  | _, [] => []
  | m, p::ps => if p∣m then p::divisorPrimes (m/p) ps else divisorPrimes m ps
```
lemma OAI.ExactQuantumFactoring.divisorPrimes_length line 50
lemma OAI.ExactQuantumFactoring.divisorPrimes_prime line 59
lemma OAI.ExactQuantumFactoring.divisorPrimes_prod line 73
def OAI.ExactQuantumFactoring.FactorData.factors line 88
Source documentation
Literal stored record projection, used only after complete-data validation.
```
def FactorData.factors : FactorData→FactorRecord
  | .node _ f _ => f
```
Mentions: OAI.ExactQuantumFactoring.FactorData, OAI.ExactQuantumFactoring.FactorRecord
def OAI.ExactQuantumFactoring.FactorData.descendants line 91
lemma OAI.ExactQuantumFactoring.trueData_factors line 94
lemma OAI.ExactQuantumFactoring.trueData_descendants line 96
def OAI.ExactQuantumFactoring.dataDivisorPrimes line 99
lemma OAI.ExactQuantumFactoring.dataDivisorPrimes_correct line 102
def OAI.ExactQuantumFactoring.dataChildPrimes line 115
Source documentation
Child lookup takes the first matching stored occurrence. It does not compute new children. Distinct parents deliberately retain separate occurrence data.
```
def dataChildPrimes (data : FactorData) (label : ℕ) : List ℕ :=
…
```
Mentions: OAI.ExactQuantumFactoring.FactorData
lemma OAI.ExactQuantumFactoring.dataChildPrimes_correct line 120
def OAI.ExactQuantumFactoring.dataTotientPrimes line 141
Source documentation
phi factors are reconstructed from division against the supplied parent record and the supplied p−1 children. The p=2 contribution requires no child.
```
noncomputable def dataTotientPrimes (data : FactorData) (m : ℕ) : List ℕ :=
…
```
Mentions: OAI.ExactQuantumFactoring.FactorData
lemma OAI.ExactQuantumFactoring.dataTotientPrimes_correct line 146
theorem OAI.ExactQuantumFactoring.data_strip_order line 187
Source documentation
Section5's retrospective order algorithm instantiated with the actual supplied auxiliary data, not with a hypothesized factorization of phi.
```
theorem data_strip_order {M m : ℕ} (hM : 0<M) (hm : 2 ≤ m) (hd : m∣M)
    (a : (ZMod m)ˣ) :
    stripOrderFactors a (dataTotientPrimes (trueData M) m) m.totient=orderOf a := by
…
```
Mentions: OAI.ExactQuantumFactoring.stripOrderFactors, OAI.ExactQuantumFactoring.dataTotientPrimes, OAI.ExactQuantumFactoring.trueData