OAI/Computability/QuantumFactoring/FlatDataView.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.DataView line 20

    Source documentation

    Precisely the supplied local record and p−1 lookup facts consumed by the retrospective arithmetic. This is established below from actual verified rows.

    def DataView (d : FactorData) (M : ℕ) : Prop :=
…

    Mentions: OAI.ExactQuantumFactoring.FactorData

  2. lemma OAI.ExactQuantumFactoring.trueData_view line 24
  3. def OAI.ExactQuantumFactoring.PhysicalTree.rowData line 40
  4. def OAI.ExactQuantumFactoring.PhysicalTree.flatData line 42
  5. lemma OAI.ExactQuantumFactoring.PhysicalTree.rowData_label line 44
  6. lemma OAI.ExactQuantumFactoring.PhysicalTree.rowData_factors line 45
  7. theorem OAI.ExactQuantumFactoring.PhysicalTree.completeLog_view line 53

    Source documentation

    The read-only view is constructed solely by projection of retained fields. No trueData or factorization operation occurs in its definition.

    theorem completeLog_view {n N M : ℕ} {rows : List (ℕ×List ℕ)}
    (h : CompleteLog n N rows) (hM : M∈rows.map Prod.fst) (hpos : M≠0) :
    DataView (flatData rows M) M := by
…

    Mentions: OAI.ExactQuantumFactoring.PhysicalTree.CompleteLog, OAI.ExactQuantumFactoring.DataView, OAI.ExactQuantumFactoring.PhysicalTree.flatData

  8. lemma OAI.ExactQuantumFactoring.DataView.divisorPrimes line 84
  9. lemma OAI.ExactQuantumFactoring.DataView.record line 86
  10. lemma OAI.ExactQuantumFactoring.DataView.phi line 88
  11. lemma OAI.ExactQuantumFactoring.DataView.favorable line 90
  12. lemma OAI.ExactQuantumFactoring.DataView.childPrimes line 92
  13. lemma OAI.ExactQuantumFactoring.DataView.totientPrimes line 95
  14. lemma OAI.ExactQuantumFactoring.DataView.order line 107
  15. lemma OAI.ExactQuantumFactoring.DataView.listSuccess line 109
  16. lemma OAI.ExactQuantumFactoring.DataView.orderSuccess line 111