OAI/Computability/QuantumFactoring/RetainedQuarterFilter.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.PhysicalTree.launchHistory line 20
  2. def OAI.ExactQuantumFactoring.PhysicalTree.launchInput line 22
  3. def OAI.ExactQuantumFactoring.PhysicalTree.paddedHistory line 24
  4. def OAI.ExactQuantumFactoring.PhysicalTree.paddedInput line 26
  5. def OAI.ExactQuantumFactoring.PhysicalTree.paddedPad line 28
  6. lemma OAI.ExactQuantumFactoring.PhysicalTree.paddedHistory_eval line 31
  7. lemma OAI.ExactQuantumFactoring.PhysicalTree.paddedInput_eval line 37
  8. lemma OAI.ExactQuantumFactoring.PhysicalTree.paddedPad_eval line 42
  9. def OAI.ExactQuantumFactoring.PhysicalTree.padFlag line 47
  10. lemma OAI.ExactQuantumFactoring.PhysicalTree.padFlag_eval line 49
  11. def OAI.ExactQuantumFactoring.PhysicalTree.paddedFlag line 54
  12. lemma OAI.ExactQuantumFactoring.PhysicalTree.paddedFlag_eval line 57
  13. def OAI.ExactQuantumFactoring.PhysicalTree.quarterOrd line 65
  14. def OAI.ExactQuantumFactoring.PhysicalTree.quarterGuess line 66
  15. def OAI.ExactQuantumFactoring.PhysicalTree.quarterCoin line 67
  16. def OAI.ExactQuantumFactoring.PhysicalTree.quarterRare line 68
  17. lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterOrd_eval line 70
  18. lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterGuess_eval line 73
  19. lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterCoin_eval line 76
  20. lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterRare_eval line 79
  21. def OAI.ExactQuantumFactoring.PhysicalTree.quarterKeep line 83
  22. lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterKeep_eval line 85
  23. def OAI.ExactQuantumFactoring.PhysicalTree.quarterGuessFlag line 91
  24. lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterGuessFlag_eval line 93
  25. def OAI.ExactQuantumFactoring.PhysicalTree.quarterFlag line 100
  26. theorem OAI.ExactQuantumFactoring.PhysicalTree.quarterFlag_eval line 107

    Source documentation

    The literal Boolean flag for the source's exact quarter event. All factor and order tests read the actual retained history, not an ideal initialized table.

    theorem quarterFlag_eval {n N : ℕ} (hn : 128≤n) (hN : 2≤N) (hb : N<2^n)
    (r : Quarter.Raw (PaddedRaw n) n) :
    (quarterFlag n (by omega)).eval (quarterEncoding n N r) 0=true ↔
      Quarter.passed N (paddedAccepted (N:=N) (by omega)) r := by
…

    Mentions: OAI.ExactQuantumFactoring.Quarter.Raw, OAI.ExactQuantumFactoring.PhysicalTree.PaddedRaw, OAI.ExactQuantumFactoring.PhysicalTree.quarterFlag, OAI.ExactQuantumFactoring.PhysicalTree.quarterEncoding, OAI.ExactQuantumFactoring.Quarter.passed, OAI.ExactQuantumFactoring.PhysicalTree.paddedAccepted

  27. def OAI.ExactQuantumFactoring.PhysicalTree.paddedOutputNet line 116
  28. def OAI.ExactQuantumFactoring.PhysicalTree.quarterOutputNet line 118
  29. lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterOutputNet_eval line 120