OAI/Combinatorics/ContingencyTables/Rooted/RootedOracleConfigProgram.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

Computing a phase's physical oracle configuration

Numeric schedules use binary arithmetic. The supplied reserve bounds the two materialized precision markers; no binary natural controls an unbounded list allocation.

  1. abbrev OAI.ContingencyTables.RootedOracleConfigProgram.Input line 20
  2. def OAI.ContingencyTables.RootedOracleConfigProgram.fields line 22
  3. def OAI.ContingencyTables.RootedOracleConfigProgram.consR line 25
  4. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_consR line 29
  5. def OAI.ContingencyTables.RootedOracleConfigProgram.fieldsRealizer line 33
  6. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_fields line 45
  7. def OAI.ContingencyTables.RootedOracleConfigProgram.dim line 56
  8. def OAI.ContingencyTables.RootedOracleConfigProgram.grid line 57
  9. def OAI.ContingencyTables.RootedOracleConfigProgram.height line 58
  10. def OAI.ContingencyTables.RootedOracleConfigProgram.phase line 59
  11. def OAI.ContingencyTables.RootedOracleConfigProgram.mixing line 60
  12. def OAI.ContingencyTables.RootedOracleConfigProgram.allowance line 61
  13. def OAI.ContingencyTables.RootedOracleConfigProgram.relativeDenominator line 62
  14. def OAI.ContingencyTables.RootedOracleConfigProgram.scalar line 64
  15. def OAI.ContingencyTables.RootedOracleConfigProgram.scalarRealizer line 65
  16. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_scalar line 67
  17. def OAI.ContingencyTables.RootedOracleConfigProgram.inner line 70
  18. def OAI.ContingencyTables.RootedOracleConfigProgram.innerRealizer line 72
  19. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_inner line 78
  20. def OAI.ContingencyTables.RootedOracleConfigProgram.correction line 84
  21. def OAI.ContingencyTables.RootedOracleConfigProgram.correctionRealizer line 85
  22. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_correction line 88
  23. def OAI.ContingencyTables.RootedOracleConfigProgram.samples line 91
  24. def OAI.ContingencyTables.RootedOracleConfigProgram.samplesRealizer line 92
  25. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_samples line 96
  26. def OAI.ContingencyTables.RootedOracleConfigProgram.timeInput line 100
  27. def OAI.ContingencyTables.RootedOracleConfigProgram.timeInputRealizer line 101
  28. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_timeInput line 102
  29. def OAI.ContingencyTables.RootedOracleConfigProgram.ratioTime line 105
  30. def OAI.ContingencyTables.RootedOracleConfigProgram.ratioTimeRealizer line 106
  31. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_ratioTime line 109
  32. def OAI.ContingencyTables.RootedOracleConfigProgram.correctionTime line 112
  33. def OAI.ContingencyTables.RootedOracleConfigProgram.correctionTimeRealizer line 113
  34. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_correctionTime line 116
  35. def OAI.ContingencyTables.RootedOracleConfigProgram.offsetAccuracy line 119
  36. def OAI.ContingencyTables.RootedOracleConfigProgram.offsetAccuracyRealizer line 120
  37. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_offsetAccuracy line 124
  38. def OAI.ContingencyTables.RootedOracleConfigProgram.normalizedNoise line 128
  39. def OAI.ContingencyTables.RootedOracleConfigProgram.normalizedNoiseRealizer line 129
  40. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_normalizedNoise line 131
  41. def OAI.ContingencyTables.RootedOracleConfigProgram.repeats line 135
  42. def OAI.ContingencyTables.RootedOracleConfigProgram.repeatsRealizer line 136
  43. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_repeats line 142
  44. def OAI.ContingencyTables.RootedOracleConfigProgram.rootDegree line 148
  45. def OAI.ContingencyTables.RootedOracleConfigProgram.rootDegreeRealizer line 149
  46. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_rootDegree line 152
  47. def OAI.ContingencyTables.RootedOracleConfigProgram.depth line 156
  48. def OAI.ContingencyTables.RootedOracleConfigProgram.depthRealizer line 157
  49. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_depth line 158
  50. def OAI.ContingencyTables.RootedOracleConfigProgram.markers line 161
  51. def OAI.ContingencyTables.RootedOracleConfigProgram.markersRealizer line 162
  52. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_markers line 165
  53. def OAI.ContingencyTables.RootedOracleConfigProgram.schedule line 169
  54. def OAI.ContingencyTables.RootedOracleConfigProgram.scheduleRealizer line 171
  55. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_schedule line 174
  56. def OAI.ContingencyTables.RootedOracleConfigProgram.output line 178
  57. def OAI.ContingencyTables.RootedOracleConfigProgram.outputRealizer line 180
  58. theorem OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_output line 182
  59. def OAI.ContingencyTables.RootedOracleConfigProgram.context line 189
  60. def OAI.ContingencyTables.RootedOracleConfigProgram.contextRealizer line 190
  61. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_context line 193
  62. def OAI.ContingencyTables.RootedOracleConfigProgram.contextWidth line 197
  63. def OAI.ContingencyTables.RootedOracleConfigProgram.contextWidthRealizer line 198
  64. lemma OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_contextWidth line 201
  65. def OAI.ContingencyTables.RootedOracleConfigProgram.wordWidth line 205
  66. def OAI.ContingencyTables.RootedOracleConfigProgram.wordWidthRealizer line 206
  67. theorem OAI.ContingencyTables.RootedOracleConfigProgram.polynomial_wordWidth line 209
  68. def OAI.ContingencyTables.RootedOracleConfigProgram.data line 217
  69. lemma OAI.ContingencyTables.RootedOracleConfigProgram.fields_data line 221
  70. lemma OAI.ContingencyTables.RootedOracleConfigProgram.inner_data line 227
  71. lemma OAI.ContingencyTables.RootedOracleConfigProgram.repeats_data line 239