AuxiliaryProducer.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.ExactQuantumFactoring.DataProducer.NodeKey line 23
Source documentation
Each occurrence carries its complete ancestral path. Equal labels under separate parents are never identified or memoized.
```
abbrev NodeKey := List ℕ × ℕ
```
abbrev OAI.ExactQuantumFactoring.DataProducer.Choices line 24
def OAI.ExactQuantumFactoring.DataProducer.nodeRun line 26
def OAI.ExactQuantumFactoring.DataProducer.NodeGood line 29
def OAI.ExactQuantumFactoring.DataProducer.build line 35
Source documentation
The source's factor-and-recurse producer, with a depth cap. The Finsupp is only a representation of the multiplicities in the returned prime list; primeRecord never computes an unknown prime factorization.
```
noncomputable def build (n : ℕ) (choose : Choices) : ℕ→List ℕ→ℕ→Logged NodeKey FactorData
  | 0, _, _ => Logged.abort
  | depth+1, path, m => (nodeRun n choose path m).bind (fun ps =>
      (Logged.traverse (fun d => build n choose depth (path++[d]) d)
        (recordChildren (primeRecord ps))).map (FactorData.node m (primeRecord ps)))
```
Mentions: OAI.ExactQuantumFactoring.DataProducer.Choices, OAI.ExactQuantumFactoring.Logged, OAI.ExactQuantumFactoring.DataProducer.NodeKey, OAI.ExactQuantumFactoring.FactorData, OAI.ExactQuantumFactoring.Logged.abort, OAI.ExactQuantumFactoring.DataProducer.nodeRun, OAI.ExactQuantumFactoring.Logged.traverse, OAI.ExactQuantumFactoring.recordChildren, OAI.ExactQuantumFactoring.primeRecord
lemma OAI.ExactQuantumFactoring.DataProducer.nodeRun_complete line 41
lemma OAI.ExactQuantumFactoring.DataProducer.nodeRun_record line 54
lemma OAI.ExactQuantumFactoring.DataProducer.child_level_empty line 60
theorem OAI.ExactQuantumFactoring.DataProducer.build_complete line 70
Source documentation
Literal all-good completion follows the actual short-circuit trace. There is no hypothesis about queries or child occurrences that this run never made.
```
theorem build_complete (n : ℕ) (choose : Choices) (depth : ℕ) (path : List ℕ) (m : ℕ)
    (hm : 2 ≤ m) (hb : m<2^n) (hd : level m depth=[])
    (hg : Logged.Good (NodeGood n choose) (build n choose depth path m)) :
    (build n choose depth path m).result=some (trueData m) := by
…
```
Mentions: OAI.ExactQuantumFactoring.DataProducer.Choices, OAI.ExactQuantumFactoring.Logged.Good, OAI.ExactQuantumFactoring.DataProducer.NodeGood, OAI.ExactQuantumFactoring.DataProducer.build, OAI.ExactQuantumFactoring.trueData
theorem OAI.ExactQuantumFactoring.DataProducer.build_sound line 94
Source documentation
Even a bad run cannot produce false accepted data. Every successful local prime list and all ordered descendants agree with the canonical occurrence tree.
```
theorem build_sound (n : ℕ) (choose : Choices) (depth : ℕ) (path : List ℕ) (m : ℕ)
    {d : FactorData} (hs : (build n choose depth path m).result=some d) : d=trueData m := by
…
```
Mentions: OAI.ExactQuantumFactoring.DataProducer.Choices, OAI.ExactQuantumFactoring.FactorData, OAI.ExactQuantumFactoring.DataProducer.build, OAI.ExactQuantumFactoring.trueData
theorem OAI.ExactQuantumFactoring.DataProducer.bounded_complete line 111