OAI/Combinatorics/ContingencyTables/Rooted/RootedOracleStepProgram.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Polynomial execution of the catalog-order oracle step

The program uses the computed forest exponent twice, one arithmetic axis proposal and one independent bounded dyadic acceptance word.

  1. abbrev OAI.ContingencyTables.RootedOracleStepProgram.Data line 17
  2. abbrev OAI.ContingencyTables.RootedOracleStepProgram.StepInput line 18
  3. def OAI.ContingencyTables.RootedOracleStepProgram.replace line 20
  4. def OAI.ContingencyTables.RootedOracleStepProgram.replaceRealizer line 22
  5. lemma OAI.ContingencyTables.RootedOracleStepProgram.polynomial_replace line 24
  6. def OAI.ContingencyTables.RootedOracleStepProgram.candidate line 29
  7. def OAI.ContingencyTables.RootedOracleStepProgram.candidateRealizer line 31
  8. lemma OAI.ContingencyTables.RootedOracleStepProgram.polynomial_candidate line 36
  9. def OAI.ContingencyTables.RootedOracleStepProgram.currentData line 43
  10. def OAI.ContingencyTables.RootedOracleStepProgram.currentDataRealizer line 44
  11. lemma OAI.ContingencyTables.RootedOracleStepProgram.polynomial_currentData line 45
  12. def OAI.ContingencyTables.RootedOracleStepProgram.candidateData line 48
  13. def OAI.ContingencyTables.RootedOracleStepProgram.candidateDataRealizer line 50
  14. lemma OAI.ContingencyTables.RootedOracleStepProgram.polynomial_candidateData line 53
  15. def OAI.ContingencyTables.RootedOracleStepProgram.gap line 56
  16. def OAI.ContingencyTables.RootedOracleStepProgram.gapRealizer line 59
  17. lemma OAI.ContingencyTables.RootedOracleStepProgram.polynomial_gap line 68
  18. def OAI.ContingencyTables.RootedOracleStepProgram.acceptCandidate line 74
  19. def OAI.ContingencyTables.RootedOracleStepProgram.acceptCandidateRealizer line 76
  20. lemma OAI.ContingencyTables.RootedOracleStepProgram.polynomial_acceptCandidate line 81
  21. def OAI.ContingencyTables.RootedOracleStepProgram.step line 88
  22. def OAI.ContingencyTables.RootedOracleStepProgram.stepRealizer line 90
  23. theorem OAI.ContingencyTables.RootedOracleStepProgram.polynomial_step line 96
  24. def OAI.ContingencyTables.RootedOracleStepProgram.data line 108
  25. lemma OAI.ContingencyTables.RootedOracleStepProgram.evaluate_data line 114
  26. lemma OAI.ContingencyTables.RootedOracleStepProgram.replace_data line 120
  27. theorem OAI.ContingencyTables.RootedOracleStepProgram.step_pair line 124