OAI/NumberTheory/TwoPoint/Circuits/CircuitIsolationEvent.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The single-hit test used by the random polynomial is itself a small constant-depth circuit on the original child outputs.

  1. def OAI.TwoPointCorrelations.AC0Circuit.certificateDisjunction line 16
  2. lemma OAI.TwoPointCorrelations.AC0Circuit.certificateDisjunction_eval line 20
  3. lemma OAI.TwoPointCorrelations.AC0Circuit.certificateDisjunction_depth line 26
  4. lemma OAI.TwoPointCorrelations.AC0Circuit.certificateDisjunction_size line 32
  5. def OAI.TwoPointCorrelations.AC0Circuit.uniqueFalseTerm line 36
  6. lemma OAI.TwoPointCorrelations.AC0Circuit.uniqueFalseTerm_eval line 40
  7. def OAI.TwoPointCorrelations.AC0Circuit.uniqueFalseCircuit line 59
  8. lemma OAI.TwoPointCorrelations.AC0Circuit.uniqueFalseCircuit_eval line 63
  9. lemma OAI.TwoPointCorrelations.AC0Circuit.uniqueFalseTerm_depth line 69
  10. lemma OAI.TwoPointCorrelations.AC0Circuit.uniqueFalseCircuit_depth line 76
  11. lemma OAI.TwoPointCorrelations.AC0Circuit.uniqueFalseTerm_size line 81
  12. lemma OAI.TwoPointCorrelations.AC0Circuit.uniqueFalseCircuit_size line 90
  13. lemma OAI.TwoPointCorrelations.AC0Circuit.uniqueFalseCircuit_size_le line 96