OAI/Computability/GeneralizedCircuits/Mesh.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Generalized-circuit smoothing, perturbation stability and rational meshes.

Gate satisfaction is conditional on a real fixed assignment, and mesh existence approximates a given cube point. Applying Brouwer and combining these lemmas to establish simultaneous totality remain unproved. QuasilinearPCPStatement is a goal proposition: the uniform quasilinear reduction, soundness, deterministic algorithm realization and complexity bounds also remain unproved.

  1. abbrev OAI.PCPforPPAD.BitString line 17
  2. abbrev OAI.PCPforPPAD.UnitRat line 18
  3. def OAI.PCPforPPAD.encodeNat line 20
  4. def OAI.PCPforPPAD.encodeRat line 23
  5. def OAI.PCPforPPAD.encodeList line 26
  6. inductive OAI.PCPforPPAD.BooleanGate line 29
  7. def OAI.PCPforPPAD.BooleanGate.eval line 35
  8. def OAI.PCPforPPAD.BooleanGate.encode line 40
  9. structure OAI.PCPforPPAD.BooleanCircuit line 45
  10. def OAI.PCPforPPAD.BooleanCircuit.wireValue line 50
  11. def OAI.PCPforPPAD.BooleanCircuit.eval line 62
  12. def OAI.PCPforPPAD.BooleanCircuit.encode line 66
  13. structure OAI.PCPforPPAD.EndOfLine line 72
  14. def OAI.PCPforPPAD.EndOfLine.IsSolution line 81
  15. def OAI.PCPforPPAD.EndOfLine.encode line 85
  16. def OAI.PCPforPPAD.EndOfLine.length line 87
  17. inductive OAI.PCPforPPAD.Gate line 89
  18. def OAI.PCPforPPAD.Gate.output line 101
  19. def OAI.PCPforPPAD.Gate.Satisfied line 105
  20. structure OAI.PCPforPPAD.GeneralizedCircuit line 121
  21. def OAI.PCPforPPAD.Gate.encode line 128
  22. def OAI.PCPforPPAD.GeneralizedCircuit.encode line 139
  23. def OAI.PCPforPPAD.GeneralizedCircuit.length line 143
  24. abbrev OAI.PCPforPPAD.RationalAssignment line 145
  25. def OAI.PCPforPPAD.RationalAssignment.toReal line 147
  26. def OAI.PCPforPPAD.RationalAssignment.encode line 150
  27. def OAI.PCPforPPAD.RationalAssignment.length line 153
  28. def OAI.PCPforPPAD.failedGates line 156
  29. def OAI.PCPforPPAD.Acceptable line 161
  30. structure OAI.PCPforPPAD.Algorithm line 166
  31. abbrev OAI.PCPforPPAD.Algorithm.Config line 170
  32. def OAI.PCPforPPAD.Algorithm.runSteps line 173
  33. def OAI.PCPforPPAD.Algorithm.RunsWithin line 177
  34. def OAI.PCPforPPAD.logFactor line 183
  35. def OAI.PCPforPPAD.QuasilinearPCPStatement line 185
  36. theorem OAI.PCPforPPAD.encodeNat_length line 201
  37. theorem OAI.PCPforPPAD.encodeNat_length_pos line 206
  38. theorem OAI.PCPforPPAD.BooleanCircuit.encode_length_pos line 210
  39. theorem OAI.PCPforPPAD.EndOfLine.length_ge_two line 216
  40. theorem OAI.PCPforPPAD.exists_other_endpoint line 222
  41. theorem OAI.PCPforPPAD.EndOfLine.exists_solution line 240
  42. theorem OAI.PCPforPPAD.acceptable_iff_floor_budget line 245
  43. def OAI.PCPforPPAD.clip01 line 252
  44. lemma OAI.PCPforPPAD.clip01_nonneg line 254
  45. lemma OAI.PCPforPPAD.clip01_le_one line 256
  46. lemma OAI.PCPforPPAD.clip01_eq_zero line 259
  47. lemma OAI.PCPforPPAD.clip01_eq_one line 262
  48. def OAI.PCPforPPAD.booleanSignal line 265
  49. lemma OAI.PCPforPPAD.booleanSignal_low line 267
  50. lemma OAI.PCPforPPAD.booleanSignal_high line 272
  51. lemma OAI.PCPforPPAD.booleanSignal_nonneg line 278
  52. lemma OAI.PCPforPPAD.booleanSignal_le_one line 280
  53. def OAI.PCPforPPAD.lessSignal line 282
  54. lemma OAI.PCPforPPAD.lessSignal_low line 284
  55. lemma OAI.PCPforPPAD.lessSignal_high line 292
  56. def OAI.PCPforPPAD.Gate.smoothedValue line 300
  57. lemma OAI.PCPforPPAD.low_input_before_perturbation line 311
  58. lemma OAI.PCPforPPAD.high_input_before_perturbation line 316
  59. lemma OAI.PCPforPPAD.low_output_after_perturbation line 321
  60. lemma OAI.PCPforPPAD.high_output_after_perturbation line 326
  61. lemma OAI.PCPforPPAD.abs_sum_perturbation line 331
  62. lemma OAI.PCPforPPAD.abs_difference_perturbation line 340
  63. theorem OAI.PCPforPPAD.Gate.satisfied_of_perturbation line 349
  64. theorem OAI.PCPforPPAD.all_gates_satisfied_of_perturbation line 468
  65. theorem OAI.PCPforPPAD.Gate.continuous_smoothedValue line 476
  66. theorem OAI.PCPforPPAD.Gate.smoothedValue_in_unit line 480
  67. def OAI.PCPforPPAD.GeneralizedCircuit.cubeMap line 511
  68. theorem OAI.PCPforPPAD.GeneralizedCircuit.cubeMap_at_output line 517
  69. theorem OAI.PCPforPPAD.GeneralizedCircuit.continuous_cubeMap line 525
  70. theorem OAI.PCPforPPAD.GeneralizedCircuit.cubeMap_in_unit line 536
  71. theorem OAI.PCPforPPAD.encodeNat_length_le line 546
  72. theorem OAI.PCPforPPAD.encodeList_length_le line 553
  73. theorem OAI.PCPforPPAD.encodeList_length_ge line 568
  74. theorem OAI.PCPforPPAD.GeneralizedCircuit.nodeCount_le_length line 581
  75. def OAI.PCPforPPAD.meshEntryBound line 589
  76. def OAI.PCPforPPAD.meshWitnessPolynomial line 592
  77. theorem OAI.PCPforPPAD.mesh_entry_length_le line 595
  78. theorem OAI.PCPforPPAD.RationalAssignment.mesh_length_le line 601
  79. theorem OAI.PCPforPPAD.exists_mesh_numerator line 618
  80. def OAI.PCPforPPAD.meshDenominator line 648
  81. theorem OAI.PCPforPPAD.meshDenominator_pos line 650
  82. theorem OAI.PCPforPPAD.mesh_error_le line 653
  83. theorem OAI.PCPforPPAD.exists_mesh_assignment line 664