OAI/NumberTheory/TwoPoint/Bounds/PaddingCutCircuit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary predicates of a bounded padding-prime state have a literal depth-two DNF. Conjoining a fixed divisor costs one layer.

  1. def OAI.TwoPointCorrelations.activePredicateCircuit line 14
  2. lemma OAI.TwoPointCorrelations.activePredicateCircuit_eval line 19
  3. lemma OAI.TwoPointCorrelations.activePredicateCircuit_depth line 33
  4. lemma OAI.TwoPointCorrelations.activePredicateCircuit_size line 37
  5. def OAI.TwoPointCorrelations.stateDivisorCircuit line 48
  6. lemma OAI.TwoPointCorrelations.stateDivisorCircuit_eval line 55
  7. lemma OAI.TwoPointCorrelations.stateDivisorCircuit_depth line 70
  8. lemma OAI.TwoPointCorrelations.stateDivisorCircuit_size line 80
  9. lemma OAI.TwoPointCorrelations.stateDivisorCircuit_size_exp line 93
  10. lemma OAI.TwoPointCorrelations.stateDivisorCircuit_integer line 141