OAI/Combinatorics/EditApproximation/Queries/QueryInitialWarmupPolynomial.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Polynomial certificate for the complete initial and warmup dispatch, including actual gathers, buffer scans, and the previous-pass median.

  1. abbrev OAI.EditApproximation.GP line 12

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Binary/BinarySampledGroupPolynomial.lean:12 (same statement text; different proof or body), OAI/Combinatorics/EditApproximation/Queries/QueryCallbackPolynomial.lean:9 (same statement text; different proof or body), OAI/Combinatorics/EditApproximation/Queries/QueryGatherPolynomial.lean:13 (same statement text; different proof or body), OAI/Combinatorics/EditApproximation/Queries/QueryRawWidthPolynomial.lean:9 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.GP@path.

  2. def OAI.EditApproximation.gp_initialScaleGuardBitBudget line 14
  3. def OAI.EditApproximation.gp_gridPointsBitBudget line 18

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryGatherPolynomial.lean:25 (same declaration text).

  4. def OAI.EditApproximation.gp_gridStateBoxBitBudget line 21

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryGatherPolynomial.lean:28 (same declaration text).

  5. def OAI.EditApproximation.gp_queryGridPointsBitBudget line 25

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryGatherPolynomial.lean:32 (same declaration text).

  6. def OAI.EditApproximation.gp_queryInitialCentersBitBudget line 28
  7. def OAI.EditApproximation.gp_queryInitialSeedReadBudget line 34
  8. def OAI.EditApproximation.gp_queryInitialProgramBitBudget line 37
  9. def OAI.EditApproximation.gp_queryChargedSeedBitBudget line 42
  10. def OAI.EditApproximation.gp_queryPhysicalInitialBitBudget line 46
  11. def OAI.EditApproximation.gp_localEligibilityBitBudget line 50

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryGatherPolynomial.lean:15 (same declaration text).

  12. def OAI.EditApproximation.gp_queryExponentsBitBudget line 54

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryGatherPolynomial.lean:19 (same declaration text).

  13. def OAI.EditApproximation.gp_queryScalesBitBudget line 57

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryGatherPolynomial.lean:22 (same declaration text).

  14. def OAI.EditApproximation.gp_queryRawCentersBitBudget line 60

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryGatherPolynomial.lean:35 (same declaration text).

  15. def OAI.EditApproximation.gp_queryWarmupRepresentatives line 67
  16. def OAI.EditApproximation.gp_localRepresentativeScaleBitBudget line 70

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryGatherPolynomial.lean:92 (same declaration text).

  17. def OAI.EditApproximation.gp_localRepresentativesBitBudget line 76

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryGatherPolynomial.lean:98 (same declaration text).

  18. def OAI.EditApproximation.gp_wideChildGridBitBudget line 80

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryGatherPolynomial.lean:114 (same declaration text).

  19. def OAI.EditApproximation.gp_queryWideInputsBitBudget line 83

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryGatherPolynomial.lean:117 (same declaration text).

  20. def OAI.EditApproximation.gp_queryWarmupInputsBitBudget line 89
  21. def OAI.EditApproximation.gp_queryWarmupParentReadBudget line 93
  22. def OAI.EditApproximation.gp_queryWarmupChildReadBudget line 96
  23. def OAI.EditApproximation.gp_queryWarmupProgramBitBudget line 99
  24. def OAI.EditApproximation.gp_queryChargedWarmupBitBudget line 106
  25. def OAI.EditApproximation.initialWarmupPolynomial line 111
  26. def OAI.EditApproximation.queryInitialWarmupBitDegree line 116
  27. def OAI.EditApproximation.initialWarmupEnvironment line 118
  28. theorem OAI.EditApproximation.initialWarmupPolynomial_eval line 123
  29. theorem OAI.EditApproximation.queryChargedWarmupBitBudget_fixedPower line 128