OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

A fixed polynomial envelope for the executed Boolean optimizer. The expression below records precisely the arithmetic cost formula; its degree proof avoids expanding powers or changing any computational limit.

  1. inductive OAI.EditApproximation.NumericalCostInput line 11
  2. inductive OAI.EditApproximation.NumericalCostExpression line 15
  3. instance OAI.EditApproximation.(instance at line 24) line 24
  4. instance OAI.EditApproximation.(instance at line 25) line 25
  5. instance OAI.EditApproximation.(instance at line 26) line 26
  6. instance OAI.EditApproximation.(instance at line 27) line 27
  7. def OAI.EditApproximation.NumericalCostExpression.eval line 29
  8. def OAI.EditApproximation.NumericalCostExpression.degree line 38
  9. theorem OAI.EditApproximation.NumericalCostExpression.eval_le_pow line 47
  10. def OAI.EditApproximation.numericalCostEnvironment line 72
  11. abbrev OAI.EditApproximation.CE line 83

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:11 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.CE@path.

  12. def OAI.EditApproximation.costSize line 85
  13. def OAI.EditApproximation.costMax line 86
  14. def OAI.EditApproximation.expressionLogStorage line 88

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:15 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionLogStorage@path.

  15. def OAI.EditApproximation.expressionGradientStorage line 91

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:18 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionGradientStorage@path.

  16. def OAI.EditApproximation.expressionPoint line 94

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:21 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionPoint@path.

  17. def OAI.EditApproximation.expressionLogUniversal line 97

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:24 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionLogUniversal@path.

  18. def OAI.EditApproximation.expressionLogStep line 101

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:28 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionLogStep@path.

  19. def OAI.EditApproximation.expressionLogBit line 105

    Also declared: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:32 (same declaration text).

  20. def OAI.EditApproximation.expressionGradientBit line 110

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:37 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionGradientBit@path.

  21. def OAI.EditApproximation.expressionMaximizer line 120

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:47 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionMaximizer@path.

  22. def OAI.EditApproximation.expressionUpdate line 124

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:51 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionUpdate@path.

  23. def OAI.EditApproximation.expressionOptimizer line 130

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:57 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionOptimizer@path.

  24. def OAI.EditApproximation.optimizerCostExpression line 137
  25. def OAI.EditApproximation.optimizerBitPolynomialDegree line 141
  26. theorem OAI.EditApproximation.optimizerCostExpression_eval line 143
  27. theorem OAI.EditApproximation.optimizerBitBudget_le_fixed_power line 165
  28. theorem OAI.EditApproximation.booleanOptimizer_cost_le_fixed_power line 174
  29. def OAI.EditApproximation.expressionBandSumStorage line 189

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:63 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionBandSumStorage@path.

  30. def OAI.EditApproximation.expressionBandVertexWord line 192

    Also declared: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:66 (same declaration text).

  31. def OAI.EditApproximation.expressionStoredSumWord line 195

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:69 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionStoredSumWord@path.

  32. def OAI.EditApproximation.expressionStoredSumBit line 198

    Also declared: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:72 (same declaration text).

  33. def OAI.EditApproximation.expressionBandCoordinateBit line 201

    Also declared: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:75 (same declaration text).

  34. def OAI.EditApproximation.expressionBandPreparation line 204

    Also declared: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:78 (same declaration text).

  35. def OAI.EditApproximation.expressionOptimisticStorage line 207

    Also declared: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:81 (same declaration text).

  36. def OAI.EditApproximation.expressionOnlineStorage line 209

    Also declared: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:83 (same declaration text).

  37. def OAI.EditApproximation.expressionGainBit line 213

    Also declared: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:87 (same declaration text).

  38. def OAI.EditApproximation.expressionDecrementBit line 215

    Also declared: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:89 (same declaration text).

  39. def OAI.EditApproximation.expressionCoefficientBit line 218

    Also declared: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:92 (same declaration text).

  40. def OAI.EditApproximation.expressionOptimisticBit line 221

    Also declared: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:95 (same declaration text).

  41. def OAI.EditApproximation.expressionOnlineBit line 226

    Also declared: OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean:100 (same declaration text).

  42. def OAI.EditApproximation.preparedOptimizerCostExpression line 233
  43. def OAI.EditApproximation.preparedCostEnvironment line 249
  44. def OAI.EditApproximation.preparedOptimizerBitPolynomialDegree line 263
  45. theorem OAI.EditApproximation.preparedOptimizerCostExpression_eval line 265
  46. theorem OAI.EditApproximation.preparedBandOptimizerBitBudget_le_fixed_power line 300