TreeRootOutput.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.PhysicalTree.flattenWords line 23
Source documentation
Only a fixed rearrangement of output wires, from tensor grouping to the source's consecutive n-bit fields. No factor search is present.
```
def flattenWords (n : ℕ) : BooleanNetwork (tensorWidth n n) (n*n) :=
…
```
Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.tensorWidth
lemma OAI.ExactQuantumFactoring.PhysicalTree.flattenWords_numbers line 26
def OAI.ExactQuantumFactoring.PhysicalTree.rootFlat line 39
Source documentation
A literal bounded readout for every clock count, with a harmless zero case.
```
def rootFlat (n : ℕ) : (t : ℕ)→BooleanNetwork ((machine n).width t) (n*n)
  | 0=>Completion.zeros _ _
  | t+1=>(rootResult n t).comp (flattenWords n)
```
Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.PhysicalTree.machine, OAI.ExactQuantumFactoring.PhysicalTree.width, OAI.ExactQuantumFactoring.Completion.zeros, OAI.ExactQuantumFactoring.PhysicalTree.rootResult, OAI.ExactQuantumFactoring.PhysicalTree.flattenWords
lemma OAI.ExactQuantumFactoring.PhysicalTree.rootFlat_correct line 43
def OAI.ExactQuantumFactoring.PhysicalTree.ordinaryOutput line 52
theorem OAI.ExactQuantumFactoring.PhysicalTree.padded_output line 57
Source documentation
Soundness uses verifier success on this raw history, not ideal quantum success or an externally supplied prime-factorization list.
```
theorem padded_output {n N : ℕ} (hn : 128≤n) (hN : 2≤N) (hb : N<2^n)
    (r : PaddedRaw n) (hp : paddedAccepted (N:=N) (by omega) r) :
…
```
Mentions: OAI.ExactQuantumFactoring.PhysicalTree.PaddedRaw, OAI.ExactQuantumFactoring.PhysicalTree.paddedAccepted
theorem OAI.ExactQuantumFactoring.PhysicalTree.quarter_mass line 75
Source documentation
Both branches of Section 6's final quarter-probability preparation now use the actual chronological tree. This is an event/output theorem; it does not assert the missing efficient Boolean implementation of the full flag.
```
theorem quarter_mass {n N : ℕ} (hn : 128≤n) (hN : 2≤N) (hb : N<2^n) :
    outcomeMass (Quarter.passed N (paddedAccepted (n:=n) (N:=N) (by omega)))
…
```
Mentions: OAI.ExactQuantumFactoring.Quarter.passed, OAI.ExactQuantumFactoring.PhysicalTree.paddedAccepted
theorem OAI.ExactQuantumFactoring.PhysicalTree.quarter_output line 80