OAI/Computability/QuantumFactoring/VerifiedTableOrder.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitArithmetic.tableOrderWidth line 20

    Source documentation

    The extra n bits make zero-extension unconditional, including empty malformed tables. On verified input this holds the entire repeated product.

    def tableOrderWidth (n f : ℕ) : ℕ := n*(n*f)+n+1
  2. def OAI.ExactQuantumFactoring.BitArithmetic.tableOrderPrimes line 22
  3. lemma OAI.ExactQuantumFactoring.BitArithmetic.tableOrderPrimes_values line 28
  4. lemma OAI.ExactQuantumFactoring.BitArithmetic.tableOrderPrimes_length line 39
  5. lemma OAI.ExactQuantumFactoring.BitArithmetic.tableOrderPrimes_product_bound line 45
  6. def OAI.ExactQuantumFactoring.BitArithmetic.tableOrder line 63

    Source documentation

    A literal order circuit using only retained verified table entries and modular powering. No mathematical factorization/support enumeration appears in its definition, even on malformed inputs.

    def tableOrder {k n : ℕ} (a m : BooleanNetwork k n)
    (rows : List (BooleanNetwork k n×List (BooleanNetwork k n))) : BooleanNetwork k n :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  7. theorem OAI.ExactQuantumFactoring.BitArithmetic.tableOrder_exact line 69
  8. def OAI.ExactQuantumFactoring.BitArithmetic.tableOrderBound line 98

    Source documentation

    This bound is polynomial in n, table length and the individual stored-word circuit cost. Resizing is itself a bounded circuit, not a word-RAM primitive.

    def tableOrderBound (n f c : ℕ) : ℕ :=
…
  9. lemma OAI.ExactQuantumFactoring.BitArithmetic.tableOrder_count line 103