OAI/Combinatorics/EditApproximation/Definitions.lean

GitHub source file

1155 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.bitWordValue line 14

   Also declared: ComparatorChallenges/EditApproximation.lean:14 (same declaration text).

2. def OAI.EditApproximation.bitSum line 18

   Also declared: ComparatorChallenges/EditApproximation.lean:18 (same declaration text).

3. def OAI.EditApproximation.bitCarry line 20

   Also declared: ComparatorChallenges/EditApproximation.lean:20 (same declaration text).

4. structure OAI.EditApproximation.UnreducedRational line 22

   Also declared: ComparatorChallenges/EditApproximation.lean:22 (same declaration text).

5. def OAI.EditApproximation.orderingMatches line 27

   Also declared: ComparatorChallenges/EditApproximation.lean:27 (same declaration text).

6. def OAI.EditApproximation.bitOrdering line 30

   Also declared: ComparatorChallenges/EditApproximation.lean:30 (same declaration text).

7. def OAI.EditApproximation.bitDifference line 36

   Also declared: ComparatorChallenges/EditApproximation.lean:36 (same declaration text).

8. def OAI.EditApproximation.bitBorrow line 38

   Also declared: ComparatorChallenges/EditApproximation.lean:38 (same declaration text).

9. structure OAI.EditApproximation.SignedBinary line 40

   Also declared: ComparatorChallenges/EditApproximation.lean:40 (same declaration text).

10. def OAI.EditApproximation.signedMagnitude line 44

    Also declared: ComparatorChallenges/EditApproximation.lean:44 (same declaration text).

11. def OAI.EditApproximation.trimBitWordWithWork line 47

    Also declared: ComparatorChallenges/EditApproximation.lean:47 (same declaration text).

12. def OAI.EditApproximation.balancedCut line 53

    Also declared: ComparatorChallenges/EditApproximation.lean:53 (same declaration text).

13. def OAI.EditApproximation.gridRound line 55

    Also declared: ComparatorChallenges/EditApproximation.lean:55 (same declaration text).

14. def OAI.EditApproximation.rationalMinimum line 57

    Also declared: ComparatorChallenges/EditApproximation.lean:57 (same declaration text).

15. structure OAI.EditApproximation.RationalBellmanAction line 61

    Also declared: ComparatorChallenges/EditApproximation.lean:61 (same declaration text).

16. def OAI.EditApproximation.rationalRefinementUpdate line 66

    Also declared: ComparatorChallenges/EditApproximation.lean:66 (same declaration text).

17. def OAI.EditApproximation.heightExponent line 70

    Also declared: ComparatorChallenges/EditApproximation.lean:70 (same declaration text).

18. def OAI.EditApproximation.coarseExponent line 72

    Also declared: ComparatorChallenges/EditApproximation.lean:72 (same declaration text).

19. structure OAI.EditApproximation.IntegerParameters line 74

    Also declared: ComparatorChallenges/EditApproximation.lean:74 (same declaration text).

20. structure OAI.EditApproximation.RationalParameters line 85

    Also declared: ComparatorChallenges/EditApproximation.lean:85 (same declaration text).

21. def OAI.EditApproximation.gridPointsBetween line 96

    Also declared: ComparatorChallenges/EditApproximation.lean:96 (same declaration text).

22. def OAI.EditApproximation.scaledSeedValue line 99

    Also declared: ComparatorChallenges/EditApproximation.lean:99 (same declaration text).

23. def OAI.EditApproximation.dyadicScales line 102

    Also declared: ComparatorChallenges/EditApproximation.lean:102 (same declaration text).

24. def OAI.EditApproximation.seedGridSpacing line 105

    Also declared: ComparatorChallenges/EditApproximation.lean:105 (same declaration text).

25. def OAI.EditApproximation.finiteAssignments line 107

    Also declared: ComparatorChallenges/EditApproximation.lean:107 (same declaration text).

26. def OAI.EditApproximation.powerTwoWord line 113

    Also declared: ComparatorChallenges/EditApproximation.lean:113 (same declaration text).

27. def OAI.EditApproximation.filterWithWork line 115

    Also declared: ComparatorChallenges/EditApproximation.lean:115 (same declaration text).

28. def OAI.EditApproximation.allWithWork line 122

    Also declared: ComparatorChallenges/EditApproximation.lean:122 (same declaration text).

29. def OAI.EditApproximation.arithmeticMapWithWork line 129

    Also declared: ComparatorChallenges/EditApproximation.lean:129 (same declaration text).

30. def OAI.EditApproximation.arithmeticFlatMapWithWork line 136

    Also declared: ComparatorChallenges/EditApproximation.lean:136 (same declaration text).

31. def OAI.EditApproximation.upperMedian line 143

    Also declared: ComparatorChallenges/EditApproximation.lean:143 (same declaration text).

32. def OAI.EditApproximation.filterMapWithWork line 146

    Also declared: ComparatorChallenges/EditApproximation.lean:146 (same declaration text).

33. def OAI.EditApproximation.cellGridPoints line 153

    Also declared: ComparatorChallenges/EditApproximation.lean:153 (same declaration text).

34. def OAI.EditApproximation.groupRoundSpacing line 157

    Also declared: ComparatorChallenges/EditApproximation.lean:157 (same declaration text).

35. def OAI.EditApproximation.refinementFactor line 160

    Also declared: ComparatorChallenges/EditApproximation.lean:160 (same declaration text).

36. def OAI.EditApproximation.localCellCoordinates line 162

    Also declared: ComparatorChallenges/EditApproximation.lean:162 (same declaration text).

37. def OAI.EditApproximation.dyadicSeedPassCount line 167

    Also declared: ComparatorChallenges/EditApproximation.lean:167 (same declaration text).

38. def OAI.EditApproximation.dyadicSeedExponent line 169

    Also declared: ComparatorChallenges/EditApproximation.lean:169 (same declaration text).

39. def OAI.EditApproximation.memberByWithWork line 171

    Also declared: ComparatorChallenges/EditApproximation.lean:171 (same declaration text).

40. inductive OAI.EditApproximation.BinaryMemo line 178

    Also declared: ComparatorChallenges/EditApproximation.lean:178 (same declaration text).

41. def OAI.EditApproximation.binaryMemoKey line 182

    Also declared: ComparatorChallenges/EditApproximation.lean:182 (same declaration text).

42. inductive OAI.EditApproximation.FiniteQuery line 186

    Also declared: ComparatorChallenges/EditApproximation.lean:186 (same declaration text).

43. def OAI.EditApproximation.finiteAnswerTable line 190

    Also declared: ComparatorChallenges/EditApproximation.lean:190 (same declaration text).

44. def OAI.EditApproximation.queryFinRange line 195

    Also declared: ComparatorChallenges/EditApproximation.lean:195 (same declaration text).

45. def OAI.EditApproximation.queryInsertWithWork line 198

    Also declared: ComparatorChallenges/EditApproximation.lean:198 (same declaration text).

46. def OAI.EditApproximation.integerSymbolCode line 207

    Also declared: ComparatorChallenges/EditApproximation.lean:207 (same declaration text).

47. inductive OAI.EditApproximation.PositionCounts line 211

    Also declared: ComparatorChallenges/EditApproximation.lean:211 (same declaration text).

48. def OAI.EditApproximation.integerMagnitude line 215

    Also declared: ComparatorChallenges/EditApproximation.lean:215 (same declaration text).

49. def OAI.EditApproximation.integerInputPositionBits line 219

    Also declared: ComparatorChallenges/EditApproximation.lean:219 (same declaration text).

50. def OAI.EditApproximation.dpLength line 221

    Also declared: ComparatorChallenges/EditApproximation.lean:221 (same declaration text).

51. def OAI.EditApproximation.dpDrop line 225

    Also declared: ComparatorChallenges/EditApproximation.lean:225 (same declaration text).

52. def OAI.EditApproximation.dpTake line 230

    Also declared: ComparatorChallenges/EditApproximation.lean:230 (same declaration text).

53. def OAI.EditApproximation.dpGetD line 235

    Also declared: ComparatorChallenges/EditApproximation.lean:235 (same declaration text).

54. def OAI.EditApproximation.dpMember line 240

    Also declared: ComparatorChallenges/EditApproximation.lean:240 (same declaration text).

55. def OAI.EditApproximation.dpMinimum line 245

    Also declared: ComparatorChallenges/EditApproximation.lean:245 (same declaration text).

56. def OAI.EditApproximation.integerMagnitudeWithWork line 249

    Also declared: ComparatorChallenges/EditApproximation.lean:249 (same declaration text).

57. def OAI.EditApproximation.inputBitLengthWithWork line 255

    Also declared: ComparatorChallenges/EditApproximation.lean:255 (same declaration text).

58. def OAI.EditApproximation.naturalPairWithWork line 262

    Also declared: ComparatorChallenges/EditApproximation.lean:262 (same declaration text).

59. def OAI.EditApproximation.inspectBitPrefix line 265

    Also declared: ComparatorChallenges/EditApproximation.lean:265 (same declaration text).

60. def OAI.EditApproximation.memoRequestCells line 273

    Also declared: ComparatorChallenges/EditApproximation.lean:273 (same declaration text).

61. def OAI.EditApproximation.arithmeticMapAllocation line 275

    Also declared: ComparatorChallenges/EditApproximation.lean:275 (same declaration text).

62. def OAI.EditApproximation.arithmeticFlatMapAllocation line 279

    Also declared: ComparatorChallenges/EditApproximation.lean:279 (same declaration text).

63. def OAI.EditApproximation.filterAllocation line 284

    Also declared: ComparatorChallenges/EditApproximation.lean:284 (same declaration text).

64. def OAI.EditApproximation.filterMapAllocation line 288

    Also declared: ComparatorChallenges/EditApproximation.lean:288 (same declaration text).

65. def OAI.EditApproximation.naturalEqualAllocation line 293

    Also declared: ComparatorChallenges/EditApproximation.lean:293 (same declaration text).

66. def OAI.EditApproximation.memberByAllocation line 295

    Also declared: ComparatorChallenges/EditApproximation.lean:295 (same declaration text).

67. def OAI.EditApproximation.naturalWordLEAllocation line 299

    Also declared: ComparatorChallenges/EditApproximation.lean:299 (same declaration text).

68. def OAI.EditApproximation.vectorMapAllocation line 301

    Also declared: ComparatorChallenges/EditApproximation.lean:301 (same declaration text).

69. def OAI.EditApproximation.allAllocation line 304

    Also declared: ComparatorChallenges/EditApproximation.lean:304 (same declaration text).

70. def OAI.EditApproximation.queryInsertAllocation line 308

    Also declared: ComparatorChallenges/EditApproximation.lean:308 (same declaration text).

71. def OAI.EditApproximation.wordLEAllocation line 313

    Also declared: ComparatorChallenges/EditApproximation.lean:313 (same declaration text).

72. def OAI.EditApproximation.indexedLeafAllocation line 315

    Also declared: ComparatorChallenges/EditApproximation.lean:315 (same declaration text).

73. def OAI.EditApproximation.storedNaturalBits line 320

    Also declared: ComparatorChallenges/EditApproximation.lean:320 (same declaration text).

74. def OAI.EditApproximation.coarseHistoryKeyCost line 323

    Also declared: ComparatorChallenges/EditApproximation.lean:323 (same declaration text).

75. def OAI.EditApproximation.bitAddNilLeftWithWork line 327

    Also declared: ComparatorChallenges/EditApproximation.lean:327 (same declaration text).

76. def OAI.EditApproximation.bitCompareNilLeftWithWork line 335

    Also declared: ComparatorChallenges/EditApproximation.lean:335 (same declaration text).

77. def OAI.EditApproximation.bitSubtractNilLeftWithWork line 343

    Also declared: ComparatorChallenges/EditApproximation.lean:343 (same declaration text).

78. structure OAI.EditApproximation.BinaryFraction line 351

    Also declared: ComparatorChallenges/EditApproximation.lean:351 (same declaration text).

79. def OAI.EditApproximation.rationalActionValue line 356

    Also declared: ComparatorChallenges/EditApproximation.lean:356 (same declaration text).

80. def OAI.EditApproximation.inputHeight line 361

    Also declared: ComparatorChallenges/EditApproximation.lean:361 (same declaration text).

81. def OAI.EditApproximation.smallLogExponent line 363

    Also declared: ComparatorChallenges/EditApproximation.lean:363 (same declaration text).

82. def OAI.EditApproximation.rationalParameters line 365

    Also declared: ComparatorChallenges/EditApproximation.lean:365 (same declaration text).

83. def OAI.EditApproximation.materializedAssignmentsWithWork line 371

    Also declared: ComparatorChallenges/EditApproximation.lean:371 (same declaration text).

84. def OAI.EditApproximation.dyadicScalesWithWork line 381

    Also declared: ComparatorChallenges/EditApproximation.lean:381 (same declaration text).

85. def OAI.EditApproximation.dedupByWithWork line 388

    Also declared: ComparatorChallenges/EditApproximation.lean:388 (same declaration text).

86. def OAI.EditApproximation.queryEraseLoopWithWork line 395

    Also declared: ComparatorChallenges/EditApproximation.lean:395 (same declaration text).

87. structure OAI.EditApproximation.RecursiveMemoResult line 403

    Also declared: ComparatorChallenges/EditApproximation.lean:403 (same declaration text).

88. def OAI.EditApproximation.querySortWithWork line 410

    Also declared: ComparatorChallenges/EditApproximation.lean:410 (same declaration text).

89. def OAI.EditApproximation.encodeIntegerSymbolsWithWork line 417

    Also declared: ComparatorChallenges/EditApproximation.lean:417 (same declaration text).

90. def OAI.EditApproximation.integerInputSymbolBits line 423

    Also declared: ComparatorChallenges/EditApproximation.lean:423 (same declaration text).

91. def OAI.EditApproximation.dpSingleton line 426

    Also declared: ComparatorChallenges/EditApproximation.lean:426 (same declaration text).

92. def OAI.EditApproximation.dpCandidateAllocation line 432

    Also declared: ComparatorChallenges/EditApproximation.lean:432 (same declaration text).

93. def OAI.EditApproximation.integerInputInspectionWithWork line 435

    Also declared: ComparatorChallenges/EditApproximation.lean:435 (same declaration text).

94. def OAI.EditApproximation.bitAddNilLeftAllocation line 444

    Also declared: ComparatorChallenges/EditApproximation.lean:444 (same declaration text).

95. def OAI.EditApproximation.bitSubtractNilLeftAllocation line 450

    Also declared: ComparatorChallenges/EditApproximation.lean:450 (same declaration text).

96. def OAI.EditApproximation.trimBitWordAllocation line 456

    Also declared: ComparatorChallenges/EditApproximation.lean:456 (same declaration text).

97. def OAI.EditApproximation.dedupByAllocation line 461

    Also declared: ComparatorChallenges/EditApproximation.lean:461 (same declaration text).

98. def OAI.EditApproximation.dyadicScalesAllocation line 467

    Also declared: ComparatorChallenges/EditApproximation.lean:467 (same declaration text).

99. def OAI.EditApproximation.queryRangeValidAllocation line 470

    Also declared: ComparatorChallenges/EditApproximation.lean:470 (same declaration text).

100. def OAI.EditApproximation.queryEraseLoopAllocation line 473

     Also declared: ComparatorChallenges/EditApproximation.lean:473 (same declaration text).

101. def OAI.EditApproximation.queryEncodedLEAllocation line 481

     Also declared: ComparatorChallenges/EditApproximation.lean:481 (same declaration text).

102. def OAI.EditApproximation.bitAddWithWork line 485

     Also declared: ComparatorChallenges/EditApproximation.lean:485 (same declaration text).

103. def OAI.EditApproximation.bitCompareWithWork line 498

     Also declared: ComparatorChallenges/EditApproximation.lean:498 (same declaration text).

104. def OAI.EditApproximation.bitSubtractWithWork line 511

     Also declared: ComparatorChallenges/EditApproximation.lean:511 (same declaration text).

105. def OAI.EditApproximation.rationalBellman line 524

     Also declared: ComparatorChallenges/EditApproximation.lean:524 (same declaration text).

106. def OAI.EditApproximation.inputSmallLog line 529

     Also declared: ComparatorChallenges/EditApproximation.lean:529 (same declaration text).

107. structure OAI.EditApproximation.BinaryBellmanAction line 531

     Also declared: ComparatorChallenges/EditApproximation.lean:531 (same declaration text).

108. def OAI.EditApproximation.queryEraseWithWork line 536

     Also declared: ComparatorChallenges/EditApproximation.lean:536 (same declaration text).

109. inductive OAI.EditApproximation.BitQuery line 539

     Also declared: ComparatorChallenges/EditApproximation.lean:539 (same declaration text).

110. def OAI.EditApproximation.dpCandidate line 544

     Also declared: ComparatorChallenges/EditApproximation.lean:544 (same declaration text).

111. def OAI.EditApproximation.dpCellAllocation line 552

     Also declared: ComparatorChallenges/EditApproximation.lean:552 (same declaration text).

112. def OAI.EditApproximation.initialThresholdQ line 557

     Also declared: ComparatorChallenges/EditApproximation.lean:557 (same declaration text).

113. def OAI.EditApproximation.initialLambda line 559

     Also declared: ComparatorChallenges/EditApproximation.lean:559 (same declaration text).

114. structure OAI.EditApproximation.BitRecursiveMemoResult line 561

     Also declared: ComparatorChallenges/EditApproximation.lean:561 (same declaration text).

115. structure OAI.EditApproximation.RefinementParameterWords line 569

     Also declared: ComparatorChallenges/EditApproximation.lean:569 (same declaration text).

116. def OAI.EditApproximation.inspectAccuracyWithWork line 576

     Also declared: ComparatorChallenges/EditApproximation.lean:576 (same declaration text).

117. def OAI.EditApproximation.bitAddAllocation line 585

     Also declared: ComparatorChallenges/EditApproximation.lean:585 (same declaration text).

118. def OAI.EditApproximation.bitSubtractAllocation line 594

     Also declared: ComparatorChallenges/EditApproximation.lean:594 (same declaration text).

119. def OAI.EditApproximation.materializedAssignmentsAllocation line 603

     Also declared: ComparatorChallenges/EditApproximation.lean:603 (same declaration text).

120. def OAI.EditApproximation.queryEraseAllocation line 614

     Also declared: ComparatorChallenges/EditApproximation.lean:614 (same declaration text).

121. def OAI.EditApproximation.querySortAllocation line 617

     Also declared: ComparatorChallenges/EditApproximation.lean:617 (same declaration text).

122. def OAI.EditApproximation.binaryNaturalAddWithWork line 623

     Also declared: ComparatorChallenges/EditApproximation.lean:623 (same declaration text).

123. def OAI.EditApproximation.bitMulWithWork line 626

     Also declared: ComparatorChallenges/EditApproximation.lean:626 (same declaration text).

124. def OAI.EditApproximation.binaryNaturalCompareWithWork line 635

     Also declared: ComparatorChallenges/EditApproximation.lean:635 (same declaration text).

125. def OAI.EditApproximation.binaryNaturalSubtractWithWork line 637

     Also declared: ComparatorChallenges/EditApproximation.lean:637 (same declaration text).

126. def OAI.EditApproximation.integerParameters line 641

     Also declared: ComparatorChallenges/EditApproximation.lean:641 (same declaration text).

127. def OAI.EditApproximation.bitDivModWithWork line 649

     Also declared: ComparatorChallenges/EditApproximation.lean:649 (same declaration text).

128. def OAI.EditApproximation.wordLEWithWork line 661

     Also declared: ComparatorChallenges/EditApproximation.lean:661 (same declaration text).

129. def OAI.EditApproximation.computedSeedInitialExponent line 665

     Also declared: ComparatorChallenges/EditApproximation.lean:665 (same declaration text).

130. def OAI.EditApproximation.queryOrderedInputsWithWork line 668

     Also declared: ComparatorChallenges/EditApproximation.lean:668 (same declaration text).

131. def OAI.EditApproximation.queryActionInputsWithWork line 674

     Also declared: ComparatorChallenges/EditApproximation.lean:674 (same declaration text).

132. def OAI.EditApproximation.largeAccuracyInput line 680

     Also declared: ComparatorChallenges/EditApproximation.lean:680 (same declaration text).

133. def OAI.EditApproximation.dpCell line 683

     Also declared: ComparatorChallenges/EditApproximation.lean:683 (same declaration text).

134. def OAI.EditApproximation.suffixDPAllocation line 691

     Also declared: ComparatorChallenges/EditApproximation.lean:691 (same declaration text).

135. def OAI.EditApproximation.binaryNaturalAddAllocation line 697

     Also declared: ComparatorChallenges/EditApproximation.lean:697 (same declaration text).

136. def OAI.EditApproximation.queryOrderedInputsAllocation line 699

     Also declared: ComparatorChallenges/EditApproximation.lean:699 (same declaration text).

137. def OAI.EditApproximation.queryActionInputsAllocation line 704

     Also declared: ComparatorChallenges/EditApproximation.lean:704 (same declaration text).

138. def OAI.EditApproximation.binaryNaturalMulWithWork line 710

     Also declared: ComparatorChallenges/EditApproximation.lean:710 (same declaration text).

139. def OAI.EditApproximation.binaryNaturalDivModWithWork line 712

     Also declared: ComparatorChallenges/EditApproximation.lean:712 (same declaration text).

140. def OAI.EditApproximation.bitCeilDivWithWork line 715

     Also declared: ComparatorChallenges/EditApproximation.lean:715 (same declaration text).

141. def OAI.EditApproximation.wordMinWithWork line 723

     Also declared: ComparatorChallenges/EditApproximation.lean:723 (same declaration text).

142. def OAI.EditApproximation.wordInsertWithWork line 727

     Also declared: ComparatorChallenges/EditApproximation.lean:727 (same declaration text).

143. def OAI.EditApproximation.saturatingSubtractWithWork line 735

     Also declared: ComparatorChallenges/EditApproximation.lean:735 (same declaration text).

144. def OAI.EditApproximation.computedSeedPassCount line 741

     Also declared: ComparatorChallenges/EditApproximation.lean:741 (same declaration text).

145. def OAI.EditApproximation.bitPowerWithWork line 744

     Also declared: ComparatorChallenges/EditApproximation.lean:744 (same declaration text).

146. def OAI.EditApproximation.queryEncodedLEWithWork line 752

     Also declared: ComparatorChallenges/EditApproximation.lean:752 (same declaration text).

147. instance OAI.EditApproximation.largeAccuracyInput_decidable line 758

     Also declared: ComparatorChallenges/EditApproximation.lean:758 (same declaration text).

148. def OAI.EditApproximation.chargedSuffixDP line 761

     Also declared: ComparatorChallenges/EditApproximation.lean:761 (same declaration text).

149. def OAI.EditApproximation.computedCoarseDepth line 771

     Also declared: ComparatorChallenges/EditApproximation.lean:771 (same declaration text).

150. def OAI.EditApproximation.queryRangeValidWithWork line 773

     Also declared: ComparatorChallenges/EditApproximation.lean:773 (same declaration text).

151. def OAI.EditApproximation.coarsePaddedReadWithWork line 778

     Also declared: ComparatorChallenges/EditApproximation.lean:778 (same declaration text).

152. def OAI.EditApproximation.coarseRangeCopyWithWork line 784

     Also declared: ComparatorChallenges/EditApproximation.lean:784 (same declaration text).

153. def OAI.EditApproximation.bitMulAllocation line 791

     Also declared: ComparatorChallenges/EditApproximation.lean:791 (same declaration text).

154. def OAI.EditApproximation.bitDivModAllocation line 797

     Also declared: ComparatorChallenges/EditApproximation.lean:797 (same declaration text).

155. def OAI.EditApproximation.saturatingSubtractAllocation line 805

     Also declared: ComparatorChallenges/EditApproximation.lean:805 (same declaration text).

156. def OAI.EditApproximation.makeStateAllocation line 809

     Also declared: ComparatorChallenges/EditApproximation.lean:809 (same declaration text).

157. def OAI.EditApproximation.translatedEndpointAllocation line 813

     Also declared: ComparatorChallenges/EditApproximation.lean:813 (same declaration text).

158. def OAI.EditApproximation.wordInsertAllocation line 817

     Also declared: ComparatorChallenges/EditApproximation.lean:817 (same declaration text).

159. def OAI.EditApproximation.wordSortWithWork line 822

     Also declared: ComparatorChallenges/EditApproximation.lean:822 (same declaration text).

160. def OAI.EditApproximation.binaryGridRoundWithWork line 829

     Also declared: ComparatorChallenges/EditApproximation.lean:829 (same declaration text).

161. def OAI.EditApproximation.gridPointsWithWork line 834

     Also declared: ComparatorChallenges/EditApproximation.lean:834 (same declaration text).

162. def OAI.EditApproximation.seedGridSpacingWithWork line 846

     Also declared: ComparatorChallenges/EditApproximation.lean:846 (same declaration text).

163. def OAI.EditApproximation.balancedCutWithWork line 851

     Also declared: ComparatorChallenges/EditApproximation.lean:851 (same declaration text).

164. def OAI.EditApproximation.triangularMassWithWork line 857

     Also declared: ComparatorChallenges/EditApproximation.lean:857 (same declaration text).

165. def OAI.EditApproximation.refinementBaseWithWork line 863

     Also declared: ComparatorChallenges/EditApproximation.lean:863 (same declaration text).

166. def OAI.EditApproximation.queryPairWithWork line 869

     Also declared: ComparatorChallenges/EditApproximation.lean:869 (same declaration text).

167. def OAI.EditApproximation.queryCellValidWithWork line 881

     Also declared: ComparatorChallenges/EditApproximation.lean:881 (same declaration text).

168. def OAI.EditApproximation.queryFinOfNatWithWork line 887

     Also declared: ComparatorChallenges/EditApproximation.lean:887 (same declaration text).

169. def OAI.EditApproximation.coarseDenominatorWithWork line 1064

     Also declared: ComparatorChallenges/EditApproximation.lean:1064 (same declaration text).

170. def OAI.EditApproximation.coarseFramedReadWithWork line 1075

     Also declared: ComparatorChallenges/EditApproximation.lean:1075 (same declaration text).

171. def OAI.EditApproximation.coarseDescriptorWithWork line 1087

     Also declared: ComparatorChallenges/EditApproximation.lean:1087 (same declaration text).

172. def OAI.EditApproximation.coarseChildOffsetWithWork line 1094

     Also declared: ComparatorChallenges/EditApproximation.lean:1094 (same declaration text).

173. def OAI.EditApproximation.coarseInputGuardWithWork line 1099

     Also declared: ComparatorChallenges/EditApproximation.lean:1099 (same declaration text).

174. def OAI.EditApproximation.bitPowerAllocation line 1106

     Also declared: ComparatorChallenges/EditApproximation.lean:1106 (same declaration text).

175. def OAI.EditApproximation.bitCeilDivAllocation line 1113

     Also declared: ComparatorChallenges/EditApproximation.lean:1113 (same declaration text).

176. def OAI.EditApproximation.binaryNaturalMulAllocation line 1119

     Also declared: ComparatorChallenges/EditApproximation.lean:1119 (same declaration text).

177. def OAI.EditApproximation.binaryNaturalDivAllocation line 1121

     Also declared: ComparatorChallenges/EditApproximation.lean:1121 (same declaration text).

178. def OAI.EditApproximation.triangularMassAllocation line 1123

     Also declared: ComparatorChallenges/EditApproximation.lean:1123 (same declaration text).

179. def OAI.EditApproximation.binaryIntervalRoundWithWork line 1130

     Also declared: ComparatorChallenges/EditApproximation.lean:1130 (same declaration text).

180. def OAI.EditApproximation.computedQueryBase line 1135

     Also declared: ComparatorChallenges/EditApproximation.lean:1135 (same declaration text).

181. def OAI.EditApproximation.coarsePreparedSlicesWithWork line 1138

     Also declared: ComparatorChallenges/EditApproximation.lean:1138 (same declaration text).

182. def OAI.EditApproximation.gridPointsAllocation line 1146

     Also declared: ComparatorChallenges/EditApproximation.lean:1146 (same declaration text).

183. def OAI.EditApproximation.balancedCutAllocation line 1157

     Also declared: ComparatorChallenges/EditApproximation.lean:1157 (same declaration text).

184. def OAI.EditApproximation.seedGridSpacingAllocation line 1163

     Also declared: ComparatorChallenges/EditApproximation.lean:1163 (same declaration text).

185. def OAI.EditApproximation.queryCellValidAllocation line 1166

     Also declared: ComparatorChallenges/EditApproximation.lean:1166 (same declaration text).

186. def OAI.EditApproximation.queryPairAllocation line 1171

     Also declared: ComparatorChallenges/EditApproximation.lean:1171 (same declaration text).

187. def OAI.EditApproximation.binaryGridRoundAllocation line 1180

     Also declared: ComparatorChallenges/EditApproximation.lean:1180 (same declaration text).

188. def OAI.EditApproximation.wordSortAllocation line 1184

     Also declared: ComparatorChallenges/EditApproximation.lean:1184 (same declaration text).

189. def OAI.EditApproximation.reduceOnlineIntegerAllocation line 1189

     Also declared: ComparatorChallenges/EditApproximation.lean:1189 (same declaration text).

190. def OAI.EditApproximation.coarsePreparedInputStorage line 1193

     Also declared: ComparatorChallenges/EditApproximation.lean:1193 (same declaration text).

191. def OAI.EditApproximation.optimizerTriangularMass line 1208

     Also declared: ComparatorChallenges/EditApproximation.lean:1208 (same declaration text).

192. def OAI.EditApproximation.rationalLogApproximation line 1210

     Also declared: ComparatorChallenges/EditApproximation.lean:1210 (same declaration text).

193. def OAI.EditApproximation.rationalLinearizationMaximizer line 1213

     Also declared: ComparatorChallenges/EditApproximation.lean:1213 (same declaration text).

194. def OAI.EditApproximation.bandCoordinates line 1217

     Also declared: ComparatorChallenges/EditApproximation.lean:1217 (same declaration text).

195. def OAI.EditApproximation.actionVector line 1221

     Also declared: ComparatorChallenges/EditApproximation.lean:1221 (same declaration text).

196. def OAI.EditApproximation.rationalOptimisticHistory line 1225

     Also declared: ComparatorChallenges/EditApproximation.lean:1225 (same declaration text).

197. def OAI.EditApproximation.rejectionBitCount line 1229

     Also declared: ComparatorChallenges/EditApproximation.lean:1229 (same declaration text).

198. def OAI.EditApproximation.vectorMapWithWork line 1231

     Also declared: ComparatorChallenges/EditApproximation.lean:1231 (same declaration text).

199. def OAI.EditApproximation.TreeLayer line 1235

     Also declared: ComparatorChallenges/EditApproximation.lean:1235 (same declaration text).

200. def OAI.EditApproximation.intervalTreeDepth line 1239

     Also declared: ComparatorChallenges/EditApproximation.lean:1239 (same declaration text).

201. def OAI.EditApproximation.rationalMaximum line 1241

     Also declared: ComparatorChallenges/EditApproximation.lean:1241 (same declaration text).

202. def OAI.EditApproximation.rationalDyadicCeiling line 1245

     Also declared: ComparatorChallenges/EditApproximation.lean:1245 (same declaration text).

203. def OAI.EditApproximation.listedBandCoordinates line 1247

     Also declared: ComparatorChallenges/EditApproximation.lean:1247 (same declaration text).

204. def OAI.EditApproximation.childGain line 1251

     Also declared: ComparatorChallenges/EditApproximation.lean:1251 (same declaration text).

205. def OAI.EditApproximation.childDecrement line 1254

     Also declared: ComparatorChallenges/EditApproximation.lean:1254 (same declaration text).

206. def OAI.EditApproximation.naturalEqualWithWork line 1257

     Also declared: ComparatorChallenges/EditApproximation.lean:1257 (same declaration text).

207. def OAI.EditApproximation.translatedEndpointWithWork line 1261

     Also declared: ComparatorChallenges/EditApproximation.lean:1261 (same declaration text).

208. def OAI.EditApproximation.rationalOnlineMinimum line 1266

     Also declared: ComparatorChallenges/EditApproximation.lean:1266 (same declaration text).

209. def OAI.EditApproximation.dyadicQueryWindow line 1270

     Also declared: ComparatorChallenges/EditApproximation.lean:1270 (same declaration text).

210. def OAI.EditApproximation.actionCurrentInputCover line 1273

     Also declared: ComparatorChallenges/EditApproximation.lean:1273 (same declaration text).

211. def OAI.EditApproximation.boundedOnlineInteger line 1278

     Also declared: ComparatorChallenges/EditApproximation.lean:1278 (same declaration text).

212. def OAI.EditApproximation.orderedInputs line 1281

     Also declared: ComparatorChallenges/EditApproximation.lean:1281 (same declaration text).

213. def OAI.EditApproximation.CoarseThresholdDraws line 1286

     Also declared: ComparatorChallenges/EditApproximation.lean:1286 (same declaration text).

214. def OAI.EditApproximation.coarseThresholdContribution line 1290

     Also declared: ComparatorChallenges/EditApproximation.lean:1290 (same declaration text).

215. def OAI.EditApproximation.coarseChildThreshold line 1293

     Also declared: ComparatorChallenges/EditApproximation.lean:1293 (same declaration text).

216. def OAI.EditApproximation.coarseCommonDenominator line 1296

     Also declared: ComparatorChallenges/EditApproximation.lean:1296 (same declaration text).

217. def OAI.EditApproximation.rationalSmoothedGradient line 1299

     Also declared: ComparatorChallenges/EditApproximation.lean:1299 (same declaration text).

218. def OAI.EditApproximation.rationalOnlineLinear line 1302

     Also declared: ComparatorChallenges/EditApproximation.lean:1302 (same declaration text).

219. def OAI.EditApproximation.triangularChoice line 1306

     Also declared: ComparatorChallenges/EditApproximation.lean:1306 (same declaration text).

220. instance OAI.EditApproximation.treeLayerFintype line 1313

     Also declared: ComparatorChallenges/EditApproximation.lean:1313 (same declaration text).

221. abbrev OAI.EditApproximation.PhysicalNode line 1319

     Also declared: ComparatorChallenges/EditApproximation.lean:1319 (same declaration text).

222. def OAI.EditApproximation.finiteRationalOptimizer line 1321

     Also declared: ComparatorChallenges/EditApproximation.lean:1321 (same declaration text).

223. instance OAI.EditApproximation.physicalNodeFintype line 1330

     Also declared: ComparatorChallenges/EditApproximation.lean:1330 (same declaration text).

224. abbrev OAI.EditApproximation.PhysicalInternalNode line 1332

     Also declared: ComparatorChallenges/EditApproximation.lean:1332 (same declaration text).

225. def OAI.EditApproximation.finiteOptimizerAction line 1334

     Also declared: ComparatorChallenges/EditApproximation.lean:1334 (same declaration text).

226. def OAI.EditApproximation.finiteOptimizerActionDraw line 1343

     Also declared: ComparatorChallenges/EditApproximation.lean:1343 (same declaration text).

227. def OAI.EditApproximation.BinaryFraction.width line 1357

     Also declared: ComparatorChallenges/EditApproximation.lean:1357 (same declaration text).

228. def OAI.EditApproximation.BinaryFraction.denominatorInteger line 1359

     Also declared: ComparatorChallenges/EditApproximation.lean:1359 (same declaration text).

229. def OAI.EditApproximation.BinaryFraction.zero line 1361

     Also declared: ComparatorChallenges/EditApproximation.lean:1361 (same declaration text).

230. def OAI.EditApproximation.BinaryFraction.canonicalizeWithWork line 1363

     Also declared: ComparatorChallenges/EditApproximation.lean:1363 (same declaration text).

231. def OAI.EditApproximation.BinaryFraction.inversePowerTwo line 1381

     Also declared: ComparatorChallenges/EditApproximation.lean:1381 (same declaration text).

232. def OAI.EditApproximation.BinaryFraction.doubleFraction line 1393

     Also declared: ComparatorChallenges/EditApproximation.lean:1393 (same declaration text).

233. def OAI.EditApproximation.BinaryFraction.absolute line 1396

     Also declared: ComparatorChallenges/EditApproximation.lean:1396 (same declaration text).

234. def OAI.EditApproximation.BinaryFraction.naturalCeilingWithWork line 1399

     Also declared: ComparatorChallenges/EditApproximation.lean:1399 (same declaration text).

235. def OAI.EditApproximation.BinaryFraction.ofNaturalWord line 1405

     Also declared: ComparatorChallenges/EditApproximation.lean:1405 (same declaration text).

236. def OAI.EditApproximation.BinaryFraction.naturalFloorWithWork line 1408

     Also declared: ComparatorChallenges/EditApproximation.lean:1408 (same declaration text).

237. def OAI.EditApproximation.BinaryFraction.queryDataReadBudget line 1413

     Also declared: ComparatorChallenges/EditApproximation.lean:1413 (same declaration text).

238. def OAI.EditApproximation.BinaryFraction.onlineParametersWithWork line 1416

     Also declared: ComparatorChallenges/EditApproximation.lean:1416 (same declaration text).

239. def OAI.EditApproximation.BinaryFraction.refinementDecrementWithWork line 1477

     Also declared: ComparatorChallenges/EditApproximation.lean:1477 (same declaration text).

240. abbrev OAI.EditApproximation.BinaryFraction.CoarseBinaryArray line 1534

     Also declared: ComparatorChallenges/EditApproximation.lean:1534 (same declaration text).

241. def OAI.EditApproximation.BinaryFraction.coarseRootDenominator line 1536

     Also declared: ComparatorChallenges/EditApproximation.lean:1536 (same declaration text).

242. def OAI.EditApproximation.BinaryFraction.naturalListEqualWithWork line 1539

     Also declared: ComparatorChallenges/EditApproximation.lean:1539 (same declaration text).

243. def OAI.EditApproximation.BinaryFraction.canonicalizeAllocation line 1549

     Also declared: ComparatorChallenges/EditApproximation.lean:1549 (same declaration text).

244. def OAI.EditApproximation.BinaryFraction.invAllocation line 1552

     Also declared: ComparatorChallenges/EditApproximation.lean:1552 (same declaration text).

245. def OAI.EditApproximation.BinaryFraction.naturalCeilingAllocation line 1555

     Also declared: ComparatorChallenges/EditApproximation.lean:1555 (same declaration text).

246. def OAI.EditApproximation.BinaryFraction.gatheredLookupAllocation line 1558

     Also declared: ComparatorChallenges/EditApproximation.lean:1558 (same declaration text).

247. def OAI.EditApproximation.BinaryFraction.naturalFloorAllocation line 1565

     Also declared: ComparatorChallenges/EditApproximation.lean:1565 (same declaration text).

248. def OAI.EditApproximation.BinaryFraction.signedPowerTwoAllocation line 1568

     Also declared: ComparatorChallenges/EditApproximation.lean:1568 (same declaration text).

249. def OAI.EditApproximation.BinaryFraction.invWithWork line 1571

     Also declared: ComparatorChallenges/EditApproximation.lean:1571 (same declaration text).

250. def OAI.EditApproximation.BinaryFraction.signedPowerTwoWithWork line 1611

     Also declared: ComparatorChallenges/EditApproximation.lean:1611 (same declaration text).

251. def OAI.EditApproximation.BinaryFraction.fixedDenominatorWithWork line 1616

     Also declared: ComparatorChallenges/EditApproximation.lean:1616 (same declaration text).

252. def OAI.EditApproximation.BinaryFraction.finalAnswerWithWork line 1624

     Also declared: ComparatorChallenges/EditApproximation.lean:1624 (same declaration text).

253. def OAI.EditApproximation.BinaryFraction.coarseGridNatWithWork line 1629

     Also declared: ComparatorChallenges/EditApproximation.lean:1629 (same declaration text).

254. def OAI.EditApproximation.BinaryFraction.coarseBinaryMapWithWork line 1636

     Also declared: ComparatorChallenges/EditApproximation.lean:1636 (same declaration text).

255. def OAI.EditApproximation.BinaryFraction.fixedDenominatorAllocation line 1643

     Also declared: ComparatorChallenges/EditApproximation.lean:1643 (same declaration text).

256. def OAI.EditApproximation.BinaryFraction.finalAnswerAllocation line 1651

     Also declared: ComparatorChallenges/EditApproximation.lean:1651 (same declaration text).

257. def OAI.EditApproximation.BinaryFraction.powerDenominatorWithWork line 1654

     Also declared: ComparatorChallenges/EditApproximation.lean:1654 (same declaration text).

258. def OAI.EditApproximation.BinaryFraction.powerDenominatorAllocation line 1713

     Also declared: ComparatorChallenges/EditApproximation.lean:1713 (same declaration text).

259. def OAI.EditApproximation.BinaryFraction.finishCachedWithWork line 1769

     Also declared: ComparatorChallenges/EditApproximation.lean:1769 (same declaration text).

260. def OAI.EditApproximation.BinaryFraction.finishCachedAllocation line 1774

     Also declared: ComparatorChallenges/EditApproximation.lean:1774 (same declaration text).

261. def OAI.EditApproximation.physicalChild line 1787

     Also declared: ComparatorChallenges/EditApproximation.lean:1787 (same declaration text).

262. instance OAI.EditApproximation.treeLayerDecidableEq line 1791

     Also declared: ComparatorChallenges/EditApproximation.lean:1791 (same declaration text).

263. def OAI.EditApproximation.treeLayerCode line 1797

     Also declared: ComparatorChallenges/EditApproximation.lean:1797 (same declaration text).

264. def OAI.EditApproximation.localOnlineMassBound line 1801

     Also declared: ComparatorChallenges/EditApproximation.lean:1801 (same declaration text).

265. def OAI.EditApproximation.treeLayerCodeWithWork line 1804

     Also declared: ComparatorChallenges/EditApproximation.lean:1804 (same declaration text).

266. def OAI.EditApproximation.queryNaturalIndexWithWork line 1809

     Also declared: ComparatorChallenges/EditApproximation.lean:1809 (same declaration text).

267. def OAI.EditApproximation.scheduledSeedWordWithWork line 1818

     Also declared: ComparatorChallenges/EditApproximation.lean:1818 (same declaration text).

268. def OAI.EditApproximation.coarseLetterMatchWithWork line 1822

     Also declared: ComparatorChallenges/EditApproximation.lean:1822 (same declaration text).

269. def OAI.EditApproximation.queryNaturalIndexAllocation line 1828

     Also declared: ComparatorChallenges/EditApproximation.lean:1828 (same declaration text).

270. def OAI.EditApproximation.physicalNodeCode line 1833

     Also declared: ComparatorChallenges/EditApproximation.lean:1833 (same declaration text).

271. def OAI.EditApproximation.queryScaleDispatchWithWork line 1836

     Also declared: ComparatorChallenges/EditApproximation.lean:1836 (same declaration text).

272. def OAI.EditApproximation.queryScaleDispatchAllocation line 1841

     Also declared: ComparatorChallenges/EditApproximation.lean:1841 (same declaration text).

273. def OAI.EditApproximation.queryScalePresentWithWork line 1845

     Also declared: ComparatorChallenges/EditApproximation.lean:1845 (same declaration text).

274. def OAI.EditApproximation.queryScalePresentAllocation line 1850

     Also declared: ComparatorChallenges/EditApproximation.lean:1850 (same declaration text).

275. def OAI.EditApproximation.physicalScaleIndex line 1862

     Also declared: ComparatorChallenges/EditApproximation.lean:1862 (same declaration text).

276. abbrev OAI.EditApproximation.PositiveDrawRange line 1866

     Also declared: ComparatorChallenges/EditApproximation.lean:1866 (same declaration text).

277. abbrev OAI.EditApproximation.PhysicalLocalGroupKey line 1868

     Also declared: ComparatorChallenges/EditApproximation.lean:1868 (same declaration text).

278. def OAI.EditApproximation.rejectionSuccessParameter line 1872

     Also declared: ComparatorChallenges/EditApproximation.lean:1872 (same declaration text).

279. def OAI.EditApproximation.scheduledSeedFactor line 1876

     Also declared: ComparatorChallenges/EditApproximation.lean:1876 (same declaration text).

280. def OAI.EditApproximation.scheduledSeedMultiplier line 1879

     Also declared: ComparatorChallenges/EditApproximation.lean:1879 (same declaration text).

281. instance OAI.EditApproximation.computedBranching_neZero line 1882

     Also declared: ComparatorChallenges/EditApproximation.lean:1882 (same declaration text).

282. instance OAI.EditApproximation.computedCoarseBranching_neZero line 1885

     Also declared: ComparatorChallenges/EditApproximation.lean:1885 (same declaration text).

283. instance OAI.EditApproximation.computedSourceTime_neZero line 1888

     Also declared: ComparatorChallenges/EditApproximation.lean:1888 (same declaration text).

284. abbrev OAI.EditApproximation.CommonRangeKey line 1891

     Also declared: ComparatorChallenges/EditApproximation.lean:1891 (same declaration text).

285. def OAI.EditApproximation.positiveDrawRangeOfLE line 1893

     Also declared: ComparatorChallenges/EditApproximation.lean:1893 (same declaration text).

286. instance OAI.EditApproximation.positiveDrawRange_nezero line 1896

     Also declared: ComparatorChallenges/EditApproximation.lean:1896 (same declaration text).

287. def OAI.EditApproximation.SignedBinary.value line 1908

     Also declared: ComparatorChallenges/EditApproximation.lean:1908 (same declaration text).

288. def OAI.EditApproximation.SignedBinary.ofInt line 1910

     Also declared: ComparatorChallenges/EditApproximation.lean:1910 (same declaration text).

289. def OAI.EditApproximation.SignedBinary.neg line 1912

     Also declared: ComparatorChallenges/EditApproximation.lean:1912 (same declaration text).

290. def OAI.EditApproximation.SignedBinary.addWithWork line 1914

     Also declared: ComparatorChallenges/EditApproximation.lean:1914 (same declaration text).

291. def OAI.EditApproximation.SignedBinary.mulWithWork line 1929

     Also declared: ComparatorChallenges/EditApproximation.lean:1929 (same declaration text).

292. def OAI.EditApproximation.SignedBinary.nonzeroWithWork line 1933

     Also declared: ComparatorChallenges/EditApproximation.lean:1933 (same declaration text).

293. def OAI.EditApproximation.SignedBinary.addAllocation line 1937

     Also declared: ComparatorChallenges/EditApproximation.lean:1937 (same declaration text).

294. def OAI.EditApproximation.SignedBinary.mulAllocation line 1944

     Also declared: ComparatorChallenges/EditApproximation.lean:1944 (same declaration text).

295. def OAI.EditApproximation.SignedBinary.ltWithWork line 1946

     Also declared: ComparatorChallenges/EditApproximation.lean:1946 (same declaration text).

296. def OAI.EditApproximation.BinaryFraction.value line 1970

     Also declared: ComparatorChallenges/EditApproximation.lean:1970 (same declaration text).

297. def OAI.EditApproximation.BinaryFraction.representation line 1972

     Also declared: ComparatorChallenges/EditApproximation.lean:1972 (same declaration text).

298. def OAI.EditApproximation.BinaryFraction.addWithWork line 1975

     Also declared: ComparatorChallenges/EditApproximation.lean:1975 (same declaration text).

299. def OAI.EditApproximation.BinaryFraction.mulWithWork line 2021

     Also declared: ComparatorChallenges/EditApproximation.lean:2021 (same declaration text).

300. def OAI.EditApproximation.BinaryFraction.neg line 2065

     Also declared: ComparatorChallenges/EditApproximation.lean:2065 (same declaration text).

301. def OAI.EditApproximation.BinaryFraction.ltWithWork line 2068

     Also declared: ComparatorChallenges/EditApproximation.lean:2068 (same declaration text).

302. def OAI.EditApproximation.BinaryFraction.nat line 2074

     Also declared: ComparatorChallenges/EditApproximation.lean:2074 (same declaration text).

303. def OAI.EditApproximation.BinaryFraction.coarseGridAddWithWork line 2077

     Also declared: ComparatorChallenges/EditApproximation.lean:2077 (same declaration text).

304. def OAI.EditApproximation.BinaryFraction.coarseReadShiftWithWork line 2083

     Also declared: ComparatorChallenges/EditApproximation.lean:2083 (same declaration text).

305. def OAI.EditApproximation.BinaryFraction.addAllocation line 2093

     Also declared: ComparatorChallenges/EditApproximation.lean:2093 (same declaration text).

306. def OAI.EditApproximation.BinaryFraction.mulAllocation line 2100

     Also declared: ComparatorChallenges/EditApproximation.lean:2100 (same declaration text).

307. def OAI.EditApproximation.BinaryFraction.ltAllocation line 2103

     Also declared: ComparatorChallenges/EditApproximation.lean:2103 (same declaration text).

308. def OAI.EditApproximation.BinaryFraction.canonicalAddWithWork line 2107

     Also declared: ComparatorChallenges/EditApproximation.lean:2107 (same declaration text).

309. def OAI.EditApproximation.BinaryFraction.canonicalMulWithWork line 2112

     Also declared: ComparatorChallenges/EditApproximation.lean:2112 (same declaration text).

310. def OAI.EditApproximation.BinaryFraction.one line 2117

     Also declared: ComparatorChallenges/EditApproximation.lean:2117 (same declaration text).

311. def OAI.EditApproximation.BinaryFraction.dyadicScanWithWork line 2119

     Also declared: ComparatorChallenges/EditApproximation.lean:2119 (same declaration text).

312. def OAI.EditApproximation.BinaryFraction.maxWithWork line 2128

     Also declared: ComparatorChallenges/EditApproximation.lean:2128 (same declaration text).

313. def OAI.EditApproximation.BinaryFraction.leWithWork line 2132

     Also declared: ComparatorChallenges/EditApproximation.lean:2132 (same declaration text).

314. def OAI.EditApproximation.BinaryFraction.minWithWork line 2136

     Also declared: ComparatorChallenges/EditApproximation.lean:2136 (same declaration text).

315. def OAI.EditApproximation.BinaryFraction.queryScaleAt line 2140

     Also declared: ComparatorChallenges/EditApproximation.lean:2140 (same declaration text).

316. def OAI.EditApproximation.BinaryFraction.gatheredWordLookupWithWork line 2144

     Also declared: ComparatorChallenges/EditApproximation.lean:2144 (same declaration text).

317. def OAI.EditApproximation.BinaryFraction.coarseGridZipAddWithWork line 2154

     Also declared: ComparatorChallenges/EditApproximation.lean:2154 (same declaration text).

318. def OAI.EditApproximation.BinaryFraction.coarseBinaryRead line 2161

     Also declared: ComparatorChallenges/EditApproximation.lean:2161 (same declaration text).

319. def OAI.EditApproximation.BinaryFraction.canonicalAddAllocation line 2166

     Also declared: ComparatorChallenges/EditApproximation.lean:2166 (same declaration text).

320. def OAI.EditApproximation.BinaryFraction.canonicalMulAllocation line 2169

     Also declared: ComparatorChallenges/EditApproximation.lean:2169 (same declaration text).

321. def OAI.EditApproximation.BinaryFraction.minAllocation line 2172

     Also declared: ComparatorChallenges/EditApproximation.lean:2172 (same declaration text).

322. def OAI.EditApproximation.BinaryFraction.maxAllocation line 2174

     Also declared: ComparatorChallenges/EditApproximation.lean:2174 (same declaration text).

323. def OAI.EditApproximation.BinaryFraction.leAllocation line 2176

     Also declared: ComparatorChallenges/EditApproximation.lean:2176 (same declaration text).

324. def OAI.EditApproximation.BinaryFraction.dyadicScanAllocation line 2178

     Also declared: ComparatorChallenges/EditApproximation.lean:2178 (same declaration text).

325. def OAI.EditApproximation.BinaryFraction.equalAllocation line 2184

     Also declared: ComparatorChallenges/EditApproximation.lean:2184 (same declaration text).

326. def OAI.EditApproximation.BinaryFraction.subWithWork line 2187

     Also declared: ComparatorChallenges/EditApproximation.lean:2187 (same declaration text).

327. def OAI.EditApproximation.BinaryFraction.divWithWork line 2191

     Also declared: ComparatorChallenges/EditApproximation.lean:2191 (same declaration text).

328. def OAI.EditApproximation.BinaryFraction.powWithWork line 2196

     Also declared: ComparatorChallenges/EditApproximation.lean:2196 (same declaration text).

329. def OAI.EditApproximation.BinaryFraction.dotListWithWork line 2203

     Also declared: ComparatorChallenges/EditApproximation.lean:2203 (same declaration text).

330. def OAI.EditApproximation.BinaryFraction.dyadicCeilingWithWork line 2211

     Also declared: ComparatorChallenges/EditApproximation.lean:2211 (same declaration text).

331. def OAI.EditApproximation.BinaryFraction.maximumWithWork line 2215

     Also declared: ComparatorChallenges/EditApproximation.lean:2215 (same declaration text).

332. def OAI.EditApproximation.BinaryFraction.minimumWithWork line 2222

     Also declared: ComparatorChallenges/EditApproximation.lean:2222 (same declaration text).

333. def OAI.EditApproximation.BinaryFraction.scaledCeilingWithWork line 2229

     Also declared: ComparatorChallenges/EditApproximation.lean:2229 (same declaration text).

334. def OAI.EditApproximation.BinaryFraction.coarseContributionWithWork line 2234

     Also declared: ComparatorChallenges/EditApproximation.lean:2234 (same declaration text).

335. def OAI.EditApproximation.BinaryFraction.coarseGridScanWithWork line 2243

     Also declared: ComparatorChallenges/EditApproximation.lean:2243 (same declaration text).

336. def OAI.EditApproximation.BinaryFraction.coarseGridZipMinimumWithWork line 2252

     Also declared: ComparatorChallenges/EditApproximation.lean:2252 (same declaration text).

337. def OAI.EditApproximation.BinaryFraction.coarseBinaryAddWithWork line 2259

     Also declared: ComparatorChallenges/EditApproximation.lean:2259 (same declaration text).

338. def OAI.EditApproximation.BinaryFraction.divAllocation line 2266

     Also declared: ComparatorChallenges/EditApproximation.lean:2266 (same declaration text).

339. def OAI.EditApproximation.BinaryFraction.subAllocation line 2269

     Also declared: ComparatorChallenges/EditApproximation.lean:2269 (same declaration text).

340. def OAI.EditApproximation.BinaryFraction.optimizerUpdateCellAllocation line 2271

     Also declared: ComparatorChallenges/EditApproximation.lean:2271 (same declaration text).

341. def OAI.EditApproximation.BinaryFraction.dyadicCeilingAllocation line 2277

     Also declared: ComparatorChallenges/EditApproximation.lean:2277 (same declaration text).

342. def OAI.EditApproximation.BinaryFraction.roundedSpacingAllocation line 2280

     Also declared: ComparatorChallenges/EditApproximation.lean:2280 (same declaration text).

343. def OAI.EditApproximation.BinaryFraction.scaledCeilingAllocation line 2285

     Also declared: ComparatorChallenges/EditApproximation.lean:2285 (same declaration text).

344. def OAI.EditApproximation.BinaryFraction.groupTermsAllocation line 2289

     Also declared: ComparatorChallenges/EditApproximation.lean:2289 (same declaration text).

345. def OAI.EditApproximation.BinaryFraction.logarithmPartialWithWork line 2293

     Also declared: ComparatorChallenges/EditApproximation.lean:2293 (same declaration text).

346. def OAI.EditApproximation.BinaryFraction.dotWithWork line 2302

     Also declared: ComparatorChallenges/EditApproximation.lean:2302 (same declaration text).

347. def OAI.EditApproximation.BinaryFraction.distanceWithWork line 2305

     Also declared: ComparatorChallenges/EditApproximation.lean:2305 (same declaration text).

348. def OAI.EditApproximation.BinaryFraction.affineErrorWithWork line 2309

     Also declared: ComparatorChallenges/EditApproximation.lean:2309 (same declaration text).

349. def OAI.EditApproximation.BinaryFraction.bandToleranceWithWork line 2317

     Also declared: ComparatorChallenges/EditApproximation.lean:2317 (same declaration text).

350. def OAI.EditApproximation.BinaryFraction.medianSeedWithWork line 2323

     Also declared: ComparatorChallenges/EditApproximation.lean:2323 (same declaration text).

351. def OAI.EditApproximation.BinaryFraction.groupSampleCountWithWork line 2330

     Also declared: ComparatorChallenges/EditApproximation.lean:2330 (same declaration text).

352. def OAI.EditApproximation.BinaryFraction.gainReadWithWork line 2339

     Also declared: ComparatorChallenges/EditApproximation.lean:2339 (same declaration text).

353. def OAI.EditApproximation.BinaryFraction.decrementReadWithWork line 2345

     Also declared: ComparatorChallenges/EditApproximation.lean:2345 (same declaration text).

354. def OAI.EditApproximation.BinaryFraction.scaledSeedWithWork line 2353

     Also declared: ComparatorChallenges/EditApproximation.lean:2353 (same declaration text).

355. def OAI.EditApproximation.BinaryFraction.initialScaleGuardWithWork line 2359

     Also declared: ComparatorChallenges/EditApproximation.lean:2359 (same declaration text).

356. def OAI.EditApproximation.BinaryFraction.initialCenterGuardWithWork line 2370

     Also declared: ComparatorChallenges/EditApproximation.lean:2370 (same declaration text).

357. def OAI.EditApproximation.BinaryFraction.cellCoordinatesWithWork line 2378

     Also declared: ComparatorChallenges/EditApproximation.lean:2378 (same declaration text).

358. def OAI.EditApproximation.BinaryFraction.cellGridPointsWithWork line 2391

     Also declared: ComparatorChallenges/EditApproximation.lean:2391 (same declaration text).

359. def OAI.EditApproximation.BinaryFraction.centerEligibilityWithWork line 2407

     Also declared: ComparatorChallenges/EditApproximation.lean:2407 (same declaration text).

360. def OAI.EditApproximation.BinaryFraction.refinementScaleGuardWithWork line 2417

     Also declared: ComparatorChallenges/EditApproximation.lean:2417 (same declaration text).

361. def OAI.EditApproximation.BinaryFraction.coarseDivideWithWork line 2427

     Also declared: ComparatorChallenges/EditApproximation.lean:2427 (same declaration text).

362. def OAI.EditApproximation.BinaryFraction.coarseGridLeftWithWork line 2432

     Also declared: ComparatorChallenges/EditApproximation.lean:2432 (same declaration text).

363. def OAI.EditApproximation.BinaryFraction.coarseMinimumWithWork line 2436

     Also declared: ComparatorChallenges/EditApproximation.lean:2436 (same declaration text).

364. def OAI.EditApproximation.BinaryFraction.powAllocation line 2440

     Also declared: ComparatorChallenges/EditApproximation.lean:2440 (same declaration text).

365. def OAI.EditApproximation.BinaryFraction.dotListAllocation line 2444

     Also declared: ComparatorChallenges/EditApproximation.lean:2444 (same declaration text).

366. def OAI.EditApproximation.BinaryFraction.minimumAllocation line 2450

     Also declared: ComparatorChallenges/EditApproximation.lean:2450 (same declaration text).

367. def OAI.EditApproximation.BinaryFraction.maximumAllocation line 2455

     Also declared: ComparatorChallenges/EditApproximation.lean:2455 (same declaration text).

368. def OAI.EditApproximation.BinaryFraction.distanceAllocation line 2460

     Also declared: ComparatorChallenges/EditApproximation.lean:2460 (same declaration text).

369. def OAI.EditApproximation.BinaryFraction.optimizerUpdateAllocation line 2462

     Also declared: ComparatorChallenges/EditApproximation.lean:2462 (same declaration text).

370. def OAI.EditApproximation.BinaryFraction.affineErrorAllocation line 2469

     Also declared: ComparatorChallenges/EditApproximation.lean:2469 (same declaration text).

371. def OAI.EditApproximation.BinaryFraction.bandToleranceAllocation line 2475

     Also declared: ComparatorChallenges/EditApproximation.lean:2475 (same declaration text).

372. def OAI.EditApproximation.BinaryFraction.initialScaleGuardAllocation line 2481

     Also declared: ComparatorChallenges/EditApproximation.lean:2481 (same declaration text).

373. def OAI.EditApproximation.BinaryFraction.initialCenterGuardAllocation line 2491

     Also declared: ComparatorChallenges/EditApproximation.lean:2491 (same declaration text).

374. def OAI.EditApproximation.BinaryFraction.scaledSeedAllocation line 2498

     Also declared: ComparatorChallenges/EditApproximation.lean:2498 (same declaration text).

375. def OAI.EditApproximation.BinaryFraction.centerEligibilityAllocation line 2504

     Also declared: ComparatorChallenges/EditApproximation.lean:2504 (same declaration text).

376. def OAI.EditApproximation.BinaryFraction.refinementScaleGuardAllocation line 2512

     Also declared: ComparatorChallenges/EditApproximation.lean:2512 (same declaration text).

377. def OAI.EditApproximation.BinaryFraction.cellCoordinatesAllocation line 2520

     Also declared: ComparatorChallenges/EditApproximation.lean:2520 (same declaration text).

378. def OAI.EditApproximation.BinaryFraction.cellGridPointsAllocation line 2536

     Also declared: ComparatorChallenges/EditApproximation.lean:2536 (same declaration text).

379. def OAI.EditApproximation.BinaryFraction.medianSeedAllocation line 2553

     Also declared: ComparatorChallenges/EditApproximation.lean:2553 (same declaration text).

380. def OAI.EditApproximation.BinaryFraction.groupSampleCountAllocation line 2560

     Also declared: ComparatorChallenges/EditApproximation.lean:2560 (same declaration text).

381. def OAI.EditApproximation.BinaryFraction.refinementUpdateAllocation line 2569

     Also declared: ComparatorChallenges/EditApproximation.lean:2569 (same declaration text).

382. def OAI.EditApproximation.BinaryFraction.coefficientAllocation line 2578

     Also declared: ComparatorChallenges/EditApproximation.lean:2578 (same declaration text).

383. def OAI.EditApproximation.BinaryFraction.gainReadAllocation line 2581

     Also declared: ComparatorChallenges/EditApproximation.lean:2581 (same declaration text).

384. def OAI.EditApproximation.BinaryFraction.decrementReadAllocation line 2586

     Also declared: ComparatorChallenges/EditApproximation.lean:2586 (same declaration text).

385. def OAI.EditApproximation.BinaryFraction.logarithmWithWork line 2592

     Also declared: ComparatorChallenges/EditApproximation.lean:2592 (same declaration text).

386. def OAI.EditApproximation.BinaryFraction.optimisticTermReadWithWork line 2600

     Also declared: ComparatorChallenges/EditApproximation.lean:2600 (same declaration text).

387. def OAI.EditApproximation.BinaryFraction.queryExponentsWithWork line 2609

     Also declared: ComparatorChallenges/EditApproximation.lean:2609 (same declaration text).

388. def OAI.EditApproximation.BinaryFraction.seedMedianWithWork line 2616

     Also declared: ComparatorChallenges/EditApproximation.lean:2616 (same declaration text).

389. def OAI.EditApproximation.BinaryFraction.coarseGridPenaltyWithWork line 2621

     Also declared: ComparatorChallenges/EditApproximation.lean:2621 (same declaration text).

390. def OAI.EditApproximation.BinaryFraction.coarseChildThresholdWithWork line 2628

     Also declared: ComparatorChallenges/EditApproximation.lean:2628 (same declaration text).

391. def OAI.EditApproximation.BinaryFraction.coarseChildAllowanceWithWork line 2635

     Also declared: ComparatorChallenges/EditApproximation.lean:2635 (same declaration text).

392. def OAI.EditApproximation.BinaryFraction.logarithmPartialAllocation line 2639

     Also declared: ComparatorChallenges/EditApproximation.lean:2639 (same declaration text).

393. def OAI.EditApproximation.BinaryFraction.bandMassAllocation line 2648

     Also declared: ComparatorChallenges/EditApproximation.lean:2648 (same declaration text).

394. def OAI.EditApproximation.BinaryFraction.sumListAllocation line 2651

     Also declared: ComparatorChallenges/EditApproximation.lean:2651 (same declaration text).

395. def OAI.EditApproximation.BinaryFraction.naturalDistanceLeAllocation line 2655

     Also declared: ComparatorChallenges/EditApproximation.lean:2655 (same declaration text).

396. def OAI.EditApproximation.BinaryFraction.queryExponentsAllocation line 2659

     Also declared: ComparatorChallenges/EditApproximation.lean:2659 (same declaration text).

397. def OAI.EditApproximation.BinaryFraction.seedMedianAllocation line 2666

     Also declared: ComparatorChallenges/EditApproximation.lean:2666 (same declaration text).

398. def OAI.EditApproximation.BinaryFraction.onlineMinimumAllocation line 2670

     Also declared: ComparatorChallenges/EditApproximation.lean:2670 (same declaration text).

399. def OAI.EditApproximation.BinaryFraction.optimisticTermReadAllocation line 2674

     Also declared: ComparatorChallenges/EditApproximation.lean:2674 (same declaration text).

400. def OAI.EditApproximation.BinaryFraction.gradientCellWithWork line 2683

     Also declared: ComparatorChallenges/EditApproximation.lean:2683 (same declaration text).

401. def OAI.EditApproximation.BinaryFraction.queryScalesWithWork line 2694

     Also declared: ComparatorChallenges/EditApproximation.lean:2694 (same declaration text).

402. def OAI.EditApproximation.BinaryFraction.querySeedMedianWithWork line 2699

     Also declared: ComparatorChallenges/EditApproximation.lean:2699 (same declaration text).

403. def OAI.EditApproximation.BinaryFraction.coarseBinaryPenaltyWithWork line 2703

     Also declared: ComparatorChallenges/EditApproximation.lean:2703 (same declaration text).

404. def OAI.EditApproximation.BinaryFraction.logarithmAllocation line 2709

     Also declared: ComparatorChallenges/EditApproximation.lean:2709 (same declaration text).

405. def OAI.EditApproximation.BinaryFraction.queryScalesAllocation line 2716

     Also declared: ComparatorChallenges/EditApproximation.lean:2716 (same declaration text).

406. def OAI.EditApproximation.BinaryFraction.coarseIndexChildren line 2720

     Also declared: ComparatorChallenges/EditApproximation.lean:2720 (same declaration text).

407. def OAI.EditApproximation.BinaryFraction.gradientCellAllocation line 2738

     Also declared: ComparatorChallenges/EditApproximation.lean:2738 (same declaration text).

408. def OAI.EditApproximation.BinaryFraction.coarseIndexedWithWork line 2749

     Also declared: ComparatorChallenges/EditApproximation.lean:2749 (same declaration text).

409. def OAI.EditApproximation.BinaryFraction.gradientAllocation line 2784

     Also declared: ComparatorChallenges/EditApproximation.lean:2784 (same declaration text).

410. def OAI.EditApproximation.BinaryFraction.gradientWithWork line 2796

     Also declared: ComparatorChallenges/EditApproximation.lean:2796 (same declaration text).

411. def OAI.EditApproximation.BinaryFraction.scoredArgmaxWithWork line 2800

     Also declared: ComparatorChallenges/EditApproximation.lean:2800 (same declaration text).

412. def OAI.EditApproximation.BinaryFraction.optimizerUpdateWithWork line 2813

     Also declared: ComparatorChallenges/EditApproximation.lean:2813 (same declaration text).

413. def OAI.EditApproximation.BinaryFraction.bandMassTotalWithWork line 2824

     Also declared: ComparatorChallenges/EditApproximation.lean:2824 (same declaration text).

414. def OAI.EditApproximation.BinaryFraction.coefficientWithWork line 2827

     Also declared: ComparatorChallenges/EditApproximation.lean:2827 (same declaration text).

415. def OAI.EditApproximation.BinaryFraction.naturalDistanceLeWithWork line 2832

     Also declared: ComparatorChallenges/EditApproximation.lean:2832 (same declaration text).

416. def OAI.EditApproximation.BinaryFraction.onlineMinimumWithWork line 2837

     Also declared: ComparatorChallenges/EditApproximation.lean:2837 (same declaration text).

417. def OAI.EditApproximation.BinaryFraction.refinementUpdateWithWork line 2843

     Also declared: ComparatorChallenges/EditApproximation.lean:2843 (same declaration text).

418. def OAI.EditApproximation.BinaryFraction.equalWithWork line 2852

     Also declared: ComparatorChallenges/EditApproximation.lean:2852 (same declaration text).

419. def OAI.EditApproximation.BinaryFraction.roundedSpacingWithWork line 2857

     Also declared: ComparatorChallenges/EditApproximation.lean:2857 (same declaration text).

420. def OAI.EditApproximation.BinaryFraction.maximizerWithWork line 2863

     Also declared: ComparatorChallenges/EditApproximation.lean:2863 (same declaration text).

421. def OAI.EditApproximation.BinaryFraction.groupTermsWithWork line 2868

     Also declared: ComparatorChallenges/EditApproximation.lean:2868 (same declaration text).

422. def OAI.EditApproximation.BinaryFraction.selectGroupWithWork line 2874

     Also declared: ComparatorChallenges/EditApproximation.lean:2874 (same declaration text).

423. def OAI.EditApproximation.BinaryFraction.finiteOptimizerWithWork line 2881

     Also declared: ComparatorChallenges/EditApproximation.lean:2881 (same declaration text).

424. def OAI.EditApproximation.BinaryFraction.selectionWithWork line 2891

     Also declared: ComparatorChallenges/EditApproximation.lean:2891 (same declaration text).

425. def OAI.EditApproximation.BitQuery.value line 2908

     Also declared: ComparatorChallenges/EditApproximation.lean:2908 (same declaration text).

426. def OAI.EditApproximation.BitQuery.work line 2913

     Also declared: ComparatorChallenges/EditApproximation.lean:2913 (same declaration text).

427. def OAI.EditApproximation.BitQuery.bind line 2918

     Also declared: ComparatorChallenges/EditApproximation.lean:2918 (same declaration text).

428. def OAI.EditApproximation.BitQuery.compute line 2923

     Also declared: ComparatorChallenges/EditApproximation.lean:2923 (same declaration text).

429. def OAI.EditApproximation.BitQuery.mapKeysWithWork line 2926

     Also declared: ComparatorChallenges/EditApproximation.lean:2926 (same declaration text).

430. def OAI.EditApproximation.BitQuery.restrictWithWork line 2932

     Also declared: ComparatorChallenges/EditApproximation.lean:2932 (same declaration text).

431. def OAI.EditApproximation.BitQuery.runMemo line 2942

     Also declared: ComparatorChallenges/EditApproximation.lean:2942 (same declaration text).

432. inductive OAI.EditApproximation.BitQuery.Footprint line 2956

     Also declared: ComparatorChallenges/EditApproximation.lean:2956 (same declaration text).

433. def OAI.EditApproximation.BitQuery.collect line 2963

     Also declared: ComparatorChallenges/EditApproximation.lean:2963 (same declaration text).

434. def OAI.EditApproximation.BitQuery.normalize line 2969

     Also declared: ComparatorChallenges/EditApproximation.lean:2969 (same declaration text).

435. def OAI.EditApproximation.substring line 2983

     Also declared: ComparatorChallenges/EditApproximation.lean:2983 (same declaration text).

436. structure OAI.EditApproximation.TargetInterval line 2986

     Also declared: ComparatorChallenges/EditApproximation.lean:2986 (same declaration text).

437. def OAI.EditApproximation.occurrenceDeficit line 2992

     Also declared: ComparatorChallenges/EditApproximation.lean:2992 (same declaration text).

438. def OAI.EditApproximation.natListMinimum line 2995

     Also declared: ComparatorChallenges/EditApproximation.lean:2995 (same declaration text).

439. def OAI.EditApproximation.coarsePadTo line 2999

     Also declared: ComparatorChallenges/EditApproximation.lean:2999 (same declaration text).

440. def OAI.EditApproximation.connectionBudget line 3002

     Also declared: ComparatorChallenges/EditApproximation.lean:3002 (same declaration text).

441. def OAI.EditApproximation.singletonCost line 3008

     Also declared: ComparatorChallenges/EditApproximation.lean:3008 (same declaration text).

442. def OAI.EditApproximation.makeTargetState line 3011

     Also declared: ComparatorChallenges/EditApproximation.lean:3011 (same declaration text).

443. def OAI.EditApproximation.targetEndpointDistance line 3014

     Also declared: ComparatorChallenges/EditApproximation.lean:3014 (same declaration text).

444. def OAI.EditApproximation.targetStates line 3017

     Also declared: ComparatorChallenges/EditApproximation.lean:3017 (same declaration text).

445. def OAI.EditApproximation.shortSourceCost line 3021

     Also declared: ComparatorChallenges/EditApproximation.lean:3021 (same declaration text).

446. def OAI.EditApproximation.exactSuffixDP line 3026

     Also declared: ComparatorChallenges/EditApproximation.lean:3026 (same declaration text).

447. def OAI.EditApproximation.exactSuffixAnswer line 3035

     Also declared: ComparatorChallenges/EditApproximation.lean:3035 (same declaration text).

448. def OAI.EditApproximation.sourceChild line 3047

     Also declared: ComparatorChallenges/EditApproximation.lean:3047 (same declaration text).

449. def OAI.EditApproximation.roundInterval line 3071

     Also declared: ComparatorChallenges/EditApproximation.lean:3071 (same declaration text).

450. def OAI.EditApproximation.localTargetStates line 3084

     Also declared: ComparatorChallenges/EditApproximation.lean:3084 (same declaration text).

451. def OAI.EditApproximation.rationalStateGap line 3089

     Also declared: ComparatorChallenges/EditApproximation.lean:3089 (same declaration text).

452. def OAI.EditApproximation.gridStateBox line 3092

     Also declared: ComparatorChallenges/EditApproximation.lean:3092 (same declaration text).

453. abbrev OAI.EditApproximation.PhysicalEntry line 3097

     Also declared: ComparatorChallenges/EditApproximation.lean:3097 (same declaration text).

454. def OAI.EditApproximation.makeStateWithWork line 3099

     Also declared: ComparatorChallenges/EditApproximation.lean:3099 (same declaration text).

455. def OAI.EditApproximation.cellTargetStates line 3152

     Also declared: ComparatorChallenges/EditApproximation.lean:3152 (same declaration text).

456. def OAI.EditApproximation.gridGapStates line 3156

     Also declared: ComparatorChallenges/EditApproximation.lean:3156 (same declaration text).

457. abbrev OAI.EditApproximation.PhysicalChildTables line 3161

     Also declared: ComparatorChallenges/EditApproximation.lean:3161 (same declaration text).

458. abbrev OAI.EditApproximation.PhysicalRationalAction line 3163

     Also declared: ComparatorChallenges/EditApproximation.lean:3163 (same declaration text).

459. def OAI.EditApproximation.localTargetCells line 3166

     Also declared: ComparatorChallenges/EditApproximation.lean:3166 (same declaration text).

460. def OAI.EditApproximation.coordinateEqualWithWork line 3170

     Also declared: ComparatorChallenges/EditApproximation.lean:3170 (same declaration text).

461. def OAI.EditApproximation.queryIntervalEqualWithWork line 3176

     Also declared: ComparatorChallenges/EditApproximation.lean:3176 (same declaration text).

462. def OAI.EditApproximation.childInputCode line 3181

     Also declared: ComparatorChallenges/EditApproximation.lean:3181 (same declaration text).

463. def OAI.EditApproximation.queryChildCodeWithWork line 3184

     Also declared: ComparatorChallenges/EditApproximation.lean:3184 (same declaration text).

464. def OAI.EditApproximation.querySliceHeadWithWork line 3192

     Also declared: ComparatorChallenges/EditApproximation.lean:3192 (same declaration text).

465. def OAI.EditApproximation.rankedBitProgramValue line 3198

     Also declared: ComparatorChallenges/EditApproximation.lean:3198 (same declaration text).

466. def OAI.EditApproximation.scheduledRefinementWordWithWork line 3205

     Also declared: ComparatorChallenges/EditApproximation.lean:3205 (same declaration text).

467. def OAI.EditApproximation.coordinateEqualAllocation line 3213

     Also declared: ComparatorChallenges/EditApproximation.lean:3213 (same declaration text).

468. def OAI.EditApproximation.queryIntervalEqualAllocation line 3217

     Also declared: ComparatorChallenges/EditApproximation.lean:3217 (same declaration text).

469. def OAI.EditApproximation.sourceChildAllocation line 3220

     Also declared: ComparatorChallenges/EditApproximation.lean:3220 (same declaration text).

470. def OAI.EditApproximation.zeroConnectionAllocation line 3227

     Also declared: ComparatorChallenges/EditApproximation.lean:3227 (same declaration text).

471. def OAI.EditApproximation.queryChildCodeAllocation line 3232

     Also declared: ComparatorChallenges/EditApproximation.lean:3232 (same declaration text).

472. def OAI.EditApproximation.roundStateAllocation line 3242

     Also declared: ComparatorChallenges/EditApproximation.lean:3242 (same declaration text).

473. def OAI.EditApproximation.actionEqualAllocation line 3245

     Also declared: ComparatorChallenges/EditApproximation.lean:3245 (same declaration text).

474. structure OAI.EditApproximation.RawUnskippedBand line 3249

     Also declared: ComparatorChallenges/EditApproximation.lean:3249 (same declaration text).

475. def OAI.EditApproximation.sourceIntervalAt line 3254

     Also declared: ComparatorChallenges/EditApproximation.lean:3254 (same declaration text).

476. def OAI.EditApproximation.initialConeValue line 3258

     Also declared: ComparatorChallenges/EditApproximation.lean:3258 (same declaration text).

477. def OAI.EditApproximation.wideChildStateList line 3264

     Also declared: ComparatorChallenges/EditApproximation.lean:3264 (same declaration text).

478. def OAI.EditApproximation.bandCutShift line 3270

     Also declared: ComparatorChallenges/EditApproximation.lean:3270 (same declaration text).

479. def OAI.EditApproximation.localInitialConeCenters line 3274

     Also declared: ComparatorChallenges/EditApproximation.lean:3274 (same declaration text).

480. def OAI.EditApproximation.gridStateBoxWithWork line 3281

     Also declared: ComparatorChallenges/EditApproximation.lean:3281 (same declaration text).

481. def OAI.EditApproximation.sourceChildWithWork line 3291

     Also declared: ComparatorChallenges/EditApproximation.lean:3291 (same declaration text).

482. def OAI.EditApproximation.cellRepresentativeStates line 3538

     Also declared: ComparatorChallenges/EditApproximation.lean:3538 (same declaration text).

483. def OAI.EditApproximation.groupRoundedStateList line 3543

     Also declared: ComparatorChallenges/EditApproximation.lean:3543 (same declaration text).

484. def OAI.EditApproximation.rawInitialConeCenters line 3551

     Also declared: ComparatorChallenges/EditApproximation.lean:3551 (same declaration text).

485. def OAI.EditApproximation.historyInputCode line 3557

     Also declared: ComparatorChallenges/EditApproximation.lean:3557 (same declaration text).

486. def OAI.EditApproximation.localOnlineSourceKeys line 3560

     Also declared: ComparatorChallenges/EditApproximation.lean:3560 (same declaration text).

487. def OAI.EditApproximation.queryHistoryCodeWithWork line 3565

     Also declared: ComparatorChallenges/EditApproximation.lean:3565 (same declaration text).

488. def OAI.EditApproximation.queryOrderedChildInputsWithWork line 3570

     Also declared: ComparatorChallenges/EditApproximation.lean:3570 (same declaration text).

489. def OAI.EditApproximation.queryHistoryEqualWithWork line 3575

     Also declared: ComparatorChallenges/EditApproximation.lean:3575 (same declaration text).

490. def OAI.EditApproximation.queryGapStatesWithWork line 3580

     Also declared: ComparatorChallenges/EditApproximation.lean:3580 (same declaration text).

491. def OAI.EditApproximation.queryOnlineKeyEqualWithWork line 3594

     Also declared: ComparatorChallenges/EditApproximation.lean:3594 (same declaration text).

492. def OAI.EditApproximation.physicalEntryCode line 3599

     Also declared: ComparatorChallenges/EditApproximation.lean:3599 (same declaration text).

493. def OAI.EditApproximation.rankedBitLocalWork line 3602

     Also declared: ComparatorChallenges/EditApproximation.lean:3602 (same declaration text).

494. def OAI.EditApproximation.refinementParameterWordsWithWork line 3607

     Also declared: ComparatorChallenges/EditApproximation.lean:3607 (same declaration text).

495. def OAI.EditApproximation.queryHistoryEqualAllocation line 3615

     Also declared: ComparatorChallenges/EditApproximation.lean:3615 (same declaration text).

496. def OAI.EditApproximation.queryOnlineKeyEqualAllocation line 3618

     Also declared: ComparatorChallenges/EditApproximation.lean:3618 (same declaration text).

497. def OAI.EditApproximation.gridStateBoxAllocation line 3621

     Also declared: ComparatorChallenges/EditApproximation.lean:3621 (same declaration text).

498. def OAI.EditApproximation.queryHistoryCodeAllocation line 3635

     Also declared: ComparatorChallenges/EditApproximation.lean:3635 (same declaration text).

499. def OAI.EditApproximation.queryOrderedChildInputsAllocation line 3639

     Also declared: ComparatorChallenges/EditApproximation.lean:3639 (same declaration text).

500. def OAI.EditApproximation.actionMemberAllocation line 3643

     Also declared: ComparatorChallenges/EditApproximation.lean:3643 (same declaration text).

501. def OAI.EditApproximation.queryGapStatesAllocation line 3647

     Also declared: ComparatorChallenges/EditApproximation.lean:3647 (same declaration text).

502. def OAI.EditApproximation.wideActionList line 3669

     Also declared: ComparatorChallenges/EditApproximation.lean:3669 (same declaration text).

503. def OAI.EditApproximation.physicalSourceInterval line 3673

     Also declared: ComparatorChallenges/EditApproximation.lean:3673 (same declaration text).

504. def OAI.EditApproximation.localInitialConeTable line 3676

     Also declared: ComparatorChallenges/EditApproximation.lean:3676 (same declaration text).

505. def OAI.EditApproximation.wideChildGridWithWork line 3684

     Also declared: ComparatorChallenges/EditApproximation.lean:3684 (same declaration text).

506. def OAI.EditApproximation.queryOrderedHistoryInputsWithWork line 3697

     Also declared: ComparatorChallenges/EditApproximation.lean:3697 (same declaration text).

507. def OAI.EditApproximation.queryNeededInputsWithWork line 3702

     Also declared: ComparatorChallenges/EditApproximation.lean:3702 (same declaration text).

508. def OAI.EditApproximation.computedQueryParameters line 3710

     Also declared: ComparatorChallenges/EditApproximation.lean:3710 (same declaration text).

509. def OAI.EditApproximation.wideChildGridAllocation line 3723

     Also declared: ComparatorChallenges/EditApproximation.lean:3723 (same declaration text).

510. def OAI.EditApproximation.queryOrderedHistoryInputsAllocation line 3738

     Also declared: ComparatorChallenges/EditApproximation.lean:3738 (same declaration text).

511. def OAI.EditApproximation.queryNeededInputsAllocation line 3742

     Also declared: ComparatorChallenges/EditApproximation.lean:3742 (same declaration text).

512. def OAI.EditApproximation.physicalSource line 3749

     Also declared: ComparatorChallenges/EditApproximation.lean:3749 (same declaration text).

513. def OAI.EditApproximation.wideActionGridWithWork line 3752

     Also declared: ComparatorChallenges/EditApproximation.lean:3752 (same declaration text).

514. def OAI.EditApproximation.physicalCoarsePreparationCost line 3758

     Also declared: ComparatorChallenges/EditApproximation.lean:3758 (same declaration text).

515. def OAI.EditApproximation.wideActionGridAllocation line 3763

     Also declared: ComparatorChallenges/EditApproximation.lean:3763 (same declaration text).

516. def OAI.EditApproximation.BinaryFraction.sumListWithWork line 3777

     Also declared: ComparatorChallenges/EditApproximation.lean:3777 (same declaration text).

517. def OAI.EditApproximation.BinaryFraction.connectionTermsWithWork line 3781

     Also declared: ComparatorChallenges/EditApproximation.lean:3781 (same declaration text).

518. def OAI.EditApproximation.BinaryFraction.bandEnvelopeReadWithWork line 3792

     Also declared: ComparatorChallenges/EditApproximation.lean:3792 (same declaration text).

519. def OAI.EditApproximation.BinaryFraction.onlineLinearReadWithWork line 3801

     Also declared: ComparatorChallenges/EditApproximation.lean:3801 (same declaration text).

520. def OAI.EditApproximation.BinaryFraction.targetCellsWithWork line 3812

     Also declared: ComparatorChallenges/EditApproximation.lean:3812 (same declaration text).

521. def OAI.EditApproximation.BinaryFraction.cellStatesWithWork line 3820

     Also declared: ComparatorChallenges/EditApproximation.lean:3820 (same declaration text).

522. def OAI.EditApproximation.BinaryFraction.bandCoordinatesWithWork line 3828

     Also declared: ComparatorChallenges/EditApproximation.lean:3828 (same declaration text).

523. def OAI.EditApproximation.BinaryFraction.countedBandCoordinateWithWork line 3835

     Also declared: ComparatorChallenges/EditApproximation.lean:3835 (same declaration text).

524. def OAI.EditApproximation.BinaryFraction.representativeScaleReadWithWork line 3842

     Also declared: ComparatorChallenges/EditApproximation.lean:3842 (same declaration text).

525. def OAI.EditApproximation.BinaryFraction.queryRawCentersWithWork line 3855

     Also declared: ComparatorChallenges/EditApproximation.lean:3855 (same declaration text).

526. def OAI.EditApproximation.BinaryFraction.queryWideInputsWithWork line 3866

     Also declared: ComparatorChallenges/EditApproximation.lean:3866 (same declaration text).

527. def OAI.EditApproximation.BinaryFraction.queryRawHistoryInputsWithWork line 3876

     Also declared: ComparatorChallenges/EditApproximation.lean:3876 (same declaration text).

528. def OAI.EditApproximation.BinaryFraction.queryGroupRoundedStatesWithWork line 3887

     Also declared: ComparatorChallenges/EditApproximation.lean:3887 (same declaration text).

529. def OAI.EditApproximation.BinaryFraction.queryOnlineIntegerReadWithWork line 3907

     Also declared: ComparatorChallenges/EditApproximation.lean:3907 (same declaration text).

530. def OAI.EditApproximation.BinaryFraction.queryChildReadWithWork line 3913

     Also declared: ComparatorChallenges/EditApproximation.lean:3913 (same declaration text).

531. def OAI.EditApproximation.BinaryFraction.queryHistoryReadWithWork line 3917

     Also declared: ComparatorChallenges/EditApproximation.lean:3917 (same declaration text).

532. def OAI.EditApproximation.BinaryFraction.queryParentReadWithWork line 3921

     Also declared: ComparatorChallenges/EditApproximation.lean:3921 (same declaration text).

533. def OAI.EditApproximation.BinaryFraction.initialGridReadWithWork line 3925

     Also declared: ComparatorChallenges/EditApproximation.lean:3925 (same declaration text).

534. def OAI.EditApproximation.BinaryFraction.queryInitialConeCentersWithWork line 3936

     Also declared: ComparatorChallenges/EditApproximation.lean:3936 (same declaration text).

535. def OAI.EditApproximation.BinaryFraction.connectionTermsAllocation line 3947

     Also declared: ComparatorChallenges/EditApproximation.lean:3947 (same declaration text).

536. def OAI.EditApproximation.BinaryFraction.endpointDistanceAllocation line 3953

     Also declared: ComparatorChallenges/EditApproximation.lean:3953 (same declaration text).

537. def OAI.EditApproximation.BinaryFraction.stateGapAllocation line 3958

     Also declared: ComparatorChallenges/EditApproximation.lean:3958 (same declaration text).

538. def OAI.EditApproximation.BinaryFraction.queryChildReadAllocation line 3962

     Also declared: ComparatorChallenges/EditApproximation.lean:3962 (same declaration text).

539. def OAI.EditApproximation.BinaryFraction.queryHistoryReadAllocation line 3966

     Also declared: ComparatorChallenges/EditApproximation.lean:3966 (same declaration text).

540. def OAI.EditApproximation.BinaryFraction.queryOnlineIntegerReadAllocation line 3970

     Also declared: ComparatorChallenges/EditApproximation.lean:3970 (same declaration text).

541. def OAI.EditApproximation.BinaryFraction.bandCoordinatesAllocation line 3976

     Also declared: ComparatorChallenges/EditApproximation.lean:3976 (same declaration text).

542. def OAI.EditApproximation.BinaryFraction.scoredArgmaxAllocation line 3984

     Also declared: ComparatorChallenges/EditApproximation.lean:3984 (same declaration text).

543. def OAI.EditApproximation.BinaryFraction.anchorGuardAllocation line 3993

     Also declared: ComparatorChallenges/EditApproximation.lean:3993 (same declaration text).

544. def OAI.EditApproximation.BinaryFraction.bandEnvelopeReadAllocation line 4002

     Also declared: ComparatorChallenges/EditApproximation.lean:4002 (same declaration text).

545. def OAI.EditApproximation.BinaryFraction.targetCellsAllocation line 4012

     Also declared: ComparatorChallenges/EditApproximation.lean:4012 (same declaration text).

546. def OAI.EditApproximation.BinaryFraction.cellStatesAllocation line 4019

     Also declared: ComparatorChallenges/EditApproximation.lean:4019 (same declaration text).

547. def OAI.EditApproximation.BinaryFraction.queryRawCentersAllocation line 4026

     Also declared: ComparatorChallenges/EditApproximation.lean:4026 (same declaration text).

548. def OAI.EditApproximation.BinaryFraction.queryOnlineKeysAllocation line 4039

     Also declared: ComparatorChallenges/EditApproximation.lean:4039 (same declaration text).

549. def OAI.EditApproximation.BinaryFraction.representativeScaleReadAllocation line 4045

     Also declared: ComparatorChallenges/EditApproximation.lean:4045 (same declaration text).

550. def OAI.EditApproximation.BinaryFraction.queryWideInputsAllocation line 4058

     Also declared: ComparatorChallenges/EditApproximation.lean:4058 (same declaration text).

551. def OAI.EditApproximation.BinaryFraction.queryRawHistoryInputsAllocation line 4075

     Also declared: ComparatorChallenges/EditApproximation.lean:4075 (same declaration text).

552. def OAI.EditApproximation.BinaryFraction.queryGroupRoundedStatesAllocation line 4091

     Also declared: ComparatorChallenges/EditApproximation.lean:4091 (same declaration text).

553. def OAI.EditApproximation.BinaryFraction.groupIndexAllocation line 4112

     Also declared: ComparatorChallenges/EditApproximation.lean:4112 (same declaration text).

554. def OAI.EditApproximation.BinaryFraction.queryParentReadAllocation line 4117

     Also declared: ComparatorChallenges/EditApproximation.lean:4117 (same declaration text).

555. def OAI.EditApproximation.BinaryFraction.onlineLinearReadAllocation line 4121

     Also declared: ComparatorChallenges/EditApproximation.lean:4121 (same declaration text).

556. def OAI.EditApproximation.BinaryFraction.countedBandCoordinateAllocation line 4133

     Also declared: ComparatorChallenges/EditApproximation.lean:4133 (same declaration text).

557. def OAI.EditApproximation.BinaryFraction.queryInitialConeCentersAllocation line 4139

     Also declared: ComparatorChallenges/EditApproximation.lean:4139 (same declaration text).

558. def OAI.EditApproximation.BinaryFraction.connectionWithWork line 4154

     Also declared: ComparatorChallenges/EditApproximation.lean:4154 (same declaration text).

559. def OAI.EditApproximation.BinaryFraction.envelopeVectorReadWithWork line 4160

     Also declared: ComparatorChallenges/EditApproximation.lean:4160 (same declaration text).

560. def OAI.EditApproximation.BinaryFraction.bellmanActionReadWithWork line 4164

     Also declared: ComparatorChallenges/EditApproximation.lean:4164 (same declaration text).

561. def OAI.EditApproximation.BinaryFraction.cellCentersReadWithWork line 4176

     Also declared: ComparatorChallenges/EditApproximation.lean:4176 (same declaration text).

562. def OAI.EditApproximation.BinaryFraction.countedBandVerticesWithWork line 4188

     Also declared: ComparatorChallenges/EditApproximation.lean:4188 (same declaration text).

563. def OAI.EditApproximation.BinaryFraction.onlineIndexSetupWithWork line 4198

     Also declared: ComparatorChallenges/EditApproximation.lean:4198 (same declaration text).

564. def OAI.EditApproximation.BinaryFraction.localRepresentativeReadWithWork line 4206

     Also declared: ComparatorChallenges/EditApproximation.lean:4206 (same declaration text).

565. def OAI.EditApproximation.BinaryFraction.queryGroupKeysWithWork line 4216

     Also declared: ComparatorChallenges/EditApproximation.lean:4216 (same declaration text).

566. def OAI.EditApproximation.BinaryFraction.queryMeanWithWork line 4227

     Also declared: ComparatorChallenges/EditApproximation.lean:4227 (same declaration text).

567. def OAI.EditApproximation.BinaryFraction.initialCentersReadWithWork line 4232

     Also declared: ComparatorChallenges/EditApproximation.lean:4232 (same declaration text).

568. def OAI.EditApproximation.BinaryFraction.queryInitialSeedReadWithWork line 4242

     Also declared: ComparatorChallenges/EditApproximation.lean:4242 (same declaration text).

569. def OAI.EditApproximation.BinaryFraction.queryOverrideParentReadWithWork line 4253

     Also declared: ComparatorChallenges/EditApproximation.lean:4253 (same declaration text).

570. def OAI.EditApproximation.BinaryFraction.connectionAllocation line 4262

     Also declared: ComparatorChallenges/EditApproximation.lean:4262 (same declaration text).

571. def OAI.EditApproximation.BinaryFraction.coordinateVectorAllocation line 4267

     Also declared: ComparatorChallenges/EditApproximation.lean:4267 (same declaration text).

572. def OAI.EditApproximation.BinaryFraction.maximizerAllocation line 4270

     Also declared: ComparatorChallenges/EditApproximation.lean:4270 (same declaration text).

573. def OAI.EditApproximation.BinaryFraction.onlineIndexSetupAllocation line 4275

     Also declared: ComparatorChallenges/EditApproximation.lean:4275 (same declaration text).

574. def OAI.EditApproximation.BinaryFraction.envelopeVectorReadAllocation line 4282

     Also declared: ComparatorChallenges/EditApproximation.lean:4282 (same declaration text).

575. def OAI.EditApproximation.BinaryFraction.roundedBandReadAllocation line 4287

     Also declared: ComparatorChallenges/EditApproximation.lean:4287 (same declaration text).

576. def OAI.EditApproximation.BinaryFraction.queryGroupKeysAllocation line 4297

     Also declared: ComparatorChallenges/EditApproximation.lean:4297 (same declaration text).

577. def OAI.EditApproximation.BinaryFraction.initialCellAllocation line 4311

     Also declared: ComparatorChallenges/EditApproximation.lean:4311 (same declaration text).

578. def OAI.EditApproximation.BinaryFraction.localRepresentativeReadAllocation line 4316

     Also declared: ComparatorChallenges/EditApproximation.lean:4316 (same declaration text).

579. def OAI.EditApproximation.BinaryFraction.cellCentersReadAllocation line 4325

     Also declared: ComparatorChallenges/EditApproximation.lean:4325 (same declaration text).

580. def OAI.EditApproximation.BinaryFraction.selectGroupAllocation line 4337

     Also declared: ComparatorChallenges/EditApproximation.lean:4337 (same declaration text).

581. def OAI.EditApproximation.BinaryFraction.bellmanActionReadAllocation line 4341

     Also declared: ComparatorChallenges/EditApproximation.lean:4341 (same declaration text).

582. def OAI.EditApproximation.BinaryFraction.countedBandVerticesAllocation line 4355

     Also declared: ComparatorChallenges/EditApproximation.lean:4355 (same declaration text).

583. def OAI.EditApproximation.BinaryFraction.queryInitialSeedReadAllocation line 4362

     Also declared: ComparatorChallenges/EditApproximation.lean:4362 (same declaration text).

584. def OAI.EditApproximation.BinaryFraction.queryOverrideParentReadAllocation line 4368

     Also declared: ComparatorChallenges/EditApproximation.lean:4368 (same declaration text).

585. def OAI.EditApproximation.BinaryFraction.prefixReadWithWork line 4373

     Also declared: ComparatorChallenges/EditApproximation.lean:4373 (same declaration text).

586. def OAI.EditApproximation.BinaryFraction.bellmanReadWithWork line 4385

     Also declared: ComparatorChallenges/EditApproximation.lean:4385 (same declaration text).

587. def OAI.EditApproximation.BinaryFraction.queryWarmupInputsWithWork line 4393

     Also declared: ComparatorChallenges/EditApproximation.lean:4393 (same declaration text).

588. def OAI.EditApproximation.BinaryFraction.endpointConnectionAllocation line 4400

     Also declared: ComparatorChallenges/EditApproximation.lean:4400 (same declaration text).

589. def OAI.EditApproximation.BinaryFraction.prefixReadAllocation line 4404

     Also declared: ComparatorChallenges/EditApproximation.lean:4404 (same declaration text).

590. def OAI.EditApproximation.BinaryFraction.optimizerAllocation line 4418

     Also declared: ComparatorChallenges/EditApproximation.lean:4418 (same declaration text).

591. def OAI.EditApproximation.BinaryFraction.queryEarlierRepresentativesAllocation line 4428

     Also declared: ComparatorChallenges/EditApproximation.lean:4428 (same declaration text).

592. def OAI.EditApproximation.BinaryFraction.queryWarmupInputsAllocation line 4446

     Also declared: ComparatorChallenges/EditApproximation.lean:4446 (same declaration text).

593. def OAI.EditApproximation.BinaryFraction.bellmanReadAllocation line 4453

     Also declared: ComparatorChallenges/EditApproximation.lean:4453 (same declaration text).

594. def OAI.EditApproximation.BinaryFraction.prefixMinimumReadWithWork line 4461

     Also declared: ComparatorChallenges/EditApproximation.lean:4461 (same declaration text).

595. def OAI.EditApproximation.BinaryFraction.localContinuationReadWithWork line 4470

     Also declared: ComparatorChallenges/EditApproximation.lean:4470 (same declaration text).

596. def OAI.EditApproximation.BinaryFraction.prefixMinimumReadAllocation line 4481

     Also declared: ComparatorChallenges/EditApproximation.lean:4481 (same declaration text).

597. def OAI.EditApproximation.BinaryFraction.localContinuationReadAllocation line 4491

     Also declared: ComparatorChallenges/EditApproximation.lean:4491 (same declaration text).

598. def OAI.EditApproximation.BinaryFraction.endpointActionAllocation line 4505

     Also declared: ComparatorChallenges/EditApproximation.lean:4505 (same declaration text).

599. def OAI.EditApproximation.BinaryFraction.selectionAllocation line 4508

     Also declared: ComparatorChallenges/EditApproximation.lean:4508 (same declaration text).

600. def OAI.EditApproximation.BinaryFraction.cutGuardReadWithWork line 4517

     Also declared: ComparatorChallenges/EditApproximation.lean:4517 (same declaration text).

601. def OAI.EditApproximation.BinaryFraction.cutGuardReadAllocation line 4529

     Also declared: ComparatorChallenges/EditApproximation.lean:4529 (same declaration text).

602. def OAI.EditApproximation.BinaryFraction.bandPredicateReadAllocation line 4544

     Also declared: ComparatorChallenges/EditApproximation.lean:4544 (same declaration text).

603. def OAI.EditApproximation.rationalConnectionBudget line 4564

     Also declared: ComparatorChallenges/EditApproximation.lean:4564 (same declaration text).

604. def OAI.EditApproximation.bandChildEnvelope line 4568

     Also declared: ComparatorChallenges/EditApproximation.lean:4568 (same declaration text).

605. def OAI.EditApproximation.bandEnvelopeExponent line 4574

     Also declared: ComparatorChallenges/EditApproximation.lean:4574 (same declaration text).

606. def OAI.EditApproximation.zeroConnectionWithWork line 4580

     Also declared: ComparatorChallenges/EditApproximation.lean:4580 (same declaration text).

607. def OAI.EditApproximation.roundStateWithWork line 4587

     Also declared: ComparatorChallenges/EditApproximation.lean:4587 (same declaration text).

608. def OAI.EditApproximation.actionEqualWithWork line 4811

     Also declared: ComparatorChallenges/EditApproximation.lean:4811 (same declaration text).

609. def OAI.EditApproximation.localRefinementRepresentatives line 4817

     Also declared: ComparatorChallenges/EditApproximation.lean:4817 (same declaration text).

610. def OAI.EditApproximation.sharedBandRationalAction line 4824

     Also declared: ComparatorChallenges/EditApproximation.lean:4824 (same declaration text).

611. def OAI.EditApproximation.localGroupQueryKeys line 4828

     Also declared: ComparatorChallenges/EditApproximation.lean:4828 (same declaration text).

612. def OAI.EditApproximation.rationalWidePrefixCost line 4833

     Also declared: ComparatorChallenges/EditApproximation.lean:4833 (same declaration text).

613. def OAI.EditApproximation.bandRoundSpacing line 4840

     Also declared: ComparatorChallenges/EditApproximation.lean:4840 (same declaration text).

614. def OAI.EditApproximation.actionMemberWithWork line 4844

     Also declared: ComparatorChallenges/EditApproximation.lean:4844 (same declaration text).

615. def OAI.EditApproximation.wideEarlierInputCover line 4852

     Also declared: ComparatorChallenges/EditApproximation.lean:4852 (same declaration text).

616. def OAI.EditApproximation.queryEarlierRepresentatives line 4859

     Also declared: ComparatorChallenges/EditApproximation.lean:4859 (same declaration text).

617. def OAI.EditApproximation.rationalWidePrefixMinimum line 4868

     Also declared: ComparatorChallenges/EditApproximation.lean:4868 (same declaration text).

618. def OAI.EditApproximation.roundedBandAction line 4874

     Also declared: ComparatorChallenges/EditApproximation.lean:4874 (same declaration text).

619. def OAI.EditApproximation.queryEarlierInputCover line 4880

     Also declared: ComparatorChallenges/EditApproximation.lean:4880 (same declaration text).

620. def OAI.EditApproximation.canonicalRoundedBandAction line 4886

     Also declared: ComparatorChallenges/EditApproximation.lean:4886 (same declaration text).

621. def OAI.EditApproximation.parameterClogWithWork line 4900

     Also declared: ComparatorChallenges/EditApproximation.lean:4900 (same declaration text).

622. def OAI.EditApproximation.parameterLogWithWork line 4904

     Also declared: ComparatorChallenges/EditApproximation.lean:4904 (same declaration text).

623. def OAI.EditApproximation.parameterRootSearch line 4908

     Also declared: ComparatorChallenges/EditApproximation.lean:4908 (same declaration text).

624. def OAI.EditApproximation.parameterPowerWithWork line 4914

     Also declared: ComparatorChallenges/EditApproximation.lean:4914 (same declaration text).

625. def OAI.EditApproximation.physicalCoarseInputStorage line 4919

     Also declared: ComparatorChallenges/EditApproximation.lean:4919 (same declaration text).

626. def OAI.EditApproximation.computedQueryPassWithWork line 4924

     Also declared: ComparatorChallenges/EditApproximation.lean:4924 (same declaration text).

627. def OAI.EditApproximation.storedIntegerBits line 4937

     Also declared: ComparatorChallenges/EditApproximation.lean:4937 (same declaration text).

628. def OAI.EditApproximation.parameterSqrtWithWork line 4940

     Also declared: ComparatorChallenges/EditApproximation.lean:4940 (same declaration text).

629. def OAI.EditApproximation.computedQuerySetupWithWork line 4942

     Also declared: ComparatorChallenges/EditApproximation.lean:4942 (same declaration text).

630. def OAI.EditApproximation.integerParametersWithWork line 4948

     Also declared: ComparatorChallenges/EditApproximation.lean:4948 (same declaration text).

631. structure OAI.EditApproximation.PhysicalTableRequest line 4979

     Also declared: ComparatorChallenges/EditApproximation.lean:4979 (same declaration text).

632. def OAI.EditApproximation.rawRefinementCenters line 4988

     Also declared: ComparatorChallenges/EditApproximation.lean:4988 (same declaration text).

633. def OAI.EditApproximation.wideWarmupInputs line 4993

     Also declared: ComparatorChallenges/EditApproximation.lean:4993 (same declaration text).

634. def OAI.EditApproximation.queryMeanRead line 4998

     Also declared: ComparatorChallenges/EditApproximation.lean:4998 (same declaration text).

635. def OAI.EditApproximation.physicalNodeCodeWithWork line 5003

     Also declared: ComparatorChallenges/EditApproximation.lean:5003 (same declaration text).

636. def OAI.EditApproximation.rationalParametersWithWork line 5008

     Also declared: ComparatorChallenges/EditApproximation.lean:5008 (same declaration text).

637. def OAI.EditApproximation.onlineMassWithWork line 5019

     Also declared: ComparatorChallenges/EditApproximation.lean:5019 (same declaration text).

638. def OAI.EditApproximation.refinementInitialSupport line 5026

     Also declared: ComparatorChallenges/EditApproximation.lean:5026 (same declaration text).

639. def OAI.EditApproximation.refinementBandInputList line 5034

     Also declared: ComparatorChallenges/EditApproximation.lean:5034 (same declaration text).

640. def OAI.EditApproximation.previousPassRequest line 5039

     Also declared: ComparatorChallenges/EditApproximation.lean:5039 (same declaration text).

641. def OAI.EditApproximation.physicalEntryCodeWithWork line 5043

     Also declared: ComparatorChallenges/EditApproximation.lean:5043 (same declaration text).

642. def OAI.EditApproximation.queryPhysicalBoundedWithWork line 5048

     Also declared: ComparatorChallenges/EditApproximation.lean:5048 (same declaration text).

643. def OAI.EditApproximation.globalParameterWork line 5057

     Also declared: ComparatorChallenges/EditApproximation.lean:5057 (same declaration text).

644. def OAI.EditApproximation.physicalLargeInputWithWork line 5061

     Also declared: ComparatorChallenges/EditApproximation.lean:5061 (same declaration text).

645. def OAI.EditApproximation.physicalTableCodeAllocation line 5074

     Also declared: ComparatorChallenges/EditApproximation.lean:5074 (same declaration text).

646. def OAI.EditApproximation.queryPhysicalBoundedAllocation line 5077

     Also declared: ComparatorChallenges/EditApproximation.lean:5077 (same declaration text).

647. def OAI.EditApproximation.physicalTableCodeWithWork line 5082

     Also declared: ComparatorChallenges/EditApproximation.lean:5082 (same declaration text).

648. def OAI.EditApproximation.PhysicalTableRequest.remainingDepth line 5099

     Also declared: ComparatorChallenges/EditApproximation.lean:5099 (same declaration text).

649. def OAI.EditApproximation.PhysicalTableRequest.rank line 5102

     Also declared: ComparatorChallenges/EditApproximation.lean:5102 (same declaration text).

650. def OAI.EditApproximation.PhysicalTableRequest.Bounded line 5105

     Also declared: ComparatorChallenges/EditApproximation.lean:5105 (same declaration text).

651. def OAI.EditApproximation.PhysicalTableRequest.warmup line 5108

     Also declared: ComparatorChallenges/EditApproximation.lean:5108 (same declaration text).

652. def OAI.EditApproximation.PhysicalTableRequest.refinement line 5112

     Also declared: ComparatorChallenges/EditApproximation.lean:5112 (same declaration text).

653. def OAI.EditApproximation.PhysicalTableRequest.sameIndexChild line 5116

     Also declared: ComparatorChallenges/EditApproximation.lean:5116 (same declaration text).

654. def OAI.EditApproximation.PhysicalTableRequest.combinedRank line 5121

     Also declared: ComparatorChallenges/EditApproximation.lean:5121 (same declaration text).

655. def OAI.EditApproximation.physicalWarmupChildQuery line 5133

     Also declared: ComparatorChallenges/EditApproximation.lean:5133 (same declaration text).

656. def OAI.EditApproximation.physicalRefinementCurrentQuery line 5172

     Also declared: ComparatorChallenges/EditApproximation.lean:5172 (same declaration text).

657. def OAI.EditApproximation.physicalRefinementEarlierQuery line 5204

     Also declared: ComparatorChallenges/EditApproximation.lean:5204 (same declaration text).

658. def OAI.EditApproximation.physicalRefinementWarmupRead line 5241

     Also declared: ComparatorChallenges/EditApproximation.lean:5241 (same declaration text).

659. def OAI.EditApproximation.previousPassRead line 5267

     Also declared: ComparatorChallenges/EditApproximation.lean:5267 (same declaration text).

660. abbrev OAI.EditApproximation.ChargedPhysicalRequest line 5303

     Also declared: ComparatorChallenges/EditApproximation.lean:5303 (same declaration text).

661. def OAI.EditApproximation.chargedPreviousPass line 5307

     Also declared: ComparatorChallenges/EditApproximation.lean:5307 (same declaration text).

662. def OAI.EditApproximation.queryPhysicalTableRead line 5314

     Also declared: ComparatorChallenges/EditApproximation.lean:5314 (same declaration text).

663. abbrev OAI.EditApproximation.ComputedFamilyTableKey line 5321

     Also declared: ComparatorChallenges/EditApproximation.lean:5321 (same declaration text).

664. def OAI.EditApproximation.chargedPhysicalCodeWithWork line 5326

     Also declared: ComparatorChallenges/EditApproximation.lean:5326 (same declaration text).

665. def OAI.EditApproximation.queryPhysicalWarmupRead line 5333

     Also declared: ComparatorChallenges/EditApproximation.lean:5333 (same declaration text).

666. def OAI.EditApproximation.queryPhysicalCurrentRead line 5360

     Also declared: ComparatorChallenges/EditApproximation.lean:5360 (same declaration text).

667. def OAI.EditApproximation.queryPhysicalEarlierRead line 5393

     Also declared: ComparatorChallenges/EditApproximation.lean:5393 (same declaration text).

668. def OAI.EditApproximation.chargedPhysicalRemaining line 5471

     Also declared: ComparatorChallenges/EditApproximation.lean:5471 (same declaration text).

669. def OAI.EditApproximation.chargedPhysicalCodeAllocation line 5476

     Also declared: ComparatorChallenges/EditApproximation.lean:5476 (same declaration text).

670. def OAI.EditApproximation.queryPhysicalMassRead line 5481

     Also declared: ComparatorChallenges/EditApproximation.lean:5481 (same declaration text).

671. def OAI.EditApproximation.integerClosedRange line 5499

     Also declared: ComparatorChallenges/EditApproximation.lean:5499 (same declaration text).

672. def OAI.EditApproximation.groupSampleCount line 5502

     Also declared: ComparatorChallenges/EditApproximation.lean:5502 (same declaration text).

673. def OAI.EditApproximation.groupScaleTrueCost line 5504

     Also declared: ComparatorChallenges/EditApproximation.lean:5504 (same declaration text).

674. def OAI.EditApproximation.selectGroupMember line 5507

     Also declared: ComparatorChallenges/EditApproximation.lean:5507 (same declaration text).

675. instance OAI.EditApproximation.coarseDrawsMeasurableSpace line 5511

     Also declared: ComparatorChallenges/EditApproximation.lean:5511 (same declaration text).

676. def OAI.EditApproximation.groupDyadicScales line 5520

     Also declared: ComparatorChallenges/EditApproximation.lean:5520 (same declaration text).

677. def OAI.EditApproximation.groupScaleEstimate line 5524

     Also declared: ComparatorChallenges/EditApproximation.lean:5524 (same declaration text).

678. def OAI.EditApproximation.coarseDrawMeasure line 5529

     Also declared: ComparatorChallenges/EditApproximation.lean:5529 (same declaration text).

679. def OAI.EditApproximation.groupMemberEstimate line 5537

     Also declared: ComparatorChallenges/EditApproximation.lean:5537 (same declaration text).

680. def OAI.EditApproximation.BinaryFraction.groupScalesWithWork line 5551

     Also declared: ComparatorChallenges/EditApproximation.lean:5551 (same declaration text).

681. def OAI.EditApproximation.BinaryFraction.bandPredicateReadWithWork line 5556

     Also declared: ComparatorChallenges/EditApproximation.lean:5556 (same declaration text).

682. def OAI.EditApproximation.BinaryFraction.indexedGroupScales line 5574

     Also declared: ComparatorChallenges/EditApproximation.lean:5574 (same declaration text).

683. def OAI.EditApproximation.BinaryFraction.queryOnlineKeysWithWork line 5582

     Also declared: ComparatorChallenges/EditApproximation.lean:5582 (same declaration text).

684. def OAI.EditApproximation.BinaryFraction.groupScalesAllocation line 5790

     Also declared: ComparatorChallenges/EditApproximation.lean:5790 (same declaration text).

685. def OAI.EditApproximation.BinaryFraction.bandFromActionsReadWithWork line 5795

     Also declared: ComparatorChallenges/EditApproximation.lean:5795 (same declaration text).

686. def OAI.EditApproximation.BinaryFraction.queryInitialSupportWithWork line 5808

     Also declared: ComparatorChallenges/EditApproximation.lean:5808 (same declaration text).

687. def OAI.EditApproximation.BinaryFraction.queryEarlierRepresentativesWithWork line 5822

     Also declared: ComparatorChallenges/EditApproximation.lean:5822 (same declaration text).

688. def OAI.EditApproximation.BinaryFraction.bandFromActionsReadAllocation line 5836

     Also declared: ComparatorChallenges/EditApproximation.lean:5836 (same declaration text).

689. def OAI.EditApproximation.BinaryFraction.queryInitialSupportAllocation line 5848

     Also declared: ComparatorChallenges/EditApproximation.lean:5848 (same declaration text).

690. def OAI.EditApproximation.BinaryFraction.queryBandInputsWithWork line 5864

     Also declared: ComparatorChallenges/EditApproximation.lean:5864 (same declaration text).

691. def OAI.EditApproximation.BinaryFraction.queryEarlierInputsWithWork line 5872

     Also declared: ComparatorChallenges/EditApproximation.lean:5872 (same declaration text).

692. def OAI.EditApproximation.BinaryFraction.queryEarlierInputsAllocation line 5881

     Also declared: ComparatorChallenges/EditApproximation.lean:5881 (same declaration text).

693. def OAI.EditApproximation.BinaryFraction.queryBandInputsAllocation line 5890

     Also declared: ComparatorChallenges/EditApproximation.lean:5890 (same declaration text).

694. def OAI.EditApproximation.FiniteQuery.run line 5906

     Also declared: ComparatorChallenges/EditApproximation.lean:5906 (same declaration text).

695. def OAI.EditApproximation.FiniteQuery.bind line 5915

     Also declared: ComparatorChallenges/EditApproximation.lean:5915 (same declaration text).

696. def OAI.EditApproximation.FiniteQuery.mapKeys line 5919

     Also declared: ComparatorChallenges/EditApproximation.lean:5919 (same declaration text).

697. def OAI.EditApproximation.FiniteQuery.restrict line 5923

     Also declared: ComparatorChallenges/EditApproximation.lean:5923 (same declaration text).

698. def OAI.EditApproximation.FiniteQuery.requestWork line 5929

     Also declared: ComparatorChallenges/EditApproximation.lean:5929 (same declaration text).

699. def OAI.EditApproximation.FiniteQuery.collect line 5936

     Also declared: ComparatorChallenges/EditApproximation.lean:5936 (same declaration text).

700. def OAI.EditApproximation.physicalInitialQuery line 5951

     Also declared: ComparatorChallenges/EditApproximation.lean:5951 (same declaration text).

701. def OAI.EditApproximation.queryInitialGather line 5965

     Also declared: ComparatorChallenges/EditApproximation.lean:5965 (same declaration text).

702. def OAI.EditApproximation.queryBandGather line 5973

     Also declared: ComparatorChallenges/EditApproximation.lean:5973 (same declaration text).

703. def OAI.EditApproximation.physicalRefinementMassQuery line 5983

     Also declared: ComparatorChallenges/EditApproximation.lean:5983 (same declaration text).

704. def OAI.EditApproximation.physicalMedianSeedQuery line 5993

     Also declared: ComparatorChallenges/EditApproximation.lean:5993 (same declaration text).

705. def OAI.EditApproximation.globalSeedRead line 6001

     Also declared: ComparatorChallenges/EditApproximation.lean:6001 (same declaration text).

706. def OAI.EditApproximation.UnreducedRational.value line 6021

     Also declared: ComparatorChallenges/EditApproximation.lean:6021 (same declaration text).

707. def OAI.EditApproximation.UnreducedRational.zero line 6023

     Also declared: ComparatorChallenges/EditApproximation.lean:6023 (same declaration text).

708. def OAI.EditApproximation.UnreducedRational.mul line 6025

     Also declared: ComparatorChallenges/EditApproximation.lean:6025 (same declaration text).

709. def OAI.EditApproximation.UnreducedRational.lt line 6028

     Also declared: ComparatorChallenges/EditApproximation.lean:6028 (same declaration text).

710. def OAI.EditApproximation.UnreducedRational.inv line 6030

     Also declared: ComparatorChallenges/EditApproximation.lean:6030 (same declaration text).

711. def OAI.EditApproximation.UnreducedRational.div line 6034

     Also declared: ComparatorChallenges/EditApproximation.lean:6034 (same declaration text).

712. inductive OAI.EditApproximation.CoarseSourceTree line 6045

     Also declared: ComparatorChallenges/EditApproximation.lean:6045 (same declaration text).

713. def OAI.EditApproximation.coarseTargetFrame line 6049

     Also declared: ComparatorChallenges/EditApproximation.lean:6049 (same declaration text).

714. def OAI.EditApproximation.coarseRootShift line 6052

     Also declared: ComparatorChallenges/EditApproximation.lean:6052 (same declaration text).

715. def OAI.EditApproximation.endpointActionConnection line 6054

     Also declared: ComparatorChallenges/EditApproximation.lean:6054 (same declaration text).

716. def OAI.EditApproximation.coarseSourceTreeOfList line 6058

     Also declared: ComparatorChallenges/EditApproximation.lean:6058 (same declaration text).

717. def OAI.EditApproximation.BinaryFraction.groupIndexWithWork line 6073

     Also declared: ComparatorChallenges/EditApproximation.lean:6073 (same declaration text).

718. def OAI.EditApproximation.BinaryFraction.endpointDistanceWithWork line 6079

     Also declared: ComparatorChallenges/EditApproximation.lean:6079 (same declaration text).

719. def OAI.EditApproximation.BinaryFraction.endpointConnectionWithWork line 6086

     Also declared: ComparatorChallenges/EditApproximation.lean:6086 (same declaration text).

720. def OAI.EditApproximation.BinaryFraction.stateGapWithWork line 6091

     Also declared: ComparatorChallenges/EditApproximation.lean:6091 (same declaration text).

721. def OAI.EditApproximation.BinaryFraction.groupScaleSourceWithWork line 6105

     Also declared: ComparatorChallenges/EditApproximation.lean:6105 (same declaration text).

722. def OAI.EditApproximation.BinaryFraction.endpointScoreReadWithWork line 6113

     Also declared: ComparatorChallenges/EditApproximation.lean:6113 (same declaration text).

723. def OAI.EditApproximation.BinaryFraction.initialConeWithWork line 6122

     Also declared: ComparatorChallenges/EditApproximation.lean:6122 (same declaration text).

724. def OAI.EditApproximation.BinaryFraction.endpointActionWithWork line 6131

     Also declared: ComparatorChallenges/EditApproximation.lean:6131 (same declaration text).

725. def OAI.EditApproximation.BinaryFraction.endpointScoreReadAllocation line 6137

     Also declared: ComparatorChallenges/EditApproximation.lean:6137 (same declaration text).

726. def OAI.EditApproximation.BinaryFraction.initialConeAllocation line 6145

     Also declared: ComparatorChallenges/EditApproximation.lean:6145 (same declaration text).

727. def OAI.EditApproximation.BinaryFraction.groupScaleSourceAllocation line 6154

     Also declared: ComparatorChallenges/EditApproximation.lean:6154 (same declaration text).

728. def OAI.EditApproximation.BinaryFraction.gapGuardAllocation line 6165

     Also declared: ComparatorChallenges/EditApproximation.lean:6165 (same declaration text).

729. def OAI.EditApproximation.BinaryFraction.wideMinimumReadWithWork line 6174

     Also declared: ComparatorChallenges/EditApproximation.lean:6174 (same declaration text).

730. def OAI.EditApproximation.BinaryFraction.groupMemberSourceWithWork line 6182

     Also declared: ComparatorChallenges/EditApproximation.lean:6182 (same declaration text).

731. def OAI.EditApproximation.BinaryFraction.wideActionsFromRepresentativesWithWork line 6191

     Also declared: ComparatorChallenges/EditApproximation.lean:6191 (same declaration text).

732. def OAI.EditApproximation.BinaryFraction.initialConeReadWithWork line 6199

     Also declared: ComparatorChallenges/EditApproximation.lean:6199 (same declaration text).

733. def OAI.EditApproximation.BinaryFraction.wideMinimumReadAllocation line 6206

     Also declared: ComparatorChallenges/EditApproximation.lean:6206 (same declaration text).

734. def OAI.EditApproximation.BinaryFraction.groupMemberSourceAllocation line 6216

     Also declared: ComparatorChallenges/EditApproximation.lean:6216 (same declaration text).

735. def OAI.EditApproximation.BinaryFraction.wideActionsFromRepresentativesAllocation line 6225

     Also declared: ComparatorChallenges/EditApproximation.lean:6225 (same declaration text).

736. def OAI.EditApproximation.BinaryFraction.representativeFromActionsReadWithWork line 6235

     Also declared: ComparatorChallenges/EditApproximation.lean:6235 (same declaration text).

737. def OAI.EditApproximation.BinaryFraction.physicalContinuationReadWithWork line 6249

     Also declared: ComparatorChallenges/EditApproximation.lean:6249 (same declaration text).

738. def OAI.EditApproximation.BinaryFraction.initialMinimumReadWithWork line 6261

     Also declared: ComparatorChallenges/EditApproximation.lean:6261 (same declaration text).

739. def OAI.EditApproximation.BinaryFraction.localWarmupReadKernelWithWork line 6275

     Also declared: ComparatorChallenges/EditApproximation.lean:6275 (same declaration text).

740. def OAI.EditApproximation.BinaryFraction.representativeFromActionsReadAllocation line 6286

     Also declared: ComparatorChallenges/EditApproximation.lean:6286 (same declaration text).

741. def OAI.EditApproximation.BinaryFraction.physicalContinuationReadAllocation line 6300

     Also declared: ComparatorChallenges/EditApproximation.lean:6300 (same declaration text).

742. def OAI.EditApproximation.BinaryFraction.localWarmupReadAllocation line 6311

     Also declared: ComparatorChallenges/EditApproximation.lean:6311 (same declaration text).

743. def OAI.EditApproximation.BinaryFraction.preparedRepresentativeReadWithWork line 6322

     Also declared: ComparatorChallenges/EditApproximation.lean:6322 (same declaration text).

744. def OAI.EditApproximation.BinaryFraction.initialProgramReadWithWork line 6330

     Also declared: ComparatorChallenges/EditApproximation.lean:6330 (same declaration text).

745. def OAI.EditApproximation.BinaryFraction.preparedRepresentativeReadAllocation line 6336

     Also declared: ComparatorChallenges/EditApproximation.lean:6336 (same declaration text).

746. def OAI.EditApproximation.BinaryFraction.queryRefinementFinishAllocation line 6344

     Also declared: ComparatorChallenges/EditApproximation.lean:6344 (same declaration text).

747. def OAI.EditApproximation.BinaryFraction.queryOnlineRangeWithWork line 6358

     Also declared: ComparatorChallenges/EditApproximation.lean:6358 (same declaration text).

748. def OAI.EditApproximation.BinaryFraction.cachedInitialProgramReadWithWork line 6370

     Also declared: ComparatorChallenges/EditApproximation.lean:6370 (same declaration text).

749. def OAI.EditApproximation.BinaryFraction.queryOnlineRangeAllocation line 6375

     Also declared: ComparatorChallenges/EditApproximation.lean:6375 (same declaration text).

750. def OAI.EditApproximation.PositionCounts.count line 6398

     Also declared: ComparatorChallenges/EditApproximation.lean:6398 (same declaration text).

751. def OAI.EditApproximation.PositionCounts.left line 6402

     Also declared: ComparatorChallenges/EditApproximation.lean:6402 (same declaration text).

752. def OAI.EditApproximation.PositionCounts.right line 6406

     Also declared: ComparatorChallenges/EditApproximation.lean:6406 (same declaration text).

753. def OAI.EditApproximation.PositionCounts.storageBits line 6410

     Also declared: ComparatorChallenges/EditApproximation.lean:6410 (same declaration text).

754. def OAI.EditApproximation.PositionCounts.add line 6414

     Also declared: ComparatorChallenges/EditApproximation.lean:6414 (same declaration text).

755. def OAI.EditApproximation.PositionCounts.addWithWork line 6421

     Also declared: ComparatorChallenges/EditApproximation.lean:6421 (same declaration text).

756. def OAI.EditApproximation.PositionCounts.prefixWithWork line 6431

     Also declared: ComparatorChallenges/EditApproximation.lean:6431 (same declaration text).

757. def OAI.EditApproximation.BitQuery.Footprint.bind line 6450

     Also declared: ComparatorChallenges/EditApproximation.lean:6450 (same declaration text).

758. def OAI.EditApproximation.BitQuery.Footprint.compute line 6458

     Also declared: ComparatorChallenges/EditApproximation.lean:6458 (same declaration text).

759. def OAI.EditApproximation.BitQuery.Footprint.chargeOf line 6462

     Also declared: ComparatorChallenges/EditApproximation.lean:6462 (same declaration text).

760. def OAI.EditApproximation.BitQuery.Footprint.runCells line 6466

     Also declared: ComparatorChallenges/EditApproximation.lean:6466 (same declaration text).

761. def OAI.EditApproximation.BitQuery.Footprint.computeOf line 6476

     Also declared: ComparatorChallenges/EditApproximation.lean:6476 (same declaration text).

762. def OAI.EditApproximation.BitQuery.Footprint.collect line 6480

     Also declared: ComparatorChallenges/EditApproximation.lean:6480 (same declaration text).

763. def OAI.EditApproximation.BitQuery.Footprint.mapKeysWithWork line 6490

     Also declared: ComparatorChallenges/EditApproximation.lean:6490 (same declaration text).

764. def OAI.EditApproximation.BitQuery.Footprint.restrictWithWork line 6499

     Also declared: ComparatorChallenges/EditApproximation.lean:6499 (same declaration text).

765. def OAI.EditApproximation.BitQuery.Footprint.normalize line 6514

     Also declared: ComparatorChallenges/EditApproximation.lean:6514 (same declaration text).

766. def OAI.EditApproximation.bandActionPredicate line 6529

     Also declared: ComparatorChallenges/EditApproximation.lean:6529 (same declaration text).

767. def OAI.EditApproximation.queryOnlineSourceGather line 6541

     Also declared: ComparatorChallenges/EditApproximation.lean:6541 (same declaration text).

768. def OAI.EditApproximation.coarseLabelChildren line 6553

     Also declared: ComparatorChallenges/EditApproximation.lean:6553 (same declaration text).

769. instance OAI.EditApproximation.bandActionPredicateDecidable line 6561

     Also declared: ComparatorChallenges/EditApproximation.lean:6561 (same declaration text).

770. def OAI.EditApproximation.computedBandActions line 6569

     Also declared: ComparatorChallenges/EditApproximation.lean:6569 (same declaration text).

771. def OAI.EditApproximation.rationalEndpointActionValue line 6587

     Also declared: ComparatorChallenges/EditApproximation.lean:6587 (same declaration text).

772. def OAI.EditApproximation.rationalActualWideActions line 6591

     Also declared: ComparatorChallenges/EditApproximation.lean:6591 (same declaration text).

773. def OAI.EditApproximation.groupQueriedChildLabels line 6597

     Also declared: ComparatorChallenges/EditApproximation.lean:6597 (same declaration text).

774. def OAI.EditApproximation.rationalWideActionMinimum line 6601

     Also declared: ComparatorChallenges/EditApproximation.lean:6601 (same declaration text).

775. def OAI.EditApproximation.groupCurrentInputCover line 6607

     Also declared: ComparatorChallenges/EditApproximation.lean:6607 (same declaration text).

776. def OAI.EditApproximation.representativeBandActions line 6613

     Also declared: ComparatorChallenges/EditApproximation.lean:6613 (same declaration text).

777. structure OAI.EditApproximation.UnskippedBand line 6624

     Also declared: ComparatorChallenges/EditApproximation.lean:6624 (same declaration text).

778. def OAI.EditApproximation.keyedOnlineBandG line 6643

     Also declared: ComparatorChallenges/EditApproximation.lean:6643 (same declaration text).

779. def OAI.EditApproximation.testUnskippedBand line 6649

     Also declared: ComparatorChallenges/EditApproximation.lean:6649 (same declaration text).

780. def OAI.EditApproximation.unskippedBandList line 6668

     Also declared: ComparatorChallenges/EditApproximation.lean:6668 (same declaration text).

781. def OAI.EditApproximation.keyedOnlineCandidate line 6675

     Also declared: ComparatorChallenges/EditApproximation.lean:6675 (same declaration text).

782. def OAI.EditApproximation.cellUnskippedBands line 6720

     Also declared: ComparatorChallenges/EditApproximation.lean:6720 (same declaration text).

783. def OAI.EditApproximation.localOnlineCandidates line 6728

     Also declared: ComparatorChallenges/EditApproximation.lean:6728 (same declaration text).

784. def OAI.EditApproximation.BinaryMemo.value line 6751

     Also declared: ComparatorChallenges/EditApproximation.lean:6751 (same declaration text).

785. def OAI.EditApproximation.BinaryMemo.left line 6755

     Also declared: ComparatorChallenges/EditApproximation.lean:6755 (same declaration text).

786. def OAI.EditApproximation.BinaryMemo.right line 6759

     Also declared: ComparatorChallenges/EditApproximation.lean:6759 (same declaration text).

787. def OAI.EditApproximation.BinaryMemo.lookup line 6763

     Also declared: ComparatorChallenges/EditApproximation.lean:6763 (same declaration text).

788. def OAI.EditApproximation.BinaryMemo.insert line 6768

     Also declared: ComparatorChallenges/EditApproximation.lean:6768 (same declaration text).

789. def OAI.EditApproximation.BinaryMemo.lookupCosted line 6773

     Also declared: ComparatorChallenges/EditApproximation.lean:6773 (same declaration text).

790. def OAI.EditApproximation.BinaryMemo.insertCosted line 6782

     Also declared: ComparatorChallenges/EditApproximation.lean:6782 (same declaration text).

791. def OAI.EditApproximation.rankedMemoEvaluate line 6800

     Also declared: ComparatorChallenges/EditApproximation.lean:6800 (same declaration text).

792. def OAI.EditApproximation.localWarmupStepQuery line 6815

     Also declared: ComparatorChallenges/EditApproximation.lean:6815 (same declaration text).

793. def OAI.EditApproximation.keyedOnlineSourceRange line 6829

     Also declared: ComparatorChallenges/EditApproximation.lean:6829 (same declaration text).

794. def OAI.EditApproximation.occurrenceBuild line 6834

     Also declared: ComparatorChallenges/EditApproximation.lean:6834 (same declaration text).

795. def OAI.EditApproximation.occurrenceBuildWithWork line 6842

     Also declared: ComparatorChallenges/EditApproximation.lean:6842 (same declaration text).

796. def OAI.EditApproximation.occurrenceQueryWithWork line 6853

     Also declared: ComparatorChallenges/EditApproximation.lean:6853 (same declaration text).

797. def OAI.EditApproximation.rankedBitMemoEvaluate line 6862

     Also declared: ComparatorChallenges/EditApproximation.lean:6862 (same declaration text).

798. def OAI.EditApproximation.physicalWarmupStepQuery line 6878

     Also declared: ComparatorChallenges/EditApproximation.lean:6878 (same declaration text).

799. def OAI.EditApproximation.indexedSingletonCostWithWork line 6886

     Also declared: ComparatorChallenges/EditApproximation.lean:6886 (same declaration text).

800. def OAI.EditApproximation.integerOccurrenceIndex line 6892

     Also declared: ComparatorChallenges/EditApproximation.lean:6892 (same declaration text).

801. def OAI.EditApproximation.integerOccurrenceBuildWithWork line 6896

     Also declared: ComparatorChallenges/EditApproximation.lean:6896 (same declaration text).

802. def OAI.EditApproximation.rankedMemoAddressWork line 6900

     Also declared: ComparatorChallenges/EditApproximation.lean:6900 (same declaration text).

803. def OAI.EditApproximation.rankedMemoKernelWork line 6912

     Also declared: ComparatorChallenges/EditApproximation.lean:6912 (same declaration text).

804. def OAI.EditApproximation.physicalWarmupRequestQuery line 6924

     Also declared: ComparatorChallenges/EditApproximation.lean:6924 (same declaration text).

805. abbrev OAI.EditApproximation.PhysicalLocalOnlineKey line 6952

     Also declared: ComparatorChallenges/EditApproximation.lean:6952 (same declaration text).

806. abbrev OAI.EditApproximation.ClampedPhysicalSeed line 6955

     Also declared: ComparatorChallenges/EditApproximation.lean:6955 (same declaration text).

807. def OAI.EditApproximation.finalTargetState line 6957

     Also declared: ComparatorChallenges/EditApproximation.lean:6957 (same declaration text).

808. abbrev OAI.EditApproximation.PhysicalCommonKey line 6959

     Also declared: ComparatorChallenges/EditApproximation.lean:6959 (same declaration text).

809. def OAI.EditApproximation.clampedSeedNat line 6963

     Also declared: ComparatorChallenges/EditApproximation.lean:6963 (same declaration text).

810. def OAI.EditApproximation.triangularChoiceWithWork line 6976

     Also declared: ComparatorChallenges/EditApproximation.lean:6976 (same declaration text).

811. def OAI.EditApproximation.triangularChoiceAllocation line 7219

     Also declared: ComparatorChallenges/EditApproximation.lean:7219 (same declaration text).

812. def OAI.EditApproximation.BinaryFraction.coordinateVectorWithWork line 7473

     Also declared: ComparatorChallenges/EditApproximation.lean:7473 (same declaration text).

813. def OAI.EditApproximation.BinaryFraction.reduceOnlineIntegerWithWork line 7570

     Also declared: ComparatorChallenges/EditApproximation.lean:7570 (same declaration text).

814. def OAI.EditApproximation.BinaryFraction.countedPreparedActionReadWithWork line 7822

     Also declared: ComparatorChallenges/EditApproximation.lean:7822 (same declaration text).

815. def OAI.EditApproximation.BinaryFraction.countedPreparedActionKernelAllocation line 7833

     Also declared: ComparatorChallenges/EditApproximation.lean:7833 (same declaration text).

816. def OAI.EditApproximation.BinaryFraction.countedBandActionReadWithWork line 7845

     Also declared: ComparatorChallenges/EditApproximation.lean:7845 (same declaration text).

817. def OAI.EditApproximation.BinaryFraction.countedPreparedActionAllocation line 7854

     Also declared: ComparatorChallenges/EditApproximation.lean:7854 (same declaration text).

818. def OAI.EditApproximation.BinaryFraction.countedSampledOnlineReadWithWork line 7860

     Also declared: ComparatorChallenges/EditApproximation.lean:7860 (same declaration text).

819. def OAI.EditApproximation.BinaryFraction.countedBandActionAllocation line 7871

     Also declared: ComparatorChallenges/EditApproximation.lean:7871 (same declaration text).

820. def OAI.EditApproximation.BinaryFraction.countedSampledOnlineAllocation line 7881

     Also declared: ComparatorChallenges/EditApproximation.lean:7881 (same declaration text).

821. def OAI.EditApproximation.SourceRanked.rank line 7901

     Also declared: ComparatorChallenges/EditApproximation.lean:7901 (same declaration text).

822. def OAI.EditApproximation.SourceRanked.keyCode line 7905

     Also declared: ComparatorChallenges/EditApproximation.lean:7905 (same declaration text).

823. def OAI.EditApproximation.SourceRanked.child line 7909

     Also declared: ComparatorChallenges/EditApproximation.lean:7909 (same declaration text).

824. def OAI.EditApproximation.SourceRanked.body line 7915

     Also declared: ComparatorChallenges/EditApproximation.lean:7915 (same declaration text).

825. def OAI.EditApproximation.SourceRanked.bitBody line 7923

     Also declared: ComparatorChallenges/EditApproximation.lean:7923 (same declaration text).

826. def OAI.EditApproximation.ChargedPhysicalRequest.depth line 7940

     Also declared: ComparatorChallenges/EditApproximation.lean:7940 (same declaration text).

827. def OAI.EditApproximation.ChargedPhysicalRequest.index line 7944

     Also declared: ComparatorChallenges/EditApproximation.lean:7944 (same declaration text).

828. def OAI.EditApproximation.ChargedPhysicalRequest.rank line 7948

     Also declared: ComparatorChallenges/EditApproximation.lean:7948 (same declaration text).

829. def OAI.EditApproximation.chargedPreviousRead line 7961

     Also declared: ComparatorChallenges/EditApproximation.lean:7961 (same declaration text).

830. def OAI.EditApproximation.chargedWarmupChild line 8003

     Also declared: ComparatorChallenges/EditApproximation.lean:8003 (same declaration text).

831. def OAI.EditApproximation.chargedSeedQuery line 8051

     Also declared: ComparatorChallenges/EditApproximation.lean:8051 (same declaration text).

832. def OAI.EditApproximation.chargedWarmupQuery line 8072

     Also declared: ComparatorChallenges/EditApproximation.lean:8072 (same declaration text).

833. abbrev OAI.EditApproximation.coarseEntryWidth line 8100

     Also declared: ComparatorChallenges/EditApproximation.lean:8100 (same declaration text).

834. abbrev OAI.EditApproximation.CoarseGuessIndex line 8102

     Also declared: ComparatorChallenges/EditApproximation.lean:8102 (same declaration text).

835. def OAI.EditApproximation.coarseGuess line 8104

     Also declared: ComparatorChallenges/EditApproximation.lean:8104 (same declaration text).

836. def OAI.EditApproximation.coarseEntryTree line 8106

     Also declared: ComparatorChallenges/EditApproximation.lean:8106 (same declaration text).

837. def OAI.EditApproximation.coarseInitialMeasure line 8109

     Also declared: ComparatorChallenges/EditApproximation.lean:8109 (same declaration text).

838. def OAI.EditApproximation.coarseActiveChildrenWork line 8123

     Also declared: ComparatorChallenges/EditApproximation.lean:8123 (same declaration text).

839. abbrev OAI.EditApproximation.CoarseFullSeedDraws line 8132

     Also declared: ComparatorChallenges/EditApproximation.lean:8132 (same declaration text).

840. def OAI.EditApproximation.coarseFullSeedMeasure line 8135

     Also declared: ComparatorChallenges/EditApproximation.lean:8135 (same declaration text).

841. def OAI.EditApproximation.rejectionAcceptedLaw line 8151

     Also declared: ComparatorChallenges/EditApproximation.lean:8151 (same declaration text).

842. abbrev OAI.EditApproximation.RejectionRuntimeArray line 8154

     Also declared: ComparatorChallenges/EditApproximation.lean:8154 (same declaration text).

843. def OAI.EditApproximation.BinaryMemo.fractionStorage line 8165

     Also declared: ComparatorChallenges/EditApproximation.lean:8165 (same declaration text).

844. def OAI.EditApproximation.BinaryMemo.valueStorage line 8171

     Also declared: ComparatorChallenges/EditApproximation.lean:8171 (same declaration text).

845. def OAI.EditApproximation.indexedLeafWithWork line 8184

     Also declared: ComparatorChallenges/EditApproximation.lean:8184 (same declaration text).

846. def OAI.EditApproximation.integerOccurrenceStorage line 8190

     Also declared: ComparatorChallenges/EditApproximation.lean:8190 (same declaration text).

847. def OAI.EditApproximation.integerStoredDataSpace line 8193

     Also declared: ComparatorChallenges/EditApproximation.lean:8193 (same declaration text).

848. def OAI.EditApproximation.binaryIndexedLeafWithWork line 8207

     Also declared: ComparatorChallenges/EditApproximation.lean:8207 (same declaration text).

849. def OAI.EditApproximation.binaryIndexedLeafAllocation line 8212

     Also declared: ComparatorChallenges/EditApproximation.lean:8212 (same declaration text).

850. def OAI.EditApproximation.queryIndexedSliceWithWork line 8217

     Also declared: ComparatorChallenges/EditApproximation.lean:8217 (same declaration text).

851. def OAI.EditApproximation.queryIndexedSliceAllocation line 8224

     Also declared: ComparatorChallenges/EditApproximation.lean:8224 (same declaration text).

852. def OAI.EditApproximation.BinaryFraction.initialGridReadAllocation line 8239

     Also declared: ComparatorChallenges/EditApproximation.lean:8239 (same declaration text).

853. def OAI.EditApproximation.BinaryFraction.initialConeReadAllocation line 8247

     Also declared: ComparatorChallenges/EditApproximation.lean:8247 (same declaration text).

854. def OAI.EditApproximation.BinaryFraction.initialCentersReadAllocation line 8250

     Also declared: ComparatorChallenges/EditApproximation.lean:8250 (same declaration text).

855. def OAI.EditApproximation.BinaryFraction.initialMinimumReadAllocation line 8259

     Also declared: ComparatorChallenges/EditApproximation.lean:8259 (same declaration text).

856. def OAI.EditApproximation.BinaryFraction.initialProgramReadAllocation line 8273

     Also declared: ComparatorChallenges/EditApproximation.lean:8273 (same declaration text).

857. def OAI.EditApproximation.BinaryFraction.cachedInitialProgramReadAllocation line 8277

     Also declared: ComparatorChallenges/EditApproximation.lean:8277 (same declaration text).

858. def OAI.EditApproximation.BinaryFraction.onlineParametersAllocation line 8290

     Also declared: ComparatorChallenges/EditApproximation.lean:8290 (same declaration text).

859. def OAI.EditApproximation.BinaryFraction.refinementDecrementAllocation line 8293

     Also declared: ComparatorChallenges/EditApproximation.lean:8293 (same declaration text).

860. def OAI.EditApproximation.scheduledRefinementAllocation line 8304

     Also declared: ComparatorChallenges/EditApproximation.lean:8304 (same declaration text).

861. def OAI.EditApproximation.refinementBaseAllocation line 8310

     Also declared: ComparatorChallenges/EditApproximation.lean:8310 (same declaration text).

862. def OAI.EditApproximation.refinementParameterAllocation line 8316

     Also declared: ComparatorChallenges/EditApproximation.lean:8316 (same declaration text).

863. def OAI.EditApproximation.computedQueryPassAllocation line 8320

     Also declared: ComparatorChallenges/EditApproximation.lean:8320 (same declaration text).

864. def OAI.EditApproximation.computedQuerySetupAllocation line 8324

     Also declared: ComparatorChallenges/EditApproximation.lean:8324 (same declaration text).

865. def OAI.EditApproximation.UnreducedRational.nat line 8337

     Also declared: ComparatorChallenges/EditApproximation.lean:8337 (same declaration text).

866. def OAI.EditApproximation.BinaryFraction.countedGroupMemberSourceWithWork line 8349

     Also declared: ComparatorChallenges/EditApproximation.lean:8349 (same declaration text).

867. def OAI.EditApproximation.BinaryFraction.roundedBandReadWithWork line 8724

     Also declared: ComparatorChallenges/EditApproximation.lean:8724 (same declaration text).

868. def OAI.EditApproximation.BinaryFraction.queryGroupLabelsWithWork line 9081

     Also declared: ComparatorChallenges/EditApproximation.lean:9081 (same declaration text).

869. def OAI.EditApproximation.BinaryFraction.queryGroupLabelsAllocation line 9451

     Also declared: ComparatorChallenges/EditApproximation.lean:9451 (same declaration text).

870. def OAI.EditApproximation.BinaryFraction.countedGroupMemberSourceAllocation line 9821

     Also declared: ComparatorChallenges/EditApproximation.lean:9821 (same declaration text).

871. def OAI.EditApproximation.BinaryFraction.unskippedGuardReadWithWork line 10206

     Also declared: ComparatorChallenges/EditApproximation.lean:10206 (same declaration text).

872. def OAI.EditApproximation.BinaryFraction.queryGroupInputsWithWork line 10225

     Also declared: ComparatorChallenges/EditApproximation.lean:10225 (same declaration text).

873. def OAI.EditApproximation.BinaryFraction.coarseIndexedRootWithWork line 10236

     Also declared: ComparatorChallenges/EditApproximation.lean:10236 (same declaration text).

874. def OAI.EditApproximation.BinaryFraction.queryGroupInputsAllocation line 10318

     Also declared: ComparatorChallenges/EditApproximation.lean:10318 (same declaration text).

875. def OAI.EditApproximation.BinaryFraction.unskippedGuardReadAllocation line 10331

     Also declared: ComparatorChallenges/EditApproximation.lean:10331 (same declaration text).

876. def OAI.EditApproximation.BinaryFraction.queryGroupInputsTransportWithWork line 10346

     Also declared: ComparatorChallenges/EditApproximation.lean:10346 (same declaration text).

877. def OAI.EditApproximation.BinaryFraction.coarseIndexedCandidateWithWork line 10353

     Also declared: ComparatorChallenges/EditApproximation.lean:10353 (same declaration text).

878. def OAI.EditApproximation.BinaryFraction.preparedUnskippedReadAllocation line 10363

     Also declared: ComparatorChallenges/EditApproximation.lean:10363 (same declaration text).

879. def OAI.EditApproximation.BinaryFraction.queryGroupInputsTransportAllocation line 10377

     Also declared: ComparatorChallenges/EditApproximation.lean:10377 (same declaration text).

880. def OAI.EditApproximation.BinaryFraction.preparedUnskippedReadWithWorkRaw line 10385

     Also declared: ComparatorChallenges/EditApproximation.lean:10385 (same declaration text).

881. def OAI.EditApproximation.BinaryFraction.coarseIndexedInitialWithWork line 10399

     Also declared: ComparatorChallenges/EditApproximation.lean:10399 (same declaration text).

882. def OAI.EditApproximation.BinaryFraction.unskippedEstimateSourceWithWorkRaw line 10428

     Also declared: ComparatorChallenges/EditApproximation.lean:10428 (same declaration text).

883. def OAI.EditApproximation.BinaryFraction.unskippedEstimateSourceAllocationRaw line 10436

     Also declared: ComparatorChallenges/EditApproximation.lean:10436 (same declaration text).

884. def OAI.EditApproximation.BinaryFraction.chooseUnskippedSourceWithWorkRaw line 10446

     Also declared: ComparatorChallenges/EditApproximation.lean:10446 (same declaration text).

885. def OAI.EditApproximation.BinaryFraction.chooseUnskippedSourceAllocationRaw line 10450

     Also declared: ComparatorChallenges/EditApproximation.lean:10450 (same declaration text).

886. def OAI.EditApproximation.BinaryFraction.sampledGroupActionSourceWithWorkRaw line 10456

     Also declared: ComparatorChallenges/EditApproximation.lean:10456 (same declaration text).

887. def OAI.EditApproximation.BinaryFraction.sampledGroupActionSourceAllocationRaw line 10463

     Also declared: ComparatorChallenges/EditApproximation.lean:10463 (same declaration text).

888. def OAI.EditApproximation.BinaryFraction.preparedOnlineReadWithWorkRaw line 10482

     Also declared: ComparatorChallenges/EditApproximation.lean:10482 (same declaration text).

889. def OAI.EditApproximation.BinaryFraction.preparedOnlineReadAllocationRaw line 10631

     Also declared: ComparatorChallenges/EditApproximation.lean:10631 (same declaration text).

890. inductive OAI.EditDistortion.Step line 10791

     Also declared: ComparatorChallenges/EditApproximation.lean:10791 (same declaration text), ComparatorChallenges/EditDistance.lean:10 (same declaration text).

891. inductive OAI.EditDistortion.Script line 10797

     Distinct definitions of this name: ComparatorChallenges/EditApproximation.lean:10797 (same declaration text), ComparatorChallenges/EditDistance.lean:17 (different declaration text). Qualify references as OAI.EditDistortion.Script@path.

892. def OAI.EditDistortion.edit line 10802

     Also declared: ComparatorChallenges/EditApproximation.lean:10802 (same declaration text), ComparatorChallenges/EditDistance.lean:23 (same declaration text).

893. def OAI.EditDistortion.cost line 10814

     Also declared: ComparatorChallenges/EditApproximation.lean:10814 (same declaration text).

894. def OAI.EditApproximation.CoarseSourceTree.word line 10825

     Also declared: ComparatorChallenges/EditApproximation.lean:10825 (same declaration text).

895. def OAI.EditApproximation.coarseLabelCount line 10838

     Also declared: ComparatorChallenges/EditApproximation.lean:10838 (same declaration text).

896. def OAI.EditApproximation.coarseIndexedEntryBinaryCost line 10848

     Also declared: ComparatorChallenges/EditApproximation.lean:10848 (same declaration text).

897. def OAI.EditApproximation.coarseInitialLabelCount line 10854

     Also declared: ComparatorChallenges/EditApproximation.lean:10854 (same declaration text).

898. def OAI.EditApproximation.coarseChildrenCost line 10871

     Also declared: ComparatorChallenges/EditApproximation.lean:10871 (same declaration text).

899. def OAI.EditApproximation.coarseShiftCost line 10879

     Also declared: ComparatorChallenges/EditApproximation.lean:10879 (same declaration text).

900. instance OAI.EditApproximation.targetIntervalFintype line 10898

     Also declared: ComparatorChallenges/EditApproximation.lean:10898 (same declaration text).

901. def OAI.EditApproximation.UnskippedBand.actions line 10917

     Also declared: ComparatorChallenges/EditApproximation.lean:10917 (same declaration text).

902. def OAI.EditApproximation.UnskippedBand.envelope line 10924

     Also declared: ComparatorChallenges/EditApproximation.lean:10924 (same declaration text).

903. def OAI.EditApproximation.UnskippedBand.rounded line 10930

     Also declared: ComparatorChallenges/EditApproximation.lean:10930 (same declaration text).

904. def OAI.EditApproximation.UnskippedBand.rationalAction line 10937

     Also declared: ComparatorChallenges/EditApproximation.lean:10937 (same declaration text).

905. def OAI.EditApproximation.unskippedGroupEstimate line 10954

     Also declared: ComparatorChallenges/EditApproximation.lean:10954 (same declaration text).

906. def OAI.EditApproximation.groupDyadicScaleAt line 10971

     Also declared: ComparatorChallenges/EditApproximation.lean:10971 (same declaration text).

907. abbrev OAI.EditApproximation.CellGroupDraws line 10983

     Also declared: ComparatorChallenges/EditApproximation.lean:10983 (same declaration text).

908. abbrev OAI.EditApproximation.cellScaleReadDraw line 10987

     Also declared: ComparatorChallenges/EditApproximation.lean:10987 (same declaration text).

909. abbrev OAI.EditApproximation.GroupScalarKey line 10991

     Also declared: ComparatorChallenges/EditApproximation.lean:10991 (same declaration text).

910. abbrev OAI.EditApproximation.CountedCellGroupDraws line 10995

     Also declared: ComparatorChallenges/EditApproximation.lean:10995 (same declaration text).

911. abbrev OAI.EditApproximation.CellGroupSourceAllocations line 10999

     Also declared: ComparatorChallenges/EditApproximation.lean:10999 (same declaration text).

912. abbrev OAI.EditApproximation.CountedCellGroupAllocations line 11003

     Also declared: ComparatorChallenges/EditApproximation.lean:11003 (same declaration text).

913. abbrev OAI.EditApproximation.CellGroupReadDraws line 11007

     Also declared: ComparatorChallenges/EditApproximation.lean:11007 (same declaration text).

914. def OAI.EditApproximation.groupScalarKeys line 11010

     Also declared: ComparatorChallenges/EditApproximation.lean:11010 (same declaration text).

915. def OAI.EditApproximation.groupDrawFromValues line 11017

     Also declared: ComparatorChallenges/EditApproximation.lean:11017 (same declaration text).

916. def OAI.EditApproximation.queryGroupKeyEqualWithWork line 11022

     Also declared: ComparatorChallenges/EditApproximation.lean:11022 (same declaration text).

917. def OAI.EditApproximation.queryGroupKeyEqualAllocation line 11031

     Also declared: ComparatorChallenges/EditApproximation.lean:11031 (same declaration text).

918. def OAI.EditApproximation.BinaryFraction.queryGroupKeySamplesWithWork line 11046

     Also declared: ComparatorChallenges/EditApproximation.lean:11046 (same declaration text).

919. def OAI.EditApproximation.BinaryFraction.querySharedCellInputsWithWork line 11479

     Also declared: ComparatorChallenges/EditApproximation.lean:11479 (same declaration text).

920. def OAI.EditApproximation.BinaryFraction.groupKeySampleBlock line 11583

     Also declared: ComparatorChallenges/EditApproximation.lean:11583 (same declaration text).

921. def OAI.EditApproximation.BinaryFraction.groupKeySampleBlockAllocation line 11960

     Also declared: ComparatorChallenges/EditApproximation.lean:11960 (same declaration text).

922. def OAI.EditApproximation.BinaryFraction.querySharedCellInputsAllocation line 12336

     Also declared: ComparatorChallenges/EditApproximation.lean:12336 (same declaration text).

923. def OAI.EditApproximation.BinaryFraction.queryGroupKeySamplesAllocation line 12446

     Also declared: ComparatorChallenges/EditApproximation.lean:12446 (same declaration text).

924. def OAI.EditApproximation.BinaryFraction.querySharedInputsWithWork line 12543

     Also declared: ComparatorChallenges/EditApproximation.lean:12543 (same declaration text).

925. def OAI.EditApproximation.BinaryFraction.queryGroupDrawReadWithWork line 12558

     Also declared: ComparatorChallenges/EditApproximation.lean:12558 (same declaration text).

926. def OAI.EditApproximation.BinaryFraction.queryGroupSourceKeysWithWork line 12741

     Also declared: ComparatorChallenges/EditApproximation.lean:12741 (same declaration text).

927. def OAI.EditApproximation.BinaryFraction.queryGroupDrawReadAllocation line 12754

     Also declared: ComparatorChallenges/EditApproximation.lean:12754 (same declaration text).

928. def OAI.EditApproximation.BinaryFraction.queryGroupSourceKeysAllocation line 12764

     Also declared: ComparatorChallenges/EditApproximation.lean:12764 (same declaration text).

929. def OAI.EditApproximation.BinaryFraction.querySharedInputsAllocation line 12781

     Also declared: ComparatorChallenges/EditApproximation.lean:12781 (same declaration text).

930. def OAI.EditApproximation.BinaryFraction.preparedCellGroupSourceAllocationRaw line 12805

     Also declared: ComparatorChallenges/EditApproximation.lean:12805 (same declaration text).

931. def OAI.EditApproximation.BinaryFraction.preparedCellGroupSourceWithWorkRaw line 12843

     Also declared: ComparatorChallenges/EditApproximation.lean:12843 (same declaration text).

932. def OAI.EditApproximation.querySharedInputCover line 12880

     Also declared: ComparatorChallenges/EditApproximation.lean:12880 (same declaration text).

933. def OAI.EditApproximation.coarseThresholdChildrenCost line 12889

     Also declared: ComparatorChallenges/EditApproximation.lean:12889 (same declaration text).

934. def OAI.EditApproximation.coarseThresholdEstimate line 12902

     Also declared: ComparatorChallenges/EditApproximation.lean:12902 (same declaration text).

935. abbrev OAI.EditApproximation.PhysicalScalarIndex line 12923

     Also declared: ComparatorChallenges/EditApproximation.lean:12923 (same declaration text).

936. def OAI.EditApproximation.computedPhysicalCoarseDepth line 12932

     Also declared: ComparatorChallenges/EditApproximation.lean:12932 (same declaration text).

937. abbrev OAI.EditApproximation.PhysicalScalarKey line 12938

     Also declared: ComparatorChallenges/EditApproximation.lean:12938 (same declaration text).

938. instance OAI.EditApproximation.physicalScalarIndexFintype line 12941

     Also declared: ComparatorChallenges/EditApproximation.lean:12941 (same declaration text).

939. def OAI.EditApproximation.physicalScalarRange line 12946

     Also declared: ComparatorChallenges/EditApproximation.lean:12946 (same declaration text).

940. instance OAI.EditApproximation.physicalScalarRangeNeZero line 12952

     Also declared: ComparatorChallenges/EditApproximation.lean:12952 (same declaration text).

941. def OAI.EditApproximation.queryGroupSourceGather line 12967

     Also declared: ComparatorChallenges/EditApproximation.lean:12967 (same declaration text).

942. def OAI.EditApproximation.physicalScalarCodeWithWork line 12977

     Also declared: ComparatorChallenges/EditApproximation.lean:12977 (same declaration text).

943. def OAI.EditApproximation.physicalScalarCodeAllocation line 12996

     Also declared: ComparatorChallenges/EditApproximation.lean:12996 (same declaration text).

944. abbrev OAI.EditApproximation.PhysicalGroupQueries line 13011

     Also declared: ComparatorChallenges/EditApproximation.lean:13011 (same declaration text).

945. def OAI.EditApproximation.physicalScalarOnlineRead line 13016

     Also declared: ComparatorChallenges/EditApproximation.lean:13016 (same declaration text).

946. def OAI.EditApproximation.physicalScalarGroupQueriesAt line 13025

     Also declared: ComparatorChallenges/EditApproximation.lean:13025 (same declaration text).

947. abbrev OAI.EditApproximation.BitPhysicalGroupQueries line 13038

     Also declared: ComparatorChallenges/EditApproximation.lean:13038 (same declaration text).

948. def OAI.EditApproximation.queryPhysicalScalarRead line 13043

     Also declared: ComparatorChallenges/EditApproximation.lean:13043 (same declaration text).

949. def OAI.EditApproximation.queryPhysicalScalarGroupQueriesAt line 13047

     Also declared: ComparatorChallenges/EditApproximation.lean:13047 (same declaration text).

950. def OAI.EditApproximation.dyadicUnskippedGroupEstimate line 13062

     Also declared: ComparatorChallenges/EditApproximation.lean:13062 (same declaration text).

951. def OAI.EditApproximation.chooseUnskippedGroup line 13070

     Also declared: ComparatorChallenges/EditApproximation.lean:13070 (same declaration text).

952. def OAI.EditApproximation.chooseCellGroupAction line 13088

     Also declared: ComparatorChallenges/EditApproximation.lean:13088 (same declaration text).

953. def OAI.EditApproximation.localCellGroupActions line 13108

     Also declared: ComparatorChallenges/EditApproximation.lean:13108 (same declaration text).

954. def OAI.EditApproximation.localRefinementStepQuery line 13124

     Also declared: ComparatorChallenges/EditApproximation.lean:13124 (same declaration text).

955. def OAI.EditApproximation.localOnlineSourceStepQuery line 13181

     Also declared: ComparatorChallenges/EditApproximation.lean:13181 (same declaration text).

956. def OAI.EditApproximation.queryRefinementGather line 13206

     Also declared: ComparatorChallenges/EditApproximation.lean:13206 (same declaration text).

957. def OAI.EditApproximation.BinaryFraction.queryRefinementFinishWithWork line 13228

     Also declared: ComparatorChallenges/EditApproximation.lean:13228 (same declaration text).

958. def OAI.EditApproximation.localRandomSourceStepQuery line 13246

     Also declared: ComparatorChallenges/EditApproximation.lean:13246 (same declaration text).

959. def OAI.EditApproximation.localRandomBandDataQuery line 13261

     Also declared: ComparatorChallenges/EditApproximation.lean:13261 (same declaration text).

960. def OAI.EditApproximation.localRandomDataQuery line 13278

     Also declared: ComparatorChallenges/EditApproximation.lean:13278 (same declaration text).

961. def OAI.EditApproximation.physicalScalarCode line 13294

     Also declared: ComparatorChallenges/EditApproximation.lean:13294 (same declaration text).

962. def OAI.EditApproximation.physicalScalarGroupQueries line 13312

     Also declared: ComparatorChallenges/EditApproximation.lean:13312 (same declaration text).

963. def OAI.EditApproximation.physicalScalarGroupRead line 13337

     Also declared: ComparatorChallenges/EditApproximation.lean:13337 (same declaration text).

964. def OAI.EditApproximation.physicalRandomDataRequestQuery line 13350

     Also declared: ComparatorChallenges/EditApproximation.lean:13350 (same declaration text).

965. def OAI.EditApproximation.physicalInactiveGlobalQuery line 13380

     Also declared: ComparatorChallenges/EditApproximation.lean:13380 (same declaration text).

966. def OAI.EditApproximation.physicalRandomGlobalQuery line 13400

     Also declared: ComparatorChallenges/EditApproximation.lean:13400 (same declaration text).

967. def OAI.EditApproximation.PhysicalTableRequest.entryCapacity line 13433

     Also declared: ComparatorChallenges/EditApproximation.lean:13433 (same declaration text).

968. def OAI.EditApproximation.PhysicalTableRequest.code line 13435

     Also declared: ComparatorChallenges/EditApproximation.lean:13435 (same declaration text).

969. def OAI.EditApproximation.SourceRanked.supportedChild line 13448

     Also declared: ComparatorChallenges/EditApproximation.lean:13448 (same declaration text).

970. def OAI.EditApproximation.SourceRanked.supportedChildMap line 13452

     Also declared: ComparatorChallenges/EditApproximation.lean:13452 (same declaration text).

971. def OAI.EditApproximation.SourceRanked.restrictBody line 13459

     Also declared: ComparatorChallenges/EditApproximation.lean:13459 (same declaration text).

972. def OAI.EditApproximation.physicalRandomBoundedQuery line 13477

     Also declared: ComparatorChallenges/EditApproximation.lean:13477 (same declaration text).

973. def OAI.EditApproximation.chargedRandomGlobalQuery line 13486

     Also declared: ComparatorChallenges/EditApproximation.lean:13486 (same declaration text).

974. abbrev OAI.EditApproximation.PhysicalFamilyScalarKey line 13525

     Also declared: ComparatorChallenges/EditApproximation.lean:13525 (same declaration text).

975. abbrev OAI.EditApproximation.PhysicalFamilyScalarDraw line 13528

     Also declared: ComparatorChallenges/EditApproximation.lean:13528 (same declaration text).

976. def OAI.EditApproximation.physicalFamilyAnswer line 13543

     Also declared: ComparatorChallenges/EditApproximation.lean:13543 (same declaration text).

977. def OAI.EditApproximation.physicalFamilyGroupRead line 13547

     Also declared: ComparatorChallenges/EditApproximation.lean:13547 (same declaration text).

978. def OAI.EditApproximation.physicalFamilyOnlineRead line 13553

     Also declared: ComparatorChallenges/EditApproximation.lean:13553 (same declaration text).

979. abbrev OAI.EditApproximation.QueryFamilyMemoKey line 13569

     Also declared: ComparatorChallenges/EditApproximation.lean:13569 (same declaration text).

980. def OAI.EditApproximation.queryFamilySourceWordWithWork line 13573

     Also declared: ComparatorChallenges/EditApproximation.lean:13573 (same declaration text).

981. def OAI.EditApproximation.queryFamilyMemoRemaining line 13578

     Also declared: ComparatorChallenges/EditApproximation.lean:13578 (same declaration text).

982. abbrev OAI.EditApproximation.ComputedFamilySeed line 13591

     Also declared: ComparatorChallenges/EditApproximation.lean:13591 (same declaration text).

983. abbrev OAI.EditApproximation.ComputedFamilyDraw line 13595

     Also declared: ComparatorChallenges/EditApproximation.lean:13595 (same declaration text).

984. abbrev OAI.EditApproximation.ComputedFamilyInput line 13601

     Also declared: ComparatorChallenges/EditApproximation.lean:13601 (same declaration text).

985. def OAI.EditApproximation.physicalFamilyCode line 13615

     Also declared: ComparatorChallenges/EditApproximation.lean:13615 (same declaration text).

986. def OAI.EditApproximation.ChargedPhysicalRequest.code line 13627

     Also declared: ComparatorChallenges/EditApproximation.lean:13627 (same declaration text).

987. abbrev OAI.EditApproximation.ComputedFamilyScalarKey line 13640

     Also declared: ComparatorChallenges/EditApproximation.lean:13640 (same declaration text).

988. def OAI.EditApproximation.computedFamilyMemoCode line 13646

     Also declared: ComparatorChallenges/EditApproximation.lean:13646 (same declaration text).

989. def OAI.EditApproximation.coarseInitialCandidate line 13662

     Also declared: ComparatorChallenges/EditApproximation.lean:13662 (same declaration text).

990. def OAI.EditApproximation.coarseInitialMinimum line 13670

     Also declared: ComparatorChallenges/EditApproximation.lean:13670 (same declaration text).

991. def OAI.EditApproximation.coarseInitialValue line 13675

     Also declared: ComparatorChallenges/EditApproximation.lean:13675 (same declaration text).

992. def OAI.EditApproximation.coarseActiveArrayWork line 13691

     Also declared: ComparatorChallenges/EditApproximation.lean:13691 (same declaration text).

993. def OAI.EditApproximation.coarseFullSeedTable line 13702

     Also declared: ComparatorChallenges/EditApproximation.lean:13702 (same declaration text).

994. def OAI.EditApproximation.coarseInitialArrayWork line 13707

     Also declared: ComparatorChallenges/EditApproximation.lean:13707 (same declaration text).

995. def OAI.EditApproximation.integerEqualWithWork line 13725

     Also declared: ComparatorChallenges/EditApproximation.lean:13725 (same declaration text).

996. def OAI.EditApproximation.integerPreprocessingWork line 13735

     Also declared: ComparatorChallenges/EditApproximation.lean:13735 (same declaration text).

997. abbrev OAI.EditApproximation.ComputedFamilyMemoKey line 13749

     Also declared: ComparatorChallenges/EditApproximation.lean:13749 (same declaration text).

998. def OAI.EditApproximation.integerPreevaluationWork line 13753

     Also declared: ComparatorChallenges/EditApproximation.lean:13753 (same declaration text).

999. def OAI.EditApproximation.physicalFamilyCodeWithWork line 13766

     Also declared: ComparatorChallenges/EditApproximation.lean:13766 (same declaration text).

1000. def OAI.EditApproximation.computedFamilyMemoCodeWithWork line 13783

      Also declared: ComparatorChallenges/EditApproximation.lean:13783 (same declaration text).

1001. def OAI.EditApproximation.queryPhysicalScalarGroupQueries line 13804

      Also declared: ComparatorChallenges/EditApproximation.lean:13804 (same declaration text).

1002. def OAI.EditApproximation.queryPhysicalScalarGroupRead line 13983

      Also declared: ComparatorChallenges/EditApproximation.lean:13983 (same declaration text).

1003. def OAI.EditApproximation.queryPhysicalScalarOnlineRead line 14000

      Also declared: ComparatorChallenges/EditApproximation.lean:14000 (same declaration text).

1004. def OAI.EditApproximation.queryFamilyTagWithWork line 14137

      Also declared: ComparatorChallenges/EditApproximation.lean:14137 (same declaration text).

1005. def OAI.EditApproximation.queryFamilyGroupRead line 14146

      Also declared: ComparatorChallenges/EditApproximation.lean:14146 (same declaration text).

1006. def OAI.EditApproximation.queryFamilyOnlineRead line 14155

      Also declared: ComparatorChallenges/EditApproximation.lean:14155 (same declaration text).

1007. abbrev OAI.EditApproximation.QueryPhysicalChild line 14173

      Also declared: ComparatorChallenges/EditApproximation.lean:14173 (same declaration text).

1008. def OAI.EditApproximation.querySupportedChildWithWork line 14176

      Also declared: ComparatorChallenges/EditApproximation.lean:14176 (same declaration text).

1009. def OAI.EditApproximation.queryRestrictPhysicalBody line 14181

      Also declared: ComparatorChallenges/EditApproximation.lean:14181 (same declaration text).

1010. def OAI.EditApproximation.queryInitialConeProgramAt line 14291

      Also declared: ComparatorChallenges/EditApproximation.lean:14291 (same declaration text).

1011. def OAI.EditApproximation.queryChargedRead line 14309

      Also declared: ComparatorChallenges/EditApproximation.lean:14309 (same declaration text).

1012. def OAI.EditApproximation.queryChargedPreviousRead line 14316

      Also declared: ComparatorChallenges/EditApproximation.lean:14316 (same declaration text).

1013. def OAI.EditApproximation.queryChargedSeedAt line 14366

      Also declared: ComparatorChallenges/EditApproximation.lean:14366 (same declaration text).

1014. def OAI.EditApproximation.queryPhysicalInitial line 14436

      Also declared: ComparatorChallenges/EditApproximation.lean:14436 (same declaration text).

1015. def OAI.EditApproximation.queryWarmupProgram line 14458

      Also declared: ComparatorChallenges/EditApproximation.lean:14458 (same declaration text).

1016. def OAI.EditApproximation.queryChargedWarmupChild line 14477

      Also declared: ComparatorChallenges/EditApproximation.lean:14477 (same declaration text).

1017. def OAI.EditApproximation.queryChargedWarmup line 14532

      Also declared: ComparatorChallenges/EditApproximation.lean:14532 (same declaration text).

1018. abbrev OAI.EditApproximation.ChargedFamilyQueryKey line 14616

      Also declared: ComparatorChallenges/EditApproximation.lean:14616 (same declaration text).

1019. def OAI.EditApproximation.rankedNormalizeBody line 14629

      Also declared: ComparatorChallenges/EditApproximation.lean:14629 (same declaration text).

1020. def OAI.EditApproximation.chargedRandomMemoEvaluate line 14643

      Also declared: ComparatorChallenges/EditApproximation.lean:14643 (same declaration text).

1021. def OAI.EditApproximation.physicalFamilyProgram line 14661

      Also declared: ComparatorChallenges/EditApproximation.lean:14661 (same declaration text).

1022. abbrev OAI.EditApproximation.PhysicalCoarseDraw line 14678

      Also declared: ComparatorChallenges/EditApproximation.lean:14678 (same declaration text).

1023. def OAI.EditApproximation.physicalCoarseSeedTable line 14694

      Also declared: ComparatorChallenges/EditApproximation.lean:14694 (same declaration text).

1024. def OAI.EditApproximation.localFinalRootRequest line 14773

      Also declared: ComparatorChallenges/EditApproximation.lean:14773 (same declaration text).

1025. def OAI.EditApproximation.computedFamilyKernelWork line 14788

      Also declared: ComparatorChallenges/EditApproximation.lean:14788 (same declaration text).

1026. def OAI.EditApproximation.computedFamilyAddressWork line 14807

      Also declared: ComparatorChallenges/EditApproximation.lean:14807 (same declaration text).

1027. def OAI.EditApproximation.computedFamilyCoarseCopyStorage line 14826

      Also declared: ComparatorChallenges/EditApproximation.lean:14826 (same declaration text).

1028. def OAI.EditApproximation.computedFamilyCoarseArrayCapacity line 14832

      Also declared: ComparatorChallenges/EditApproximation.lean:14832 (same declaration text).

1029. def OAI.EditApproximation.computedFamilyCoarseScratchCapacity line 14836

      Also declared: ComparatorChallenges/EditApproximation.lean:14836 (same declaration text).

1030. def OAI.EditApproximation.computedFamilyCoarseControlCapacity line 14840

      Also declared: ComparatorChallenges/EditApproximation.lean:14840 (same declaration text).

1031. def OAI.EditApproximation.physicalFamilyMemoResult line 14867

      Also declared: ComparatorChallenges/EditApproximation.lean:14867 (same declaration text).

1032. def OAI.EditApproximation.selectionIndicator line 14887

      Also declared: ComparatorChallenges/EditApproximation.lean:14887 (same declaration text).

1033. def OAI.EditApproximation.coarseIndexedEntryCostSum line 14898

      Also declared: ComparatorChallenges/EditApproximation.lean:14898 (same declaration text).

1034. def OAI.EditApproximation.querySupportedChildAllocation line 14907

      Also declared: ComparatorChallenges/EditApproximation.lean:14907 (same declaration text).

1035. def OAI.EditApproximation.rejectionFailureLaw line 14925

      Also declared: ComparatorChallenges/EditApproximation.lean:14925 (same declaration text).

1036. def OAI.EditApproximation.rejectionRuntimeArrayLaw line 14957

      Also declared: ComparatorChallenges/EditApproximation.lean:14957 (same declaration text).

1037. def OAI.EditApproximation.rejectionSelectedBits line 14960

      Also declared: ComparatorChallenges/EditApproximation.lean:14960 (same declaration text).

1038. abbrev OAI.EditApproximation.physicalFamilyRange line 14975

      Also declared: ComparatorChallenges/EditApproximation.lean:14975 (same declaration text).

1039. instance OAI.EditApproximation.physicalFamilyRange_neZero line 14979

      Also declared: ComparatorChallenges/EditApproximation.lean:14979 (same declaration text).

1040. abbrev OAI.EditApproximation.ComputedPhysicalCoarseDraw line 14994

      Also declared: ComparatorChallenges/EditApproximation.lean:14994 (same declaration text).

1041. abbrev OAI.EditApproximation.ComputedRejectionRuntime line 14998

      Also declared: ComparatorChallenges/EditApproximation.lean:14998 (same declaration text).

1042. def OAI.EditApproximation.computedPhysicalCoarseLaw line 15004

      Also declared: ComparatorChallenges/EditApproximation.lean:15004 (same declaration text).

1043. abbrev OAI.EditApproximation.ComputedExecutionOutcome line 15010

      Also declared: ComparatorChallenges/EditApproximation.lean:15010 (same declaration text).

1044. def OAI.EditApproximation.computedExecutionLaw line 15013

      Also declared: ComparatorChallenges/EditApproximation.lean:15013 (same declaration text).

1045. abbrev OAI.EditApproximation.ComputedFullOutcome line 15021

      Also declared: ComparatorChallenges/EditApproximation.lean:15021 (same declaration text).

1046. abbrev OAI.EditApproximation.PhysicalFamilyRuntimeOutcome line 15042

      Also declared: ComparatorChallenges/EditApproximation.lean:15042 (same declaration text).

1047. def OAI.EditApproximation.physicalFamilyRuntimeAccepted line 15044

      Also declared: ComparatorChallenges/EditApproximation.lean:15044 (same declaration text).

1048. def OAI.EditApproximation.physicalLargeInput line 15057

      Also declared: ComparatorChallenges/EditApproximation.lean:15057 (same declaration text).

1049. instance OAI.EditApproximation.physicalLargeInput_decidable line 15063

      Also declared: ComparatorChallenges/EditApproximation.lean:15063 (same declaration text).

1050. def OAI.EditApproximation.physicalFamilyMemoBits line 15085

      Also declared: ComparatorChallenges/EditApproximation.lean:15085 (same declaration text).

1051. def OAI.EditApproximation.computedFamilyResult line 15101

      Also declared: ComparatorChallenges/EditApproximation.lean:15101 (same declaration text).

1052. def OAI.EditApproximation.computedFamilyRejectionWork line 15108

      Also declared: ComparatorChallenges/EditApproximation.lean:15108 (same declaration text).

1053. def OAI.EditApproximation.physicalFamilyMemoCoarseWork line 15138

      Also declared: ComparatorChallenges/EditApproximation.lean:15138 (same declaration text).

1054. abbrev OAI.EditApproximation.PhysicalCoarseExecution line 15158

      Also declared: ComparatorChallenges/EditApproximation.lean:15158 (same declaration text).

1055. def OAI.EditApproximation.physicalCoarseExecutionProjection line 15163

      Also declared: ComparatorChallenges/EditApproximation.lean:15163 (same declaration text).

1056. def OAI.EditApproximation.computedExecutionProjection line 15177

      Also declared: ComparatorChallenges/EditApproximation.lean:15177 (same declaration text).

1057. def OAI.EditApproximation.computedFullLaw line 15183

      Also declared: ComparatorChallenges/EditApproximation.lean:15183 (same declaration text).

1058. def OAI.EditApproximation.computedExecutionAccepted line 15197

      Also declared: ComparatorChallenges/EditApproximation.lean:15197 (same declaration text).

1059. def OAI.EditApproximation.computedExecutionRejectionWork line 15202

      Also declared: ComparatorChallenges/EditApproximation.lean:15202 (same declaration text).

1060. def OAI.EditApproximation.computedFinalRoot line 15206

      Also declared: ComparatorChallenges/EditApproximation.lean:15206 (same declaration text).

1061. def OAI.EditApproximation.computedExecutionKernelWork line 15212

      Also declared: ComparatorChallenges/EditApproximation.lean:15212 (same declaration text).

1062. def OAI.EditApproximation.computedExecutionDictionaryWork line 15227

      Also declared: ComparatorChallenges/EditApproximation.lean:15227 (same declaration text).

1063. def OAI.EditApproximation.computedExecutionAddressWork line 15231

      Also declared: ComparatorChallenges/EditApproximation.lean:15231 (same declaration text).

1064. def OAI.EditApproximation.symbolicComputedCoarseWork line 15249

      Also declared: ComparatorChallenges/EditApproximation.lean:15249 (same declaration text).

1065. def OAI.EditApproximation.symbolicComputedExecutionCoarseWork line 15259

      Also declared: ComparatorChallenges/EditApproximation.lean:15259 (same declaration text).

1066. def OAI.EditApproximation.computedExecutionCoarseWork line 15273

      Also declared: ComparatorChallenges/EditApproximation.lean:15273 (same declaration text).

1067. def OAI.EditApproximation.computedExecutionNonlocalWork line 15288

      Also declared: ComparatorChallenges/EditApproximation.lean:15288 (same declaration text).

1068. def OAI.EditApproximation.physicalFamilyIndexedCoarseWork line 15315

      Also declared: ComparatorChallenges/EditApproximation.lean:15315 (same declaration text).

1069. def OAI.EditApproximation.symbolicComputedExecutionIndexedCoarseWork line 15338

      Also declared: ComparatorChallenges/EditApproximation.lean:15338 (same declaration text).

1070. def OAI.EditApproximation.computedExecutionIndexedCoarseWork line 15359

      Also declared: ComparatorChallenges/EditApproximation.lean:15359 (same declaration text).

1071. def OAI.EditApproximation.physicalFamilyCoarseSamplingWork line 15385

      Also declared: ComparatorChallenges/EditApproximation.lean:15385 (same declaration text).

1072. def OAI.EditApproximation.symbolicComputedExecutionCoarseSamplingWork line 15409

      Also declared: ComparatorChallenges/EditApproximation.lean:15409 (same declaration text).

1073. def OAI.EditApproximation.computedExecutionCoarseSamplingWork line 15430

      Also declared: ComparatorChallenges/EditApproximation.lean:15430 (same declaration text).

1074. def OAI.EditApproximation.physicalFamilyCoarsePreparationWork line 15456

      Also declared: ComparatorChallenges/EditApproximation.lean:15456 (same declaration text).

1075. def OAI.EditApproximation.computedFamilyCoarsePreparationWork line 15473

      Also declared: ComparatorChallenges/EditApproximation.lean:15473 (same declaration text).

1076. def OAI.EditApproximation.computedExecutionCoarsePreparationWork line 15484

      Also declared: ComparatorChallenges/EditApproximation.lean:15484 (same declaration text).

1077. def OAI.EditApproximation.computedExecutionReadChargedWork line 15488

      Also declared: ComparatorChallenges/EditApproximation.lean:15488 (same declaration text).

1078. def OAI.EditApproximation.computedExecutionTotalWork line 15504

      Also declared: ComparatorChallenges/EditApproximation.lean:15504 (same declaration text).

1079. def OAI.EditApproximation.computedFullOutputWork line 15510

      Also declared: ComparatorChallenges/EditApproximation.lean:15510 (same declaration text).

1080. def OAI.EditApproximation.queryFamilyTagAllocation line 15528

      Also declared: ComparatorChallenges/EditApproximation.lean:15528 (same declaration text).

1081. def OAI.EditApproximation.BitQuery.Footprint.rankedBitMemoCells line 15542

      Also declared: ComparatorChallenges/EditApproximation.lean:15542 (same declaration text).

1082. def OAI.EditApproximation.queryInitialGatherFootprint line 15578

      Also declared: ComparatorChallenges/EditApproximation.lean:15578 (same declaration text).

1083. def OAI.EditApproximation.queryBandGatherFootprint line 15607

      Also declared: ComparatorChallenges/EditApproximation.lean:15607 (same declaration text).

1084. def OAI.EditApproximation.queryGroupSourceGatherFootprint line 15641

      Also declared: ComparatorChallenges/EditApproximation.lean:15641 (same declaration text).

1085. def OAI.EditApproximation.queryOnlineSourceGatherFootprint line 15669

      Also declared: ComparatorChallenges/EditApproximation.lean:15669 (same declaration text).

1086. def OAI.EditApproximation.queryPhysicalTableReadFootprint line 15713

      Also declared: ComparatorChallenges/EditApproximation.lean:15713 (same declaration text).

1087. def OAI.EditApproximation.queryMeanReadFootprint line 15724

      Also declared: ComparatorChallenges/EditApproximation.lean:15724 (same declaration text).

1088. def OAI.EditApproximation.queryPhysicalScalarReadFootprint line 15741

      Also declared: ComparatorChallenges/EditApproximation.lean:15741 (same declaration text).

1089. def OAI.EditApproximation.queryRestrictPhysicalBodyFootprint line 15748

      Also declared: ComparatorChallenges/EditApproximation.lean:15748 (same declaration text).

1090. def OAI.EditApproximation.queryInitialConeProgramAtFootprint line 15850

      Also declared: ComparatorChallenges/EditApproximation.lean:15850 (same declaration text).

1091. def OAI.EditApproximation.queryChargedReadFootprint line 15890

      Also declared: ComparatorChallenges/EditApproximation.lean:15890 (same declaration text).

1092. def OAI.EditApproximation.queryWarmupProgramFootprint line 15900

      Also declared: ComparatorChallenges/EditApproximation.lean:15900 (same declaration text).

1093. def OAI.EditApproximation.queryPhysicalEarlierReadFootprint line 16004

      Also declared: ComparatorChallenges/EditApproximation.lean:16004 (same declaration text).

1094. def OAI.EditApproximation.queryPhysicalScalarOnlineReadFootprint line 16088

      Also declared: ComparatorChallenges/EditApproximation.lean:16088 (same declaration text).

1095. def OAI.EditApproximation.queryChargedSeedAtFootprint line 16216

      Also declared: ComparatorChallenges/EditApproximation.lean:16216 (same declaration text).

1096. def OAI.EditApproximation.queryFamilyOnlineReadFootprint line 16321

      Also declared: ComparatorChallenges/EditApproximation.lean:16321 (same declaration text).

1097. def OAI.EditApproximation.queryPhysicalInitialFootprint line 16337

      Also declared: ComparatorChallenges/EditApproximation.lean:16337 (same declaration text).

1098. def OAI.EditApproximation.queryPhysicalScalarGroupQueriesFootprint line 16370

      Also declared: ComparatorChallenges/EditApproximation.lean:16370 (same declaration text).

1099. def OAI.EditApproximation.queryPhysicalScalarGroupReadFootprint line 16557

      Also declared: ComparatorChallenges/EditApproximation.lean:16557 (same declaration text).

1100. def OAI.EditApproximation.queryFamilyGroupReadFootprint line 16568

      Also declared: ComparatorChallenges/EditApproximation.lean:16568 (same declaration text).

1101. def OAI.EditApproximation.queryChargedWarmupFootprint line 16593

      Also declared: ComparatorChallenges/EditApproximation.lean:16593 (same declaration text).

1102. def OAI.EditApproximation.BinaryFraction.preparedComputedCellSourceWithWorkRawBand line 16716

      Also declared: ComparatorChallenges/EditApproximation.lean:16716 (same declaration text).

1103. def OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleSourceWithWorkRawBand line 16803

      Also declared: ComparatorChallenges/EditApproximation.lean:16803 (same declaration text).

1104. def OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsSourceWithWorkRawBand line 16855

      Also declared: ComparatorChallenges/EditApproximation.lean:16855 (same declaration text).

1105. def OAI.EditApproximation.BinaryFraction.preparedLocalOnlineScaleSourceWithWorkRawBand line 16879

      Also declared: ComparatorChallenges/EditApproximation.lean:16879 (same declaration text).

1106. def OAI.EditApproximation.BinaryFraction.preparedLocalOnlineActionsSourceWithWorkRawBand line 17093

      Also declared: ComparatorChallenges/EditApproximation.lean:17093 (same declaration text).

1107. def OAI.EditApproximation.BinaryFraction.queryOnlineSelectWithWorkRawBand line 17112

      Also declared: ComparatorChallenges/EditApproximation.lean:17112 (same declaration text).

1108. def OAI.EditApproximation.BinaryFraction.queryGroupSelectWithWorkRawBand line 17119

      Also declared: ComparatorChallenges/EditApproximation.lean:17119 (same declaration text).

1109. def OAI.EditApproximation.queryLocalRefinementRawBand line 17134

      Also declared: ComparatorChallenges/EditApproximation.lean:17134 (same declaration text).

1110. def OAI.EditApproximation.queryLocalRandomSourcesRawBand line 17154

      Also declared: ComparatorChallenges/EditApproximation.lean:17154 (same declaration text).

1111. def OAI.EditApproximation.queryLocalBandRawBand line 17175

      Also declared: ComparatorChallenges/EditApproximation.lean:17175 (same declaration text).

1112. def OAI.EditApproximation.queryLocalProgramRawBand line 17255

      Also declared: ComparatorChallenges/EditApproximation.lean:17255 (same declaration text).

1113. def OAI.EditApproximation.queryPhysicalRandomDataRequestRawBand line 17270

      Also declared: ComparatorChallenges/EditApproximation.lean:17270 (same declaration text).

1114. def OAI.EditApproximation.queryFamilyRefinementRawBand line 17300

      Also declared: ComparatorChallenges/EditApproximation.lean:17300 (same declaration text).

1115. def OAI.EditApproximation.queryFamilyActiveRawBand line 17319

      Also declared: ComparatorChallenges/EditApproximation.lean:17319 (same declaration text).

1116. def OAI.EditApproximation.queryFamilyBoundedActiveRawBand line 17353

      Also declared: ComparatorChallenges/EditApproximation.lean:17353 (same declaration text).

1117. def OAI.EditApproximation.queryChargedFamilyTableRawBand line 17371

      Also declared: ComparatorChallenges/EditApproximation.lean:17371 (same declaration text).

1118. def OAI.EditApproximation.queryChargedFamilyGlobalRawBand line 17455

      Also declared: ComparatorChallenges/EditApproximation.lean:17455 (same declaration text).

1119. def OAI.EditApproximation.queryFamilyMemoRawRawBand line 17474

      Also declared: ComparatorChallenges/EditApproximation.lean:17474 (same declaration text).

1120. def OAI.EditApproximation.computedQueryMemoRawRawBand line 17490

      Also declared: ComparatorChallenges/EditApproximation.lean:17490 (same declaration text).

1121. def OAI.EditApproximation.computedQueryMemoNormalizedRawBand line 17515

      Also declared: ComparatorChallenges/EditApproximation.lean:17515 (same declaration text).

1122. def OAI.EditApproximation.computedQueryMemoResultRawBand line 17604

      Also declared: ComparatorChallenges/EditApproximation.lean:17604 (same declaration text).

1123. def OAI.EditApproximation.computedQueryLocalWorkRawBand line 17613

      Also declared: ComparatorChallenges/EditApproximation.lean:17613 (same declaration text).

1124. def OAI.EditApproximation.computedQueryAnswerWithWorkRawBand line 17619

      Also declared: ComparatorChallenges/EditApproximation.lean:17619 (same declaration text).

1125. def OAI.EditApproximation.integerQueryLocalWorkRawBand line 17636

      Also declared: ComparatorChallenges/EditApproximation.lean:17636 (same declaration text).

1126. def OAI.EditApproximation.integerBinaryOutputRawBand line 17649

      Also declared: ComparatorChallenges/EditApproximation.lean:17649 (same declaration text).

1127. def OAI.EditApproximation.integerBinaryAnswerRawBand line 17663

      Also declared: ComparatorChallenges/EditApproximation.lean:17663 (same declaration text).

1128. def OAI.EditApproximation.BinaryFraction.preparedComputedCellSourceAllocationRawBand line 17682

      Also declared: ComparatorChallenges/EditApproximation.lean:17682 (same declaration text).

1129. def OAI.EditApproximation.BinaryFraction.castGroupSourceAllocationRawBand line 17779

      Also declared: ComparatorChallenges/EditApproximation.lean:17779 (same declaration text).

1130. def OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleSourceAllocationRawBand line 17824

      Also declared: ComparatorChallenges/EditApproximation.lean:17824 (same declaration text).

1131. def OAI.EditApproximation.BinaryFraction.localGroupSourceScaleBlockRawBand line 17878

      Also declared: ComparatorChallenges/EditApproximation.lean:17878 (same declaration text).

1132. def OAI.EditApproximation.BinaryFraction.localGroupSourceScaleBlockAllocationRawBand line 17887

      Also declared: ComparatorChallenges/EditApproximation.lean:17887 (same declaration text).

1133. def OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsSourceAllocationRawBand line 17895

      Also declared: ComparatorChallenges/EditApproximation.lean:17895 (same declaration text).

1134. def OAI.EditApproximation.BinaryFraction.preparedLocalOnlineScaleSourceAllocationRawBand line 17914

      Also declared: ComparatorChallenges/EditApproximation.lean:17914 (same declaration text).

1135. def OAI.EditApproximation.BinaryFraction.preparedLocalOnlineActionsSourceAllocationRawBand line 18125

      Also declared: ComparatorChallenges/EditApproximation.lean:18125 (same declaration text).

1136. def OAI.EditApproximation.BinaryFraction.queryOnlineSelectAllocationRawBand line 18144

      Also declared: ComparatorChallenges/EditApproximation.lean:18144 (same declaration text).

1137. def OAI.EditApproximation.BinaryFraction.queryGroupSelectAllocationRawBand line 18154

      Also declared: ComparatorChallenges/EditApproximation.lean:18154 (same declaration text).

1138. def OAI.EditApproximation.integerBinaryWorkRawBand line 18172

      Also declared: ComparatorChallenges/EditApproximation.lean:18172 (same declaration text).

1139. def OAI.EditApproximation.integerFinalAllocationRawBand line 18187

      Also declared: ComparatorChallenges/EditApproximation.lean:18187 (same declaration text).

1140. def OAI.EditApproximation.queryLocalRefinementFootprintRawBand line 18205

      Also declared: ComparatorChallenges/EditApproximation.lean:18205 (same declaration text).

1141. def OAI.EditApproximation.queryLocalRandomSourcesFootprintRawBand line 18446

      Also declared: ComparatorChallenges/EditApproximation.lean:18446 (same declaration text).

1142. def OAI.EditApproximation.queryLocalBandFootprintRawBand line 18524

      Also declared: ComparatorChallenges/EditApproximation.lean:18524 (same declaration text).

1143. def OAI.EditApproximation.queryLocalProgramFootprintRawBand line 18644

      Also declared: ComparatorChallenges/EditApproximation.lean:18644 (same declaration text).

1144. def OAI.EditApproximation.queryPhysicalRandomDataRequestFootprintRawBand line 18690

      Also declared: ComparatorChallenges/EditApproximation.lean:18690 (same declaration text).

1145. def OAI.EditApproximation.queryFamilyRefinementFootprintRawBand line 18755

      Also declared: ComparatorChallenges/EditApproximation.lean:18755 (same declaration text).

1146. def OAI.EditApproximation.queryFamilyActiveFootprintRawBand line 18781

      Also declared: ComparatorChallenges/EditApproximation.lean:18781 (same declaration text).

1147. def OAI.EditApproximation.queryFamilyBoundedActiveFootprintRawBand line 18808

      Also declared: ComparatorChallenges/EditApproximation.lean:18808 (same declaration text).

1148. def OAI.EditApproximation.queryChargedFamilyTableFootprintRawBand line 18829

      Also declared: ComparatorChallenges/EditApproximation.lean:18829 (same declaration text).

1149. def OAI.EditApproximation.queryChargedFamilyGlobalFootprintRawBand line 18916

      Also declared: ComparatorChallenges/EditApproximation.lean:18916 (same declaration text).

1150. def OAI.EditApproximation.queryFamilyMemoRawFootprintRawBand line 18940

      Also declared: ComparatorChallenges/EditApproximation.lean:18940 (same declaration text).

1151. def OAI.EditApproximation.computedQueryMemoRawFootprintRawBand line 18979

      Also declared: ComparatorChallenges/EditApproximation.lean:18979 (same declaration text).

1152. def OAI.EditApproximation.computedQueryMemoFootprintRawBand line 19010

      Also declared: ComparatorChallenges/EditApproximation.lean:19010 (same declaration text).

1153. def OAI.EditApproximation.computedQueryTemporaryCellsFootprintRawBand line 19102

      Also declared: ComparatorChallenges/EditApproximation.lean:19102 (same declaration text).

1154. def OAI.EditApproximation.integerAcceptedSpaceTermsFootprintRawBand line 19113

      Also declared: ComparatorChallenges/EditApproximation.lean:19113 (same declaration text).

1155. def OAI.EditApproximation.integerBinarySpaceFootprintRawBand line 19133

      Also declared: ComparatorChallenges/EditApproximation.lean:19133 (same declaration text).