OAI/Computability/QuantumFactoring/TreePadding.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.PhysicalTree.slots line 21

   Source documentation

   The actual tree has 2n² nodes, 2n split clocks per node, one list slot and n^5 padded base/order slots per split. This is not the n^10 padding cap.

   def slots (n : ℕ) : ℕ := ((n^5+1)*(2*n))*(2*n^2)

2. def OAI.ExactQuantumFactoring.PhysicalTree.padding line 22
3. lemma OAI.ExactQuantumFactoring.PhysicalTree.slots_le line 24
4. lemma OAI.ExactQuantumFactoring.PhysicalTree.slots_add_padding line 36
5. abbrev OAI.ExactQuantumFactoring.PhysicalTree.PadRaw line 39
6. def OAI.ExactQuantumFactoring.PhysicalTree.padState line 40
7. def OAI.ExactQuantumFactoring.PhysicalTree.padPassed line 41
8. def OAI.ExactQuantumFactoring.PhysicalTree.padProgram line 43
9. lemma OAI.ExactQuantumFactoring.PhysicalTree.padProgram_length line 46
10. lemma OAI.ExactQuantumFactoring.PhysicalTree.padProgram_state line 49
11. lemma OAI.ExactQuantumFactoring.PhysicalTree.pad_normalized line 56
12. lemma OAI.ExactQuantumFactoring.PhysicalTree.pad_mass line 59
13. abbrev OAI.ExactQuantumFactoring.PhysicalTree.PaddedRaw line 71
14. def OAI.ExactQuantumFactoring.PhysicalTree.paddedState line 72
15. def OAI.ExactQuantumFactoring.PhysicalTree.paddedAccepted line 74
16. lemma OAI.ExactQuantumFactoring.PhysicalTree.padded_normalized line 77
17. theorem OAI.ExactQuantumFactoring.PhysicalTree.padded_mass line 88

    Source documentation

    Exact manuscript P_n, now for the actual chronological physical tree, retrospective checks on its own data log, and literal nonzero-word padding.

    theorem padded_mass {n N : ℕ} (hn : 128≤n) (hN : 2≤N) (hb : N<2^n) :
        outcomeMass (paddedAccepted (n:=n) (N:=N) (by omega)) (paddedState n N)=
    …

    Mentions: OAI.ExactQuantumFactoring.PhysicalTree.paddedAccepted, OAI.ExactQuantumFactoring.PhysicalTree.paddedState