OAI/Computability/QuantumFactoring/ThresholdRetention.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact threshold thinning by a FIXED (not rejection-sampled) block of fair bits. The complete block is retained in the physical history.

  1. def OAI.ExactQuantumFactoring.bitsNatEquiv line 19
  2. lemma OAI.ExactQuantumFactoring.bitsNatEquiv_val line 22
  3. lemma OAI.ExactQuantumFactoring.fair_threshold_mass line 25
  4. def OAI.ExactQuantumFactoring.thresholdExpr line 47

    Source documentation

    The natural floor implementation of the exact dyadic acceptance threshold.

    def thresholdExpr {v : Type*} (T : ℕ) (p : RatExpr v) (coin : NatExpr v) : NatExpr v :=
…

    Mentions: OAI.ExactQuantumFactoring.RatExpr, OAI.ExactQuantumFactoring.NatExpr

  5. lemma OAI.ExactQuantumFactoring.thresholdExpr_eval line 51
  6. lemma OAI.ExactQuantumFactoring.dyadic_fair_threshold line 60