OAI/Combinatorics/ContingencyTables/Counting/CompanionRestartStageProgram.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

One executed warm-restart stage

The context supplies the phase, immutable oracle metadata and deterministic precision markers. The matrix is the stored multiplier for that phase.

  1. abbrev OAI.ContingencyTables.CompanionRestartStageProgram.Request line 16
  2. abbrev OAI.ContingencyTables.CompanionRestartStageProgram.Input line 17
  3. def OAI.ContingencyTables.CompanionRestartStageProgram.context line 19
  4. def OAI.ContingencyTables.CompanionRestartStageProgram.contextRealizer line 20
  5. lemma OAI.ContingencyTables.CompanionRestartStageProgram.polynomial_context line 21
  6. def OAI.ContingencyTables.CompanionRestartStageProgram.frame line 24
  7. def OAI.ContingencyTables.CompanionRestartStageProgram.frameRealizer line 27
  8. lemma OAI.ContingencyTables.CompanionRestartStageProgram.polynomial_frame line 34
  9. def OAI.ContingencyTables.CompanionRestartStageProgram.cap line 40
  10. def OAI.ContingencyTables.CompanionRestartStageProgram.capRealizer line 41
  11. lemma OAI.ContingencyTables.CompanionRestartStageProgram.polynomial_cap line 44
  12. def OAI.ContingencyTables.CompanionRestartStageProgram.repetitions line 47
  13. def OAI.ContingencyTables.CompanionRestartStageProgram.repetitionsRealizer line 48
  14. lemma OAI.ContingencyTables.CompanionRestartStageProgram.polynomial_repetitions line 51
  15. def OAI.ContingencyTables.CompanionRestartStageProgram.fixed line 56
  16. def OAI.ContingencyTables.CompanionRestartStageProgram.fixedRealizer line 57
  17. lemma OAI.ContingencyTables.CompanionRestartStageProgram.polynomial_fixed line 58
  18. def OAI.ContingencyTables.CompanionRestartStageProgram.prepare line 61
  19. def OAI.ContingencyTables.CompanionRestartStageProgram.prepareRealizer line 63
  20. lemma OAI.ContingencyTables.CompanionRestartStageProgram.polynomial_prepare line 67
  21. def OAI.ContingencyTables.CompanionRestartStageProgram.output line 73
  22. def OAI.ContingencyTables.CompanionRestartStageProgram.outputRealizer line 74
  23. theorem OAI.ContingencyTables.CompanionRestartStageProgram.polynomial_output line 77
  24. def OAI.ContingencyTables.CompanionRestartStageProgram.width line 80
  25. def OAI.ContingencyTables.CompanionRestartStageProgram.widthRealizer line 82
  26. theorem OAI.ContingencyTables.CompanionRestartStageProgram.polynomial_width line 89