OAI/NumberTheory/TwoPoint/Circuits/CircuitGateFailure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The sampled AND polynomial agrees with the Boolean gate whenever the samplers isolate a false child; all-true inputs are always exact.

  1. def OAI.TwoPointCorrelations.sampledCoordinates line 14
  2. def OAI.TwoPointCorrelations.falseCoordinates line 17
  3. def OAI.TwoPointCorrelations.sampledAndPolynomial line 20
  4. def OAI.TwoPointCorrelations.boolAndValue line 24
  5. lemma OAI.TwoPointCorrelations.sampledAndPolynomial_degree line 27
  6. lemma OAI.TwoPointCorrelations.isolatesOne_card line 46
  7. lemma OAI.TwoPointCorrelations.sampled_false_card line 62
  8. lemma OAI.TwoPointCorrelations.sampledAndPolynomial_all_true line 73
  9. lemma OAI.TwoPointCorrelations.sampledAndPolynomial_isolated line 82
  10. lemma OAI.TwoPointCorrelations.sampledAndPolynomial_failure line 91