AuxiliaryData.lean`

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.ExactQuantumFactoring.FactorRecord line 19
Source documentation
The source's distinct positive-exponent factor records. Finsupp stores each prime once; its canonical serialization sorts its support in increasing order.
```
abbrev FactorRecord := ℕ→₀ℕ
```
def OAI.ExactQuantumFactoring.factorRecordList line 21
def OAI.ExactQuantumFactoring.recordChildren line 24
inductive OAI.ExactQuantumFactoring.FactorData line 27
def OAI.ExactQuantumFactoring.FactorData.label line 30
def OAI.ExactQuantumFactoring.trueData line 33
lemma OAI.ExactQuantumFactoring.trueData_eq line 38
lemma OAI.ExactQuantumFactoring.trueData_label line 44
lemma OAI.ExactQuantumFactoring.recordChildren_factorization line 47
inductive OAI.ExactQuantumFactoring.FactorData.Valid line 51
Source documentation
Complete-data acceptance. The local tests are finite prime checks and a product check, followed by EXACT ordered children; no witness fields or advice.
```
inductive FactorData.Valid : FactorData→Prop where
…
```
Mentions: OAI.ExactQuantumFactoring.FactorData
lemma OAI.ExactQuantumFactoring.valid_factorRecord line 57
theorem OAI.ExactQuantumFactoring.valid_eq_trueData line 63
Source documentation
Unique prime factorization makes the entire ordered occurrence tree unique; equal child labels under different parents remain separate list occurrences.
```
theorem valid_eq_trueData {d : FactorData} (hd : d.Valid) : d=trueData d.label := by
…
```
Mentions: OAI.ExactQuantumFactoring.FactorData, OAI.ExactQuantumFactoring.trueData
theorem OAI.ExactQuantumFactoring.trueData_valid line 81
Source documentation
The canonical data are always complete; recursion is justified by the literal source decrease p−1<m, not a guessed tree.
```
theorem trueData_valid {m : ℕ} (hm : 2 ≤ m) : (trueData m).Valid := by
…
```
Mentions: OAI.ExactQuantumFactoring.trueData
theorem OAI.ExactQuantumFactoring.valid_iff_trueData line 95