`ComparatorChallenges/EditApproximation.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 120 curated AI-written annotations and 1273 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 9 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. Those 9 annotations were revised on 2026-10-14 to bind all of them to exact page-one quotations from 6 pinned OpenAI manuscripts, the matching pinned formalization notes, and named historical primary sources; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. The 3 manuscript-grounded matrix-multiplication annotations were composed from pinned OpenAI manuscripts and named historical sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Six additional target-specific annotations for Catalan's constant, the irrationality exponent of pi, dyadic Erdos similarity, Unique Games, quintic Lienard systems, and Yau nodal growth were composed from pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for Seymour's second-neighborhood conjecture, Cannon's conjecture, Koebe circle-domain uniformization, and circle-domain rigidity were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical primary sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for simple Lebesgue spectrum on the three-torus, Rokhlin multiple mixing, the nine-dimensional Borsuk counterexample, and Tingley's sphere-isometry problem were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical primary sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for the Abhyankar-Sathaye counterexample, the circulant Hadamard conjecture, the Eilenberg-Ganea counterexample, and short Egyptian fractions were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and quotations from Sathaye, Turyn with Storer, Eilenberg with Ganea, and Erdos in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for the complete Crouzeix inequality, unrestricted Euclidean five-coloring, the general Mahler conjecture, and Thompson F nonamenability were composed on 2026-10-14 from exact Lean statements, 4 pinned OpenAI manuscripts, the matching formalization notes, and linked historical sources by Crouzeix, de Grey, Mahler, Cannon, Floyd, and Parry; no human review is claimed. Four additional target-specific annotations for algorithmic strong thin trees, Barnette's Hamiltonian-cycle conjecture, the explicit Artin CAT(0) counterexample, and generalized amplitude-damping capacity were composed on 2026-10-14 from exact Lean statements, 4 pinned OpenAI manuscripts, matching formalization notes, and linked historical sources by Anari with Goddyn, Arts with Hopman and Timmermans, Charney, and Khatri with Sharma and Wilde; no human review is claimed. Fourteen solution-level annotations for Seymour's second-neighborhood theorem were added on 2026-10-14 from the pinned 15-page manuscript, covering the exact-neighborhood model, minimal-counterexample reduction, subset deficit, transitive blowup, pruning, extremal contradiction, and proof-bearing final theorem. The subset and blowup annotations also bind exact quotations from Tyler Seacrest (2019) and Brantner, Brockman, Kay, and Snively (2009); no human review is claimed. Thirty-seven declaration-level annotations were added on 2026-10-14 for the rest of ComparatorChallenges/AlgorithmicThinTrees.lean, covering its multigraph semantics, stack-machine cost model, explicit and binary-multiplicity encodings, output certificate, and complete algorithmic proposition. They are bound to the pinned OpenAI manuscript and linked earlier thin-tree sources by Luis Goddyn, Nima Anari, and Shayan Oveis Gharan; the annotation explicitly preserves that the concluding comparator theorem still has body by sorry, and no human review is claimed. Thirty-one supporting declarations in ComparatorChallenges/UniqueGamesTheorem.lean were upgraded or added on 2026-10-14, completing curated coverage of all thirty-two declarations in that file. The annotations cover the finite game model, Boolean formula and parser, binary-vector translations, explicit output serialization, finite-alphabet machine contract, and gap theorem; they distinguish manuscript-backed mathematics from Lean-specific canonical parsing and unary game output encoding, bind exact OpenAI manuscript quotations, and credit Subhash Khot through his 2010 survey. The comparator theorem remains explicitly labeled as having body by sorry; no human review is claimed. The source-derived generator was hardened on 2026-10-14 so a formalization note covering multiple comparator results no longer copies its combined Scope prose onto each declaration; those targets now use declaration-specific source comments when available and otherwise remain explicitly bounded to the exact Lean statement. The remaining source-derived annotations were generated mechanically from pinned formalization notes and source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the source prose.

Credit: OpenAI's pinned repository says an unreleased internal model produced the manuscripts and supporting proof artifacts. The collection builds on the mathematics community's accumulated problems, results, language, and formal libraries; each manuscript's BibTeX and bibliography are the authority for individual scholarly credit.

Project sources: Pinned openai/math documentation, Pinned formalization catalogue

1156 declarations, 1 contain sorry, 0 declared as axioms

A uniform almost-linear approximation scheme for edit distance. The statement retains the concrete binary algorithm and its exact resource accounting.

def OAI.EditApproximation.bitWordValue line 14
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14 (same declaration text).
def OAI.EditApproximation.bitSum line 18
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18 (same declaration text).
def OAI.EditApproximation.bitCarry line 20
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:20 (same declaration text).
structure OAI.EditApproximation.UnreducedRational line 22
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:22 (same declaration text).
def OAI.EditApproximation.orderingMatches line 27
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:27 (same declaration text).
def OAI.EditApproximation.bitOrdering line 30
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:30 (same declaration text).
def OAI.EditApproximation.bitDifference line 36
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:36 (same declaration text).
def OAI.EditApproximation.bitBorrow line 38
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:38 (same declaration text).
structure OAI.EditApproximation.SignedBinary line 40
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:40 (same declaration text).
def OAI.EditApproximation.signedMagnitude line 44
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:44 (same declaration text).
def OAI.EditApproximation.trimBitWordWithWork line 47
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:47 (same declaration text).
def OAI.EditApproximation.balancedCut line 53
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:53 (same declaration text).
def OAI.EditApproximation.gridRound line 55
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:55 (same declaration text).
def OAI.EditApproximation.rationalMinimum line 57
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:57 (same declaration text).
structure OAI.EditApproximation.RationalBellmanAction line 61
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:61 (same declaration text).
def OAI.EditApproximation.rationalRefinementUpdate line 66
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:66 (same declaration text).
def OAI.EditApproximation.heightExponent line 70
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:70 (same declaration text).
def OAI.EditApproximation.coarseExponent line 72
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:72 (same declaration text).
structure OAI.EditApproximation.IntegerParameters line 74
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:74 (same declaration text).
structure OAI.EditApproximation.RationalParameters line 85
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:85 (same declaration text).
def OAI.EditApproximation.gridPointsBetween line 96
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:96 (same declaration text).
def OAI.EditApproximation.scaledSeedValue line 99
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:99 (same declaration text).
def OAI.EditApproximation.dyadicScales line 102
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:102 (same declaration text).
def OAI.EditApproximation.seedGridSpacing line 105
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:105 (same declaration text).
def OAI.EditApproximation.finiteAssignments line 107
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:107 (same declaration text).
def OAI.EditApproximation.powerTwoWord line 113
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:113 (same declaration text).
def OAI.EditApproximation.filterWithWork line 115
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:115 (same declaration text).
def OAI.EditApproximation.allWithWork line 122
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:122 (same declaration text).
def OAI.EditApproximation.arithmeticMapWithWork line 129
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:129 (same declaration text).
def OAI.EditApproximation.arithmeticFlatMapWithWork line 136
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:136 (same declaration text).
def OAI.EditApproximation.upperMedian line 143
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:143 (same declaration text).
def OAI.EditApproximation.filterMapWithWork line 146
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:146 (same declaration text).
def OAI.EditApproximation.cellGridPoints line 153
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:153 (same declaration text).
def OAI.EditApproximation.groupRoundSpacing line 157
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:157 (same declaration text).
def OAI.EditApproximation.refinementFactor line 160
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:160 (same declaration text).
def OAI.EditApproximation.localCellCoordinates line 162
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:162 (same declaration text).
def OAI.EditApproximation.dyadicSeedPassCount line 167
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:167 (same declaration text).
def OAI.EditApproximation.dyadicSeedExponent line 169
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:169 (same declaration text).
def OAI.EditApproximation.memberByWithWork line 171
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:171 (same declaration text).
inductive OAI.EditApproximation.BinaryMemo line 178
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:178 (same declaration text).
def OAI.EditApproximation.binaryMemoKey line 182
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:182 (same declaration text).
inductive OAI.EditApproximation.FiniteQuery line 186
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:186 (same declaration text).
def OAI.EditApproximation.finiteAnswerTable line 190
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:190 (same declaration text).
def OAI.EditApproximation.queryFinRange line 195
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:195 (same declaration text).
def OAI.EditApproximation.queryInsertWithWork line 198
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:198 (same declaration text).
def OAI.EditApproximation.integerSymbolCode line 207
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:207 (same declaration text).
inductive OAI.EditApproximation.PositionCounts line 211
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:211 (same declaration text).
def OAI.EditApproximation.integerMagnitude line 215
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:215 (same declaration text).
def OAI.EditApproximation.integerInputPositionBits line 219
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:219 (same declaration text).
def OAI.EditApproximation.dpLength line 221
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:221 (same declaration text).
def OAI.EditApproximation.dpDrop line 225
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:225 (same declaration text).
def OAI.EditApproximation.dpTake line 230
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:230 (same declaration text).
def OAI.EditApproximation.dpGetD line 235
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:235 (same declaration text).
def OAI.EditApproximation.dpMember line 240
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:240 (same declaration text).
def OAI.EditApproximation.dpMinimum line 245
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:245 (same declaration text).
def OAI.EditApproximation.integerMagnitudeWithWork line 249
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:249 (same declaration text).
def OAI.EditApproximation.inputBitLengthWithWork line 255
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:255 (same declaration text).
def OAI.EditApproximation.naturalPairWithWork line 262
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:262 (same declaration text).
def OAI.EditApproximation.inspectBitPrefix line 265
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:265 (same declaration text).
def OAI.EditApproximation.memoRequestCells line 273
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:273 (same declaration text).
def OAI.EditApproximation.arithmeticMapAllocation line 275
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:275 (same declaration text).
def OAI.EditApproximation.arithmeticFlatMapAllocation line 279
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:279 (same declaration text).
def OAI.EditApproximation.filterAllocation line 284
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:284 (same declaration text).
def OAI.EditApproximation.filterMapAllocation line 288
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:288 (same declaration text).
def OAI.EditApproximation.naturalEqualAllocation line 293
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:293 (same declaration text).
def OAI.EditApproximation.memberByAllocation line 295
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:295 (same declaration text).
def OAI.EditApproximation.naturalWordLEAllocation line 299
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:299 (same declaration text).
def OAI.EditApproximation.vectorMapAllocation line 301
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:301 (same declaration text).
def OAI.EditApproximation.allAllocation line 304
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:304 (same declaration text).
def OAI.EditApproximation.queryInsertAllocation line 308
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:308 (same declaration text).
def OAI.EditApproximation.wordLEAllocation line 313
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:313 (same declaration text).
def OAI.EditApproximation.indexedLeafAllocation line 315
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:315 (same declaration text).
def OAI.EditApproximation.storedNaturalBits line 320
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:320 (same declaration text).
def OAI.EditApproximation.coarseHistoryKeyCost line 323
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:323 (same declaration text).
def OAI.EditApproximation.bitAddNilLeftWithWork line 327
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:327 (same declaration text).
def OAI.EditApproximation.bitCompareNilLeftWithWork line 335
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:335 (same declaration text).
def OAI.EditApproximation.bitSubtractNilLeftWithWork line 343
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:343 (same declaration text).
structure OAI.EditApproximation.BinaryFraction line 351
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:351 (same declaration text).
def OAI.EditApproximation.rationalActionValue line 356
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:356 (same declaration text).
def OAI.EditApproximation.inputHeight line 361
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:361 (same declaration text).
def OAI.EditApproximation.smallLogExponent line 363
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:363 (same declaration text).
def OAI.EditApproximation.rationalParameters line 365
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:365 (same declaration text).
def OAI.EditApproximation.materializedAssignmentsWithWork line 371
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:371 (same declaration text).
def OAI.EditApproximation.dyadicScalesWithWork line 381
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:381 (same declaration text).
def OAI.EditApproximation.dedupByWithWork line 388
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:388 (same declaration text).
def OAI.EditApproximation.queryEraseLoopWithWork line 395
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:395 (same declaration text).
structure OAI.EditApproximation.RecursiveMemoResult line 403
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:403 (same declaration text).
def OAI.EditApproximation.querySortWithWork line 410
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:410 (same declaration text).
def OAI.EditApproximation.encodeIntegerSymbolsWithWork line 417
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:417 (same declaration text).
def OAI.EditApproximation.integerInputSymbolBits line 423
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:423 (same declaration text).
def OAI.EditApproximation.dpSingleton line 426
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:426 (same declaration text).
def OAI.EditApproximation.dpCandidateAllocation line 432
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:432 (same declaration text).
def OAI.EditApproximation.integerInputInspectionWithWork line 435
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:435 (same declaration text).
def OAI.EditApproximation.bitAddNilLeftAllocation line 444
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:444 (same declaration text).
def OAI.EditApproximation.bitSubtractNilLeftAllocation line 450
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:450 (same declaration text).
def OAI.EditApproximation.trimBitWordAllocation line 456
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:456 (same declaration text).
def OAI.EditApproximation.dedupByAllocation line 461
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:461 (same declaration text).
def OAI.EditApproximation.dyadicScalesAllocation line 467
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:467 (same declaration text).
def OAI.EditApproximation.queryRangeValidAllocation line 470
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:470 (same declaration text).
def OAI.EditApproximation.queryEraseLoopAllocation line 473
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:473 (same declaration text).
def OAI.EditApproximation.queryEncodedLEAllocation line 481
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:481 (same declaration text).
def OAI.EditApproximation.bitAddWithWork line 485
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:485 (same declaration text).
def OAI.EditApproximation.bitCompareWithWork line 498
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:498 (same declaration text).
def OAI.EditApproximation.bitSubtractWithWork line 511
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:511 (same declaration text).
def OAI.EditApproximation.rationalBellman line 524
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:524 (same declaration text).
def OAI.EditApproximation.inputSmallLog line 529
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:529 (same declaration text).
structure OAI.EditApproximation.BinaryBellmanAction line 531
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:531 (same declaration text).
def OAI.EditApproximation.queryEraseWithWork line 536
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:536 (same declaration text).
inductive OAI.EditApproximation.BitQuery line 539
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:539 (same declaration text).
def OAI.EditApproximation.dpCandidate line 544
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:544 (same declaration text).
def OAI.EditApproximation.dpCellAllocation line 552
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:552 (same declaration text).
def OAI.EditApproximation.initialThresholdQ line 557
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:557 (same declaration text).
def OAI.EditApproximation.initialLambda line 559
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:559 (same declaration text).
structure OAI.EditApproximation.BitRecursiveMemoResult line 561
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:561 (same declaration text).
structure OAI.EditApproximation.RefinementParameterWords line 569
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:569 (same declaration text).
def OAI.EditApproximation.inspectAccuracyWithWork line 576
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:576 (same declaration text).
def OAI.EditApproximation.bitAddAllocation line 585
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:585 (same declaration text).
def OAI.EditApproximation.bitSubtractAllocation line 594
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:594 (same declaration text).
def OAI.EditApproximation.materializedAssignmentsAllocation line 603
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:603 (same declaration text).
def OAI.EditApproximation.queryEraseAllocation line 614
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:614 (same declaration text).
def OAI.EditApproximation.querySortAllocation line 617
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:617 (same declaration text).
def OAI.EditApproximation.binaryNaturalAddWithWork line 623
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:623 (same declaration text).
def OAI.EditApproximation.bitMulWithWork line 626
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:626 (same declaration text).
def OAI.EditApproximation.binaryNaturalCompareWithWork line 635
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:635 (same declaration text).
def OAI.EditApproximation.binaryNaturalSubtractWithWork line 637
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:637 (same declaration text).
def OAI.EditApproximation.integerParameters line 641
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:641 (same declaration text).
def OAI.EditApproximation.bitDivModWithWork line 649
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:649 (same declaration text).
def OAI.EditApproximation.wordLEWithWork line 661
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:661 (same declaration text).
def OAI.EditApproximation.computedSeedInitialExponent line 665
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:665 (same declaration text).
def OAI.EditApproximation.queryOrderedInputsWithWork line 668
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:668 (same declaration text).
def OAI.EditApproximation.queryActionInputsWithWork line 674
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:674 (same declaration text).
def OAI.EditApproximation.largeAccuracyInput line 680
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:680 (same declaration text).
def OAI.EditApproximation.dpCell line 683
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:683 (same declaration text).
def OAI.EditApproximation.suffixDPAllocation line 691
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:691 (same declaration text).
def OAI.EditApproximation.binaryNaturalAddAllocation line 697
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:697 (same declaration text).
def OAI.EditApproximation.queryOrderedInputsAllocation line 699
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:699 (same declaration text).
def OAI.EditApproximation.queryActionInputsAllocation line 704
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:704 (same declaration text).
def OAI.EditApproximation.binaryNaturalMulWithWork line 710
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:710 (same declaration text).
def OAI.EditApproximation.binaryNaturalDivModWithWork line 712
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:712 (same declaration text).
def OAI.EditApproximation.bitCeilDivWithWork line 715
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:715 (same declaration text).
def OAI.EditApproximation.wordMinWithWork line 723
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:723 (same declaration text).
def OAI.EditApproximation.wordInsertWithWork line 727
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:727 (same declaration text).
def OAI.EditApproximation.saturatingSubtractWithWork line 735
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:735 (same declaration text).
def OAI.EditApproximation.computedSeedPassCount line 741
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:741 (same declaration text).
def OAI.EditApproximation.bitPowerWithWork line 744
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:744 (same declaration text).
def OAI.EditApproximation.queryEncodedLEWithWork line 752
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:752 (same declaration text).
instance OAI.EditApproximation.largeAccuracyInput_decidable line 758
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:758 (same declaration text).
def OAI.EditApproximation.chargedSuffixDP line 761
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:761 (same declaration text).
def OAI.EditApproximation.computedCoarseDepth line 771
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:771 (same declaration text).
def OAI.EditApproximation.queryRangeValidWithWork line 773
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:773 (same declaration text).
def OAI.EditApproximation.coarsePaddedReadWithWork line 778
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:778 (same declaration text).
def OAI.EditApproximation.coarseRangeCopyWithWork line 784
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:784 (same declaration text).
def OAI.EditApproximation.bitMulAllocation line 791
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:791 (same declaration text).
def OAI.EditApproximation.bitDivModAllocation line 797
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:797 (same declaration text).
def OAI.EditApproximation.saturatingSubtractAllocation line 805
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:805 (same declaration text).
def OAI.EditApproximation.makeStateAllocation line 809
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:809 (same declaration text).
def OAI.EditApproximation.translatedEndpointAllocation line 813
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:813 (same declaration text).
def OAI.EditApproximation.wordInsertAllocation line 817
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:817 (same declaration text).
def OAI.EditApproximation.wordSortWithWork line 822
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:822 (same declaration text).
def OAI.EditApproximation.binaryGridRoundWithWork line 829
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:829 (same declaration text).
def OAI.EditApproximation.gridPointsWithWork line 834
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:834 (same declaration text).
def OAI.EditApproximation.seedGridSpacingWithWork line 846
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:846 (same declaration text).
def OAI.EditApproximation.balancedCutWithWork line 851
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:851 (same declaration text).
def OAI.EditApproximation.triangularMassWithWork line 857
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:857 (same declaration text).
def OAI.EditApproximation.refinementBaseWithWork line 863
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:863 (same declaration text).
def OAI.EditApproximation.queryPairWithWork line 869
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:869 (same declaration text).
def OAI.EditApproximation.queryCellValidWithWork line 881
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:881 (same declaration text).
def OAI.EditApproximation.queryFinOfNatWithWork line 887
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:887 (same declaration text).
def OAI.EditApproximation.coarseDenominatorWithWork line 1064
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1064 (same declaration text).
def OAI.EditApproximation.coarseFramedReadWithWork line 1075
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1075 (same declaration text).
def OAI.EditApproximation.coarseDescriptorWithWork line 1087
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1087 (same declaration text).
def OAI.EditApproximation.coarseChildOffsetWithWork line 1094
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1094 (same declaration text).
def OAI.EditApproximation.coarseInputGuardWithWork line 1099
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1099 (same declaration text).
def OAI.EditApproximation.bitPowerAllocation line 1106
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1106 (same declaration text).
def OAI.EditApproximation.bitCeilDivAllocation line 1113
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1113 (same declaration text).
def OAI.EditApproximation.binaryNaturalMulAllocation line 1119
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1119 (same declaration text).
def OAI.EditApproximation.binaryNaturalDivAllocation line 1121
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1121 (same declaration text).
def OAI.EditApproximation.triangularMassAllocation line 1123
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1123 (same declaration text).
def OAI.EditApproximation.binaryIntervalRoundWithWork line 1130
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1130 (same declaration text).
def OAI.EditApproximation.computedQueryBase line 1135
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1135 (same declaration text).
def OAI.EditApproximation.coarsePreparedSlicesWithWork line 1138
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1138 (same declaration text).
def OAI.EditApproximation.gridPointsAllocation line 1146
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1146 (same declaration text).
def OAI.EditApproximation.balancedCutAllocation line 1157
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1157 (same declaration text).
def OAI.EditApproximation.seedGridSpacingAllocation line 1163
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1163 (same declaration text).
def OAI.EditApproximation.queryCellValidAllocation line 1166
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1166 (same declaration text).
def OAI.EditApproximation.queryPairAllocation line 1171
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1171 (same declaration text).
def OAI.EditApproximation.binaryGridRoundAllocation line 1180
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1180 (same declaration text).
def OAI.EditApproximation.wordSortAllocation line 1184
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1184 (same declaration text).
def OAI.EditApproximation.reduceOnlineIntegerAllocation line 1189
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1189 (same declaration text).
def OAI.EditApproximation.coarsePreparedInputStorage line 1193
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1193 (same declaration text).
def OAI.EditApproximation.optimizerTriangularMass line 1208
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1208 (same declaration text).
def OAI.EditApproximation.rationalLogApproximation line 1210
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1210 (same declaration text).
def OAI.EditApproximation.rationalLinearizationMaximizer line 1213
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1213 (same declaration text).
def OAI.EditApproximation.bandCoordinates line 1217
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1217 (same declaration text).
def OAI.EditApproximation.actionVector line 1221
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1221 (same declaration text).
def OAI.EditApproximation.rationalOptimisticHistory line 1225
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1225 (same declaration text).
def OAI.EditApproximation.rejectionBitCount line 1229
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1229 (same declaration text).
def OAI.EditApproximation.vectorMapWithWork line 1231
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1231 (same declaration text).
def OAI.EditApproximation.TreeLayer line 1235
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1235 (same declaration text).
def OAI.EditApproximation.intervalTreeDepth line 1239
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1239 (same declaration text).
def OAI.EditApproximation.rationalMaximum line 1241
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1241 (same declaration text).
def OAI.EditApproximation.rationalDyadicCeiling line 1245
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1245 (same declaration text).
def OAI.EditApproximation.listedBandCoordinates line 1247
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1247 (same declaration text).
def OAI.EditApproximation.childGain line 1251
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1251 (same declaration text).
def OAI.EditApproximation.childDecrement line 1254
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1254 (same declaration text).
def OAI.EditApproximation.naturalEqualWithWork line 1257
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1257 (same declaration text).
def OAI.EditApproximation.translatedEndpointWithWork line 1261
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1261 (same declaration text).
def OAI.EditApproximation.rationalOnlineMinimum line 1266
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1266 (same declaration text).
def OAI.EditApproximation.dyadicQueryWindow line 1270
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1270 (same declaration text).
def OAI.EditApproximation.actionCurrentInputCover line 1273
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1273 (same declaration text).
def OAI.EditApproximation.boundedOnlineInteger line 1278
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1278 (same declaration text).
def OAI.EditApproximation.orderedInputs line 1281
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1281 (same declaration text).
def OAI.EditApproximation.CoarseThresholdDraws line 1286
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1286 (same declaration text).
def OAI.EditApproximation.coarseThresholdContribution line 1290
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1290 (same declaration text).
def OAI.EditApproximation.coarseChildThreshold line 1293
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1293 (same declaration text).
def OAI.EditApproximation.coarseCommonDenominator line 1296
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1296 (same declaration text).
def OAI.EditApproximation.rationalSmoothedGradient line 1299
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1299 (same declaration text).
def OAI.EditApproximation.rationalOnlineLinear line 1302
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1302 (same declaration text).
def OAI.EditApproximation.triangularChoice line 1306
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1306 (same declaration text).
instance OAI.EditApproximation.treeLayerFintype line 1313
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1313 (same declaration text).
abbrev OAI.EditApproximation.PhysicalNode line 1319
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1319 (same declaration text).
def OAI.EditApproximation.finiteRationalOptimizer line 1321
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1321 (same declaration text).
instance OAI.EditApproximation.physicalNodeFintype line 1330
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1330 (same declaration text).
abbrev OAI.EditApproximation.PhysicalInternalNode line 1332
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1332 (same declaration text).
def OAI.EditApproximation.finiteOptimizerAction line 1334
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1334 (same declaration text).
def OAI.EditApproximation.finiteOptimizerActionDraw line 1343
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1343 (same declaration text).
def OAI.EditApproximation.BinaryFraction.width line 1357
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1357 (same declaration text).
def OAI.EditApproximation.BinaryFraction.denominatorInteger line 1359
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1359 (same declaration text).
def OAI.EditApproximation.BinaryFraction.zero line 1361
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1361 (same declaration text).
def OAI.EditApproximation.BinaryFraction.canonicalizeWithWork line 1363
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1363 (same declaration text).
def OAI.EditApproximation.BinaryFraction.inversePowerTwo line 1381
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1381 (same declaration text).
def OAI.EditApproximation.BinaryFraction.doubleFraction line 1393
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1393 (same declaration text).
def OAI.EditApproximation.BinaryFraction.absolute line 1396
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1396 (same declaration text).
def OAI.EditApproximation.BinaryFraction.naturalCeilingWithWork line 1399
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1399 (same declaration text).
def OAI.EditApproximation.BinaryFraction.ofNaturalWord line 1405
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1405 (same declaration text).
def OAI.EditApproximation.BinaryFraction.naturalFloorWithWork line 1408
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1408 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryDataReadBudget line 1413
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1413 (same declaration text).
def OAI.EditApproximation.BinaryFraction.onlineParametersWithWork line 1416
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1416 (same declaration text).
def OAI.EditApproximation.BinaryFraction.refinementDecrementWithWork line 1477
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1477 (same declaration text).
abbrev OAI.EditApproximation.BinaryFraction.CoarseBinaryArray line 1534
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1534 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseRootDenominator line 1536
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1536 (same declaration text).
def OAI.EditApproximation.BinaryFraction.naturalListEqualWithWork line 1539
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1539 (same declaration text).
def OAI.EditApproximation.BinaryFraction.canonicalizeAllocation line 1549
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1549 (same declaration text).
def OAI.EditApproximation.BinaryFraction.invAllocation line 1552
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1552 (same declaration text).
def OAI.EditApproximation.BinaryFraction.naturalCeilingAllocation line 1555
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1555 (same declaration text).
def OAI.EditApproximation.BinaryFraction.gatheredLookupAllocation line 1558
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1558 (same declaration text).
def OAI.EditApproximation.BinaryFraction.naturalFloorAllocation line 1565
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1565 (same declaration text).
def OAI.EditApproximation.BinaryFraction.signedPowerTwoAllocation line 1568
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1568 (same declaration text).
def OAI.EditApproximation.BinaryFraction.invWithWork line 1571
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1571 (same declaration text).
def OAI.EditApproximation.BinaryFraction.signedPowerTwoWithWork line 1611
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1611 (same declaration text).
def OAI.EditApproximation.BinaryFraction.fixedDenominatorWithWork line 1616
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1616 (same declaration text).
def OAI.EditApproximation.BinaryFraction.finalAnswerWithWork line 1624
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1624 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseGridNatWithWork line 1629
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1629 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseBinaryMapWithWork line 1636
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1636 (same declaration text).
def OAI.EditApproximation.BinaryFraction.fixedDenominatorAllocation line 1643
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1643 (same declaration text).
def OAI.EditApproximation.BinaryFraction.finalAnswerAllocation line 1651
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1651 (same declaration text).
def OAI.EditApproximation.BinaryFraction.powerDenominatorWithWork line 1654
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1654 (same declaration text).
def OAI.EditApproximation.BinaryFraction.powerDenominatorAllocation line 1713
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1713 (same declaration text).
def OAI.EditApproximation.BinaryFraction.finishCachedWithWork line 1769
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1769 (same declaration text).
def OAI.EditApproximation.BinaryFraction.finishCachedAllocation line 1774
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1774 (same declaration text).
def OAI.EditApproximation.physicalChild line 1787
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1787 (same declaration text).
instance OAI.EditApproximation.treeLayerDecidableEq line 1791
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1791 (same declaration text).
def OAI.EditApproximation.treeLayerCode line 1797
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1797 (same declaration text).
def OAI.EditApproximation.localOnlineMassBound line 1801
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1801 (same declaration text).
def OAI.EditApproximation.treeLayerCodeWithWork line 1804
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1804 (same declaration text).
def OAI.EditApproximation.queryNaturalIndexWithWork line 1809
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1809 (same declaration text).
def OAI.EditApproximation.scheduledSeedWordWithWork line 1818
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1818 (same declaration text).
def OAI.EditApproximation.coarseLetterMatchWithWork line 1822
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1822 (same declaration text).
def OAI.EditApproximation.queryNaturalIndexAllocation line 1828
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1828 (same declaration text).
def OAI.EditApproximation.physicalNodeCode line 1833
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1833 (same declaration text).
def OAI.EditApproximation.queryScaleDispatchWithWork line 1836
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1836 (same declaration text).
def OAI.EditApproximation.queryScaleDispatchAllocation line 1841
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1841 (same declaration text).
def OAI.EditApproximation.queryScalePresentWithWork line 1845
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1845 (same declaration text).
def OAI.EditApproximation.queryScalePresentAllocation line 1850
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1850 (same declaration text).
def OAI.EditApproximation.physicalScaleIndex line 1862
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1862 (same declaration text).
abbrev OAI.EditApproximation.PositiveDrawRange line 1866
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1866 (same declaration text).
abbrev OAI.EditApproximation.PhysicalLocalGroupKey line 1868
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1868 (same declaration text).
def OAI.EditApproximation.rejectionSuccessParameter line 1872
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1872 (same declaration text).
def OAI.EditApproximation.scheduledSeedFactor line 1876
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1876 (same declaration text).
def OAI.EditApproximation.scheduledSeedMultiplier line 1879
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1879 (same declaration text).
instance OAI.EditApproximation.computedBranching_neZero line 1882
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1882 (same declaration text).
instance OAI.EditApproximation.computedCoarseBranching_neZero line 1885
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1885 (same declaration text).
instance OAI.EditApproximation.computedSourceTime_neZero line 1888
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1888 (same declaration text).
abbrev OAI.EditApproximation.CommonRangeKey line 1891
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1891 (same declaration text).
def OAI.EditApproximation.positiveDrawRangeOfLE line 1893
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1893 (same declaration text).
instance OAI.EditApproximation.positiveDrawRange_nezero line 1896
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1896 (same declaration text).
def OAI.EditApproximation.SignedBinary.value line 1908
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1908 (same declaration text).
def OAI.EditApproximation.SignedBinary.ofInt line 1910
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1910 (same declaration text).
def OAI.EditApproximation.SignedBinary.neg line 1912
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1912 (same declaration text).
def OAI.EditApproximation.SignedBinary.addWithWork line 1914
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1914 (same declaration text).
def OAI.EditApproximation.SignedBinary.mulWithWork line 1929
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1929 (same declaration text).
def OAI.EditApproximation.SignedBinary.nonzeroWithWork line 1933
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1933 (same declaration text).
def OAI.EditApproximation.SignedBinary.addAllocation line 1937
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1937 (same declaration text).
def OAI.EditApproximation.SignedBinary.mulAllocation line 1944
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1944 (same declaration text).
def OAI.EditApproximation.SignedBinary.ltWithWork line 1946
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1946 (same declaration text).
def OAI.EditApproximation.BinaryFraction.value line 1970
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1970 (same declaration text).
def OAI.EditApproximation.BinaryFraction.representation line 1972
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1972 (same declaration text).
def OAI.EditApproximation.BinaryFraction.addWithWork line 1975
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:1975 (same declaration text).
def OAI.EditApproximation.BinaryFraction.mulWithWork line 2021
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2021 (same declaration text).
def OAI.EditApproximation.BinaryFraction.neg line 2065
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2065 (same declaration text).
def OAI.EditApproximation.BinaryFraction.ltWithWork line 2068
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2068 (same declaration text).
def OAI.EditApproximation.BinaryFraction.nat line 2074
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2074 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseGridAddWithWork line 2077
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2077 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseReadShiftWithWork line 2083
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2083 (same declaration text).
def OAI.EditApproximation.BinaryFraction.addAllocation line 2093
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2093 (same declaration text).
def OAI.EditApproximation.BinaryFraction.mulAllocation line 2100
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2100 (same declaration text).
def OAI.EditApproximation.BinaryFraction.ltAllocation line 2103
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2103 (same declaration text).
def OAI.EditApproximation.BinaryFraction.canonicalAddWithWork line 2107
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2107 (same declaration text).
def OAI.EditApproximation.BinaryFraction.canonicalMulWithWork line 2112
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2112 (same declaration text).
def OAI.EditApproximation.BinaryFraction.one line 2117
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2117 (same declaration text).
def OAI.EditApproximation.BinaryFraction.dyadicScanWithWork line 2119
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2119 (same declaration text).
def OAI.EditApproximation.BinaryFraction.maxWithWork line 2128
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2128 (same declaration text).
def OAI.EditApproximation.BinaryFraction.leWithWork line 2132
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2132 (same declaration text).
def OAI.EditApproximation.BinaryFraction.minWithWork line 2136
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2136 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryScaleAt line 2140
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2140 (same declaration text).
def OAI.EditApproximation.BinaryFraction.gatheredWordLookupWithWork line 2144
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2144 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseGridZipAddWithWork line 2154
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2154 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseBinaryRead line 2161
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2161 (same declaration text).
def OAI.EditApproximation.BinaryFraction.canonicalAddAllocation line 2166
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2166 (same declaration text).
def OAI.EditApproximation.BinaryFraction.canonicalMulAllocation line 2169
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2169 (same declaration text).
def OAI.EditApproximation.BinaryFraction.minAllocation line 2172
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2172 (same declaration text).
def OAI.EditApproximation.BinaryFraction.maxAllocation line 2174
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2174 (same declaration text).
def OAI.EditApproximation.BinaryFraction.leAllocation line 2176
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2176 (same declaration text).
def OAI.EditApproximation.BinaryFraction.dyadicScanAllocation line 2178
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2178 (same declaration text).
def OAI.EditApproximation.BinaryFraction.equalAllocation line 2184
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2184 (same declaration text).
def OAI.EditApproximation.BinaryFraction.subWithWork line 2187
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2187 (same declaration text).
def OAI.EditApproximation.BinaryFraction.divWithWork line 2191
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2191 (same declaration text).
def OAI.EditApproximation.BinaryFraction.powWithWork line 2196
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2196 (same declaration text).
def OAI.EditApproximation.BinaryFraction.dotListWithWork line 2203
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2203 (same declaration text).
def OAI.EditApproximation.BinaryFraction.dyadicCeilingWithWork line 2211
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2211 (same declaration text).
def OAI.EditApproximation.BinaryFraction.maximumWithWork line 2215
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2215 (same declaration text).
def OAI.EditApproximation.BinaryFraction.minimumWithWork line 2222
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2222 (same declaration text).
def OAI.EditApproximation.BinaryFraction.scaledCeilingWithWork line 2229
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2229 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseContributionWithWork line 2234
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2234 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseGridScanWithWork line 2243
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2243 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseGridZipMinimumWithWork line 2252
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2252 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseBinaryAddWithWork line 2259
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2259 (same declaration text).
def OAI.EditApproximation.BinaryFraction.divAllocation line 2266
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2266 (same declaration text).
def OAI.EditApproximation.BinaryFraction.subAllocation line 2269
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2269 (same declaration text).
def OAI.EditApproximation.BinaryFraction.optimizerUpdateCellAllocation line 2271
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2271 (same declaration text).
def OAI.EditApproximation.BinaryFraction.dyadicCeilingAllocation line 2277
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2277 (same declaration text).
def OAI.EditApproximation.BinaryFraction.roundedSpacingAllocation line 2280
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2280 (same declaration text).
def OAI.EditApproximation.BinaryFraction.scaledCeilingAllocation line 2285
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2285 (same declaration text).
def OAI.EditApproximation.BinaryFraction.groupTermsAllocation line 2289
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2289 (same declaration text).
def OAI.EditApproximation.BinaryFraction.logarithmPartialWithWork line 2293
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2293 (same declaration text).
def OAI.EditApproximation.BinaryFraction.dotWithWork line 2302
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2302 (same declaration text).
def OAI.EditApproximation.BinaryFraction.distanceWithWork line 2305
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2305 (same declaration text).
def OAI.EditApproximation.BinaryFraction.affineErrorWithWork line 2309
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2309 (same declaration text).
def OAI.EditApproximation.BinaryFraction.bandToleranceWithWork line 2317
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2317 (same declaration text).
def OAI.EditApproximation.BinaryFraction.medianSeedWithWork line 2323
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2323 (same declaration text).
def OAI.EditApproximation.BinaryFraction.groupSampleCountWithWork line 2330
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2330 (same declaration text).
def OAI.EditApproximation.BinaryFraction.gainReadWithWork line 2339
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2339 (same declaration text).
def OAI.EditApproximation.BinaryFraction.decrementReadWithWork line 2345
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2345 (same declaration text).
def OAI.EditApproximation.BinaryFraction.scaledSeedWithWork line 2353
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2353 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialScaleGuardWithWork line 2359
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2359 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialCenterGuardWithWork line 2370
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2370 (same declaration text).
def OAI.EditApproximation.BinaryFraction.cellCoordinatesWithWork line 2378
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2378 (same declaration text).
def OAI.EditApproximation.BinaryFraction.cellGridPointsWithWork line 2391
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2391 (same declaration text).
def OAI.EditApproximation.BinaryFraction.centerEligibilityWithWork line 2407
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2407 (same declaration text).
def OAI.EditApproximation.BinaryFraction.refinementScaleGuardWithWork line 2417
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2417 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseDivideWithWork line 2427
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2427 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseGridLeftWithWork line 2432
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2432 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseMinimumWithWork line 2436
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2436 (same declaration text).
def OAI.EditApproximation.BinaryFraction.powAllocation line 2440
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2440 (same declaration text).
def OAI.EditApproximation.BinaryFraction.dotListAllocation line 2444
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2444 (same declaration text).
def OAI.EditApproximation.BinaryFraction.minimumAllocation line 2450
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2450 (same declaration text).
def OAI.EditApproximation.BinaryFraction.maximumAllocation line 2455
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2455 (same declaration text).
def OAI.EditApproximation.BinaryFraction.distanceAllocation line 2460
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2460 (same declaration text).
def OAI.EditApproximation.BinaryFraction.optimizerUpdateAllocation line 2462
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2462 (same declaration text).
def OAI.EditApproximation.BinaryFraction.affineErrorAllocation line 2469
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2469 (same declaration text).
def OAI.EditApproximation.BinaryFraction.bandToleranceAllocation line 2475
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2475 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialScaleGuardAllocation line 2481
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2481 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialCenterGuardAllocation line 2491
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2491 (same declaration text).
def OAI.EditApproximation.BinaryFraction.scaledSeedAllocation line 2498
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2498 (same declaration text).
def OAI.EditApproximation.BinaryFraction.centerEligibilityAllocation line 2504
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2504 (same declaration text).
def OAI.EditApproximation.BinaryFraction.refinementScaleGuardAllocation line 2512
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2512 (same declaration text).
def OAI.EditApproximation.BinaryFraction.cellCoordinatesAllocation line 2520
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2520 (same declaration text).
def OAI.EditApproximation.BinaryFraction.cellGridPointsAllocation line 2536
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2536 (same declaration text).
def OAI.EditApproximation.BinaryFraction.medianSeedAllocation line 2553
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2553 (same declaration text).
def OAI.EditApproximation.BinaryFraction.groupSampleCountAllocation line 2560
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2560 (same declaration text).
def OAI.EditApproximation.BinaryFraction.refinementUpdateAllocation line 2569
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2569 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coefficientAllocation line 2578
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2578 (same declaration text).
def OAI.EditApproximation.BinaryFraction.gainReadAllocation line 2581
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2581 (same declaration text).
def OAI.EditApproximation.BinaryFraction.decrementReadAllocation line 2586
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2586 (same declaration text).
def OAI.EditApproximation.BinaryFraction.logarithmWithWork line 2592
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2592 (same declaration text).
def OAI.EditApproximation.BinaryFraction.optimisticTermReadWithWork line 2600
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2600 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryExponentsWithWork line 2609
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2609 (same declaration text).
def OAI.EditApproximation.BinaryFraction.seedMedianWithWork line 2616
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2616 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseGridPenaltyWithWork line 2621
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2621 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseChildThresholdWithWork line 2628
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2628 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseChildAllowanceWithWork line 2635
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2635 (same declaration text).
def OAI.EditApproximation.BinaryFraction.logarithmPartialAllocation line 2639
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2639 (same declaration text).
def OAI.EditApproximation.BinaryFraction.bandMassAllocation line 2648
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2648 (same declaration text).
def OAI.EditApproximation.BinaryFraction.sumListAllocation line 2651
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2651 (same declaration text).
def OAI.EditApproximation.BinaryFraction.naturalDistanceLeAllocation line 2655
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2655 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryExponentsAllocation line 2659
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2659 (same declaration text).
def OAI.EditApproximation.BinaryFraction.seedMedianAllocation line 2666
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2666 (same declaration text).
def OAI.EditApproximation.BinaryFraction.onlineMinimumAllocation line 2670
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2670 (same declaration text).
def OAI.EditApproximation.BinaryFraction.optimisticTermReadAllocation line 2674
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2674 (same declaration text).
def OAI.EditApproximation.BinaryFraction.gradientCellWithWork line 2683
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2683 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryScalesWithWork line 2694
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2694 (same declaration text).
def OAI.EditApproximation.BinaryFraction.querySeedMedianWithWork line 2699
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2699 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseBinaryPenaltyWithWork line 2703
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2703 (same declaration text).
def OAI.EditApproximation.BinaryFraction.logarithmAllocation line 2709
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2709 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryScalesAllocation line 2716
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2716 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseIndexChildren line 2720
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2720 (same declaration text).
def OAI.EditApproximation.BinaryFraction.gradientCellAllocation line 2738
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2738 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseIndexedWithWork line 2749
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2749 (same declaration text).
def OAI.EditApproximation.BinaryFraction.gradientAllocation line 2784
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2784 (same declaration text).
def OAI.EditApproximation.BinaryFraction.gradientWithWork line 2796
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2796 (same declaration text).
def OAI.EditApproximation.BinaryFraction.scoredArgmaxWithWork line 2800
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2800 (same declaration text).
def OAI.EditApproximation.BinaryFraction.optimizerUpdateWithWork line 2813
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2813 (same declaration text).
def OAI.EditApproximation.BinaryFraction.bandMassTotalWithWork line 2824
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2824 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coefficientWithWork line 2827
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2827 (same declaration text).
def OAI.EditApproximation.BinaryFraction.naturalDistanceLeWithWork line 2832
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2832 (same declaration text).
def OAI.EditApproximation.BinaryFraction.onlineMinimumWithWork line 2837
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2837 (same declaration text).
def OAI.EditApproximation.BinaryFraction.refinementUpdateWithWork line 2843
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2843 (same declaration text).
def OAI.EditApproximation.BinaryFraction.equalWithWork line 2852
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2852 (same declaration text).
def OAI.EditApproximation.BinaryFraction.roundedSpacingWithWork line 2857
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2857 (same declaration text).
def OAI.EditApproximation.BinaryFraction.maximizerWithWork line 2863
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2863 (same declaration text).
def OAI.EditApproximation.BinaryFraction.groupTermsWithWork line 2868
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2868 (same declaration text).
def OAI.EditApproximation.BinaryFraction.selectGroupWithWork line 2874
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2874 (same declaration text).
def OAI.EditApproximation.BinaryFraction.finiteOptimizerWithWork line 2881
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2881 (same declaration text).
def OAI.EditApproximation.BinaryFraction.selectionWithWork line 2891
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2891 (same declaration text).
def OAI.EditApproximation.BitQuery.value line 2908
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2908 (same declaration text).
def OAI.EditApproximation.BitQuery.work line 2913
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2913 (same declaration text).
def OAI.EditApproximation.BitQuery.bind line 2918
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2918 (same declaration text).
def OAI.EditApproximation.BitQuery.compute line 2923
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2923 (same declaration text).
def OAI.EditApproximation.BitQuery.mapKeysWithWork line 2926
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2926 (same declaration text).
def OAI.EditApproximation.BitQuery.restrictWithWork line 2932
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2932 (same declaration text).
def OAI.EditApproximation.BitQuery.runMemo line 2942
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2942 (same declaration text).
inductive OAI.EditApproximation.BitQuery.Footprint line 2956
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2956 (same declaration text).
def OAI.EditApproximation.BitQuery.collect line 2963
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2963 (same declaration text).
def OAI.EditApproximation.BitQuery.normalize line 2969
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2969 (same declaration text).
def OAI.EditApproximation.substring line 2983
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2983 (same declaration text).
structure OAI.EditApproximation.TargetInterval line 2986
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2986 (same declaration text).
def OAI.EditApproximation.occurrenceDeficit line 2992
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2992 (same declaration text).
def OAI.EditApproximation.natListMinimum line 2995
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2995 (same declaration text).
def OAI.EditApproximation.coarsePadTo line 2999
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:2999 (same declaration text).
def OAI.EditApproximation.connectionBudget line 3002
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3002 (same declaration text).
def OAI.EditApproximation.singletonCost line 3008
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3008 (same declaration text).
def OAI.EditApproximation.makeTargetState line 3011
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3011 (same declaration text).
def OAI.EditApproximation.targetEndpointDistance line 3014
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3014 (same declaration text).
def OAI.EditApproximation.targetStates line 3017
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3017 (same declaration text).
def OAI.EditApproximation.shortSourceCost line 3021
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3021 (same declaration text).
def OAI.EditApproximation.exactSuffixDP line 3026
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3026 (same declaration text).
def OAI.EditApproximation.exactSuffixAnswer line 3035
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3035 (same declaration text).
def OAI.EditApproximation.sourceChild line 3047
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3047 (same declaration text).
def OAI.EditApproximation.roundInterval line 3071
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3071 (same declaration text).
def OAI.EditApproximation.localTargetStates line 3084
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3084 (same declaration text).
def OAI.EditApproximation.rationalStateGap line 3089
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3089 (same declaration text).
def OAI.EditApproximation.gridStateBox line 3092
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3092 (same declaration text).
abbrev OAI.EditApproximation.PhysicalEntry line 3097
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3097 (same declaration text).
def OAI.EditApproximation.makeStateWithWork line 3099
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3099 (same declaration text).
def OAI.EditApproximation.cellTargetStates line 3152
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3152 (same declaration text).
def OAI.EditApproximation.gridGapStates line 3156
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3156 (same declaration text).
abbrev OAI.EditApproximation.PhysicalChildTables line 3161
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3161 (same declaration text).
abbrev OAI.EditApproximation.PhysicalRationalAction line 3163
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3163 (same declaration text).
def OAI.EditApproximation.localTargetCells line 3166
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3166 (same declaration text).
def OAI.EditApproximation.coordinateEqualWithWork line 3170
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3170 (same declaration text).
def OAI.EditApproximation.queryIntervalEqualWithWork line 3176
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3176 (same declaration text).
def OAI.EditApproximation.childInputCode line 3181
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3181 (same declaration text).
def OAI.EditApproximation.queryChildCodeWithWork line 3184
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3184 (same declaration text).
def OAI.EditApproximation.querySliceHeadWithWork line 3192
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3192 (same declaration text).
def OAI.EditApproximation.rankedBitProgramValue line 3198
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3198 (same declaration text).
def OAI.EditApproximation.scheduledRefinementWordWithWork line 3205
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3205 (same declaration text).
def OAI.EditApproximation.coordinateEqualAllocation line 3213
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3213 (same declaration text).
def OAI.EditApproximation.queryIntervalEqualAllocation line 3217
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3217 (same declaration text).
def OAI.EditApproximation.sourceChildAllocation line 3220
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3220 (same declaration text).
def OAI.EditApproximation.zeroConnectionAllocation line 3227
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3227 (same declaration text).
def OAI.EditApproximation.queryChildCodeAllocation line 3232
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3232 (same declaration text).
def OAI.EditApproximation.roundStateAllocation line 3242
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3242 (same declaration text).
def OAI.EditApproximation.actionEqualAllocation line 3245
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3245 (same declaration text).
structure OAI.EditApproximation.RawUnskippedBand line 3249
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3249 (same declaration text).
def OAI.EditApproximation.sourceIntervalAt line 3254
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3254 (same declaration text).
def OAI.EditApproximation.initialConeValue line 3258
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3258 (same declaration text).
def OAI.EditApproximation.wideChildStateList line 3264
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3264 (same declaration text).
def OAI.EditApproximation.bandCutShift line 3270
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3270 (same declaration text).
def OAI.EditApproximation.localInitialConeCenters line 3274
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3274 (same declaration text).
def OAI.EditApproximation.gridStateBoxWithWork line 3281
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3281 (same declaration text).
def OAI.EditApproximation.sourceChildWithWork line 3291
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3291 (same declaration text).
def OAI.EditApproximation.cellRepresentativeStates line 3538
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3538 (same declaration text).
def OAI.EditApproximation.groupRoundedStateList line 3543
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3543 (same declaration text).
def OAI.EditApproximation.rawInitialConeCenters line 3551
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3551 (same declaration text).
def OAI.EditApproximation.historyInputCode line 3557
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3557 (same declaration text).
def OAI.EditApproximation.localOnlineSourceKeys line 3560
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3560 (same declaration text).
def OAI.EditApproximation.queryHistoryCodeWithWork line 3565
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3565 (same declaration text).
def OAI.EditApproximation.queryOrderedChildInputsWithWork line 3570
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3570 (same declaration text).
def OAI.EditApproximation.queryHistoryEqualWithWork line 3575
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3575 (same declaration text).
def OAI.EditApproximation.queryGapStatesWithWork line 3580
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3580 (same declaration text).
def OAI.EditApproximation.queryOnlineKeyEqualWithWork line 3594
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3594 (same declaration text).
def OAI.EditApproximation.physicalEntryCode line 3599
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3599 (same declaration text).
def OAI.EditApproximation.rankedBitLocalWork line 3602
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3602 (same declaration text).
def OAI.EditApproximation.refinementParameterWordsWithWork line 3607
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3607 (same declaration text).
def OAI.EditApproximation.queryHistoryEqualAllocation line 3615
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3615 (same declaration text).
def OAI.EditApproximation.queryOnlineKeyEqualAllocation line 3618
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3618 (same declaration text).
def OAI.EditApproximation.gridStateBoxAllocation line 3621
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3621 (same declaration text).
def OAI.EditApproximation.queryHistoryCodeAllocation line 3635
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3635 (same declaration text).
def OAI.EditApproximation.queryOrderedChildInputsAllocation line 3639
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3639 (same declaration text).
def OAI.EditApproximation.actionMemberAllocation line 3643
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3643 (same declaration text).
def OAI.EditApproximation.queryGapStatesAllocation line 3647
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3647 (same declaration text).
def OAI.EditApproximation.wideActionList line 3669
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3669 (same declaration text).
def OAI.EditApproximation.physicalSourceInterval line 3673
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3673 (same declaration text).
def OAI.EditApproximation.localInitialConeTable line 3676
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3676 (same declaration text).
def OAI.EditApproximation.wideChildGridWithWork line 3684
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3684 (same declaration text).
def OAI.EditApproximation.queryOrderedHistoryInputsWithWork line 3697
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3697 (same declaration text).
def OAI.EditApproximation.queryNeededInputsWithWork line 3702
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3702 (same declaration text).
def OAI.EditApproximation.computedQueryParameters line 3710
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3710 (same declaration text).
def OAI.EditApproximation.wideChildGridAllocation line 3723
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3723 (same declaration text).
def OAI.EditApproximation.queryOrderedHistoryInputsAllocation line 3738
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3738 (same declaration text).
def OAI.EditApproximation.queryNeededInputsAllocation line 3742
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3742 (same declaration text).
def OAI.EditApproximation.physicalSource line 3749
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3749 (same declaration text).
def OAI.EditApproximation.wideActionGridWithWork line 3752
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3752 (same declaration text).
def OAI.EditApproximation.physicalCoarsePreparationCost line 3758
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3758 (same declaration text).
def OAI.EditApproximation.wideActionGridAllocation line 3763
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3763 (same declaration text).
def OAI.EditApproximation.BinaryFraction.sumListWithWork line 3777
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3777 (same declaration text).
def OAI.EditApproximation.BinaryFraction.connectionTermsWithWork line 3781
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3781 (same declaration text).
def OAI.EditApproximation.BinaryFraction.bandEnvelopeReadWithWork line 3792
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3792 (same declaration text).
def OAI.EditApproximation.BinaryFraction.onlineLinearReadWithWork line 3801
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3801 (same declaration text).
def OAI.EditApproximation.BinaryFraction.targetCellsWithWork line 3812
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3812 (same declaration text).
def OAI.EditApproximation.BinaryFraction.cellStatesWithWork line 3820
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3820 (same declaration text).
def OAI.EditApproximation.BinaryFraction.bandCoordinatesWithWork line 3828
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3828 (same declaration text).
def OAI.EditApproximation.BinaryFraction.countedBandCoordinateWithWork line 3835
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3835 (same declaration text).
def OAI.EditApproximation.BinaryFraction.representativeScaleReadWithWork line 3842
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3842 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryRawCentersWithWork line 3855
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3855 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryWideInputsWithWork line 3866
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3866 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryRawHistoryInputsWithWork line 3876
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3876 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupRoundedStatesWithWork line 3887
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3887 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryOnlineIntegerReadWithWork line 3907
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3907 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryChildReadWithWork line 3913
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3913 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryHistoryReadWithWork line 3917
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3917 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryParentReadWithWork line 3921
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3921 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialGridReadWithWork line 3925
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3925 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryInitialConeCentersWithWork line 3936
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3936 (same declaration text).
def OAI.EditApproximation.BinaryFraction.connectionTermsAllocation line 3947
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3947 (same declaration text).
def OAI.EditApproximation.BinaryFraction.endpointDistanceAllocation line 3953
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3953 (same declaration text).
def OAI.EditApproximation.BinaryFraction.stateGapAllocation line 3958
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3958 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryChildReadAllocation line 3962
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3962 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryHistoryReadAllocation line 3966
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3966 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryOnlineIntegerReadAllocation line 3970
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3970 (same declaration text).
def OAI.EditApproximation.BinaryFraction.bandCoordinatesAllocation line 3976
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3976 (same declaration text).
def OAI.EditApproximation.BinaryFraction.scoredArgmaxAllocation line 3984
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3984 (same declaration text).
def OAI.EditApproximation.BinaryFraction.anchorGuardAllocation line 3993
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:3993 (same declaration text).
def OAI.EditApproximation.BinaryFraction.bandEnvelopeReadAllocation line 4002
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4002 (same declaration text).
def OAI.EditApproximation.BinaryFraction.targetCellsAllocation line 4012
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4012 (same declaration text).
def OAI.EditApproximation.BinaryFraction.cellStatesAllocation line 4019
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4019 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryRawCentersAllocation line 4026
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4026 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryOnlineKeysAllocation line 4039
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4039 (same declaration text).
def OAI.EditApproximation.BinaryFraction.representativeScaleReadAllocation line 4045
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4045 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryWideInputsAllocation line 4058
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4058 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryRawHistoryInputsAllocation line 4075
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4075 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupRoundedStatesAllocation line 4091
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4091 (same declaration text).
def OAI.EditApproximation.BinaryFraction.groupIndexAllocation line 4112
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4112 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryParentReadAllocation line 4117
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4117 (same declaration text).
def OAI.EditApproximation.BinaryFraction.onlineLinearReadAllocation line 4121
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4121 (same declaration text).
def OAI.EditApproximation.BinaryFraction.countedBandCoordinateAllocation line 4133
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4133 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryInitialConeCentersAllocation line 4139
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4139 (same declaration text).
def OAI.EditApproximation.BinaryFraction.connectionWithWork line 4154
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4154 (same declaration text).
def OAI.EditApproximation.BinaryFraction.envelopeVectorReadWithWork line 4160
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4160 (same declaration text).
def OAI.EditApproximation.BinaryFraction.bellmanActionReadWithWork line 4164
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4164 (same declaration text).
def OAI.EditApproximation.BinaryFraction.cellCentersReadWithWork line 4176
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4176 (same declaration text).
def OAI.EditApproximation.BinaryFraction.countedBandVerticesWithWork line 4188
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4188 (same declaration text).
def OAI.EditApproximation.BinaryFraction.onlineIndexSetupWithWork line 4198
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4198 (same declaration text).
def OAI.EditApproximation.BinaryFraction.localRepresentativeReadWithWork line 4206
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4206 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupKeysWithWork line 4216
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4216 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryMeanWithWork line 4227
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4227 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialCentersReadWithWork line 4232
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4232 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryInitialSeedReadWithWork line 4242
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4242 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryOverrideParentReadWithWork line 4253
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4253 (same declaration text).
def OAI.EditApproximation.BinaryFraction.connectionAllocation line 4262
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4262 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coordinateVectorAllocation line 4267
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4267 (same declaration text).
def OAI.EditApproximation.BinaryFraction.maximizerAllocation line 4270
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4270 (same declaration text).
def OAI.EditApproximation.BinaryFraction.onlineIndexSetupAllocation line 4275
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4275 (same declaration text).
def OAI.EditApproximation.BinaryFraction.envelopeVectorReadAllocation line 4282
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4282 (same declaration text).
def OAI.EditApproximation.BinaryFraction.roundedBandReadAllocation line 4287
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4287 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupKeysAllocation line 4297
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4297 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialCellAllocation line 4311
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4311 (same declaration text).
def OAI.EditApproximation.BinaryFraction.localRepresentativeReadAllocation line 4316
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4316 (same declaration text).
def OAI.EditApproximation.BinaryFraction.cellCentersReadAllocation line 4325
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4325 (same declaration text).
def OAI.EditApproximation.BinaryFraction.selectGroupAllocation line 4337
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4337 (same declaration text).
def OAI.EditApproximation.BinaryFraction.bellmanActionReadAllocation line 4341
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4341 (same declaration text).
def OAI.EditApproximation.BinaryFraction.countedBandVerticesAllocation line 4355
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4355 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryInitialSeedReadAllocation line 4362
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4362 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryOverrideParentReadAllocation line 4368
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4368 (same declaration text).
def OAI.EditApproximation.BinaryFraction.prefixReadWithWork line 4373
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4373 (same declaration text).
def OAI.EditApproximation.BinaryFraction.bellmanReadWithWork line 4385
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4385 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryWarmupInputsWithWork line 4393
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4393 (same declaration text).
def OAI.EditApproximation.BinaryFraction.endpointConnectionAllocation line 4400
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4400 (same declaration text).
def OAI.EditApproximation.BinaryFraction.prefixReadAllocation line 4404
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4404 (same declaration text).
def OAI.EditApproximation.BinaryFraction.optimizerAllocation line 4418
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4418 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryEarlierRepresentativesAllocation line 4428
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4428 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryWarmupInputsAllocation line 4446
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4446 (same declaration text).
def OAI.EditApproximation.BinaryFraction.bellmanReadAllocation line 4453
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4453 (same declaration text).
def OAI.EditApproximation.BinaryFraction.prefixMinimumReadWithWork line 4461
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4461 (same declaration text).
def OAI.EditApproximation.BinaryFraction.localContinuationReadWithWork line 4470
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4470 (same declaration text).
def OAI.EditApproximation.BinaryFraction.prefixMinimumReadAllocation line 4481
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4481 (same declaration text).
def OAI.EditApproximation.BinaryFraction.localContinuationReadAllocation line 4491
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4491 (same declaration text).
def OAI.EditApproximation.BinaryFraction.endpointActionAllocation line 4505
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4505 (same declaration text).
def OAI.EditApproximation.BinaryFraction.selectionAllocation line 4508
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4508 (same declaration text).
def OAI.EditApproximation.BinaryFraction.cutGuardReadWithWork line 4517
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4517 (same declaration text).
def OAI.EditApproximation.BinaryFraction.cutGuardReadAllocation line 4529
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4529 (same declaration text).
def OAI.EditApproximation.BinaryFraction.bandPredicateReadAllocation line 4544
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4544 (same declaration text).
def OAI.EditApproximation.rationalConnectionBudget line 4564
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4564 (same declaration text).
def OAI.EditApproximation.bandChildEnvelope line 4568
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4568 (same declaration text).
def OAI.EditApproximation.bandEnvelopeExponent line 4574
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4574 (same declaration text).
def OAI.EditApproximation.zeroConnectionWithWork line 4580
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4580 (same declaration text).
def OAI.EditApproximation.roundStateWithWork line 4587
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4587 (same declaration text).
def OAI.EditApproximation.actionEqualWithWork line 4811
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4811 (same declaration text).
def OAI.EditApproximation.localRefinementRepresentatives line 4817
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4817 (same declaration text).
def OAI.EditApproximation.sharedBandRationalAction line 4824
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4824 (same declaration text).
def OAI.EditApproximation.localGroupQueryKeys line 4828
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4828 (same declaration text).
def OAI.EditApproximation.rationalWidePrefixCost line 4833
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4833 (same declaration text).
def OAI.EditApproximation.bandRoundSpacing line 4840
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4840 (same declaration text).
def OAI.EditApproximation.actionMemberWithWork line 4844
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4844 (same declaration text).
def OAI.EditApproximation.wideEarlierInputCover line 4852
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4852 (same declaration text).
def OAI.EditApproximation.queryEarlierRepresentatives line 4859
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4859 (same declaration text).
def OAI.EditApproximation.rationalWidePrefixMinimum line 4868
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4868 (same declaration text).
def OAI.EditApproximation.roundedBandAction line 4874
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4874 (same declaration text).
def OAI.EditApproximation.queryEarlierInputCover line 4880
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4880 (same declaration text).
def OAI.EditApproximation.canonicalRoundedBandAction line 4886
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4886 (same declaration text).
def OAI.EditApproximation.parameterClogWithWork line 4900
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4900 (same declaration text).
def OAI.EditApproximation.parameterLogWithWork line 4904
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4904 (same declaration text).
def OAI.EditApproximation.parameterRootSearch line 4908
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4908 (same declaration text).
def OAI.EditApproximation.parameterPowerWithWork line 4914
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4914 (same declaration text).
def OAI.EditApproximation.physicalCoarseInputStorage line 4919
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4919 (same declaration text).
def OAI.EditApproximation.computedQueryPassWithWork line 4924
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4924 (same declaration text).
def OAI.EditApproximation.storedIntegerBits line 4937
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4937 (same declaration text).
def OAI.EditApproximation.parameterSqrtWithWork line 4940
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4940 (same declaration text).
def OAI.EditApproximation.computedQuerySetupWithWork line 4942
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4942 (same declaration text).
def OAI.EditApproximation.integerParametersWithWork line 4948
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4948 (same declaration text).
structure OAI.EditApproximation.PhysicalTableRequest line 4979
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4979 (same declaration text).
def OAI.EditApproximation.rawRefinementCenters line 4988
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4988 (same declaration text).
def OAI.EditApproximation.wideWarmupInputs line 4993
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4993 (same declaration text).
def OAI.EditApproximation.queryMeanRead line 4998
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:4998 (same declaration text).
def OAI.EditApproximation.physicalNodeCodeWithWork line 5003
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5003 (same declaration text).
def OAI.EditApproximation.rationalParametersWithWork line 5008
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5008 (same declaration text).
def OAI.EditApproximation.onlineMassWithWork line 5019
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5019 (same declaration text).
def OAI.EditApproximation.refinementInitialSupport line 5026
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5026 (same declaration text).
def OAI.EditApproximation.refinementBandInputList line 5034
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5034 (same declaration text).
def OAI.EditApproximation.previousPassRequest line 5039
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5039 (same declaration text).
def OAI.EditApproximation.physicalEntryCodeWithWork line 5043
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5043 (same declaration text).
def OAI.EditApproximation.queryPhysicalBoundedWithWork line 5048
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5048 (same declaration text).
def OAI.EditApproximation.globalParameterWork line 5057
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5057 (same declaration text).
def OAI.EditApproximation.physicalLargeInputWithWork line 5061
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5061 (same declaration text).
def OAI.EditApproximation.physicalTableCodeAllocation line 5074
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5074 (same declaration text).
def OAI.EditApproximation.queryPhysicalBoundedAllocation line 5077
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5077 (same declaration text).
def OAI.EditApproximation.physicalTableCodeWithWork line 5082
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5082 (same declaration text).
def OAI.EditApproximation.PhysicalTableRequest.remainingDepth line 5099
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5099 (same declaration text).
def OAI.EditApproximation.PhysicalTableRequest.rank line 5102
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5102 (same declaration text).
def OAI.EditApproximation.PhysicalTableRequest.Bounded line 5105
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5105 (same declaration text).
def OAI.EditApproximation.PhysicalTableRequest.warmup line 5108
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5108 (same declaration text).
def OAI.EditApproximation.PhysicalTableRequest.refinement line 5112
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5112 (same declaration text).
def OAI.EditApproximation.PhysicalTableRequest.sameIndexChild line 5116
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5116 (same declaration text).
def OAI.EditApproximation.PhysicalTableRequest.combinedRank line 5121
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5121 (same declaration text).
def OAI.EditApproximation.physicalWarmupChildQuery line 5133
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5133 (same declaration text).
def OAI.EditApproximation.physicalRefinementCurrentQuery line 5172
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5172 (same declaration text).
def OAI.EditApproximation.physicalRefinementEarlierQuery line 5204
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5204 (same declaration text).
def OAI.EditApproximation.physicalRefinementWarmupRead line 5241
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5241 (same declaration text).
def OAI.EditApproximation.previousPassRead line 5267
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5267 (same declaration text).
abbrev OAI.EditApproximation.ChargedPhysicalRequest line 5303
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5303 (same declaration text).
def OAI.EditApproximation.chargedPreviousPass line 5307
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5307 (same declaration text).
def OAI.EditApproximation.queryPhysicalTableRead line 5314
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5314 (same declaration text).
abbrev OAI.EditApproximation.ComputedFamilyTableKey line 5321
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5321 (same declaration text).
def OAI.EditApproximation.chargedPhysicalCodeWithWork line 5326
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5326 (same declaration text).
def OAI.EditApproximation.queryPhysicalWarmupRead line 5333
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5333 (same declaration text).
def OAI.EditApproximation.queryPhysicalCurrentRead line 5360
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5360 (same declaration text).
def OAI.EditApproximation.queryPhysicalEarlierRead line 5393
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5393 (same declaration text).
def OAI.EditApproximation.chargedPhysicalRemaining line 5471
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5471 (same declaration text).
def OAI.EditApproximation.chargedPhysicalCodeAllocation line 5476
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5476 (same declaration text).
def OAI.EditApproximation.queryPhysicalMassRead line 5481
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5481 (same declaration text).
def OAI.EditApproximation.integerClosedRange line 5499
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5499 (same declaration text).
def OAI.EditApproximation.groupSampleCount line 5502
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5502 (same declaration text).
def OAI.EditApproximation.groupScaleTrueCost line 5504
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5504 (same declaration text).
def OAI.EditApproximation.selectGroupMember line 5507
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5507 (same declaration text).
instance OAI.EditApproximation.coarseDrawsMeasurableSpace line 5511
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5511 (same declaration text).
def OAI.EditApproximation.groupDyadicScales line 5520
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5520 (same declaration text).
def OAI.EditApproximation.groupScaleEstimate line 5524
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5524 (same declaration text).
def OAI.EditApproximation.coarseDrawMeasure line 5529
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5529 (same declaration text).
def OAI.EditApproximation.groupMemberEstimate line 5537
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5537 (same declaration text).
def OAI.EditApproximation.BinaryFraction.groupScalesWithWork line 5551
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5551 (same declaration text).
def OAI.EditApproximation.BinaryFraction.bandPredicateReadWithWork line 5556
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5556 (same declaration text).
def OAI.EditApproximation.BinaryFraction.indexedGroupScales line 5574
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5574 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryOnlineKeysWithWork line 5582
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5582 (same declaration text).
def OAI.EditApproximation.BinaryFraction.groupScalesAllocation line 5790
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5790 (same declaration text).
def OAI.EditApproximation.BinaryFraction.bandFromActionsReadWithWork line 5795
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5795 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryInitialSupportWithWork line 5808
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5808 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryEarlierRepresentativesWithWork line 5822
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5822 (same declaration text).
def OAI.EditApproximation.BinaryFraction.bandFromActionsReadAllocation line 5836
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5836 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryInitialSupportAllocation line 5848
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5848 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryBandInputsWithWork line 5864
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5864 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryEarlierInputsWithWork line 5872
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5872 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryEarlierInputsAllocation line 5881
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5881 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryBandInputsAllocation line 5890
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5890 (same declaration text).
def OAI.EditApproximation.FiniteQuery.run line 5906
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5906 (same declaration text).
def OAI.EditApproximation.FiniteQuery.bind line 5915
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5915 (same declaration text).
def OAI.EditApproximation.FiniteQuery.mapKeys line 5919
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5919 (same declaration text).
def OAI.EditApproximation.FiniteQuery.restrict line 5923
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5923 (same declaration text).
def OAI.EditApproximation.FiniteQuery.requestWork line 5929
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5929 (same declaration text).
def OAI.EditApproximation.FiniteQuery.collect line 5936
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5936 (same declaration text).
def OAI.EditApproximation.physicalInitialQuery line 5951
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5951 (same declaration text).
def OAI.EditApproximation.queryInitialGather line 5965
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5965 (same declaration text).
def OAI.EditApproximation.queryBandGather line 5973
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5973 (same declaration text).
def OAI.EditApproximation.physicalRefinementMassQuery line 5983
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5983 (same declaration text).
def OAI.EditApproximation.physicalMedianSeedQuery line 5993
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:5993 (same declaration text).
def OAI.EditApproximation.globalSeedRead line 6001
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6001 (same declaration text).
def OAI.EditApproximation.UnreducedRational.value line 6021
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6021 (same declaration text).
def OAI.EditApproximation.UnreducedRational.zero line 6023
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6023 (same declaration text).
def OAI.EditApproximation.UnreducedRational.mul line 6025
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6025 (same declaration text).
def OAI.EditApproximation.UnreducedRational.lt line 6028
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6028 (same declaration text).
def OAI.EditApproximation.UnreducedRational.inv line 6030
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6030 (same declaration text).
def OAI.EditApproximation.UnreducedRational.div line 6034
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6034 (same declaration text).
inductive OAI.EditApproximation.CoarseSourceTree line 6045
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6045 (same declaration text).
def OAI.EditApproximation.coarseTargetFrame line 6049
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6049 (same declaration text).
def OAI.EditApproximation.coarseRootShift line 6052
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6052 (same declaration text).
def OAI.EditApproximation.endpointActionConnection line 6054
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6054 (same declaration text).
def OAI.EditApproximation.coarseSourceTreeOfList line 6058
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6058 (same declaration text).
def OAI.EditApproximation.BinaryFraction.groupIndexWithWork line 6073
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6073 (same declaration text).
def OAI.EditApproximation.BinaryFraction.endpointDistanceWithWork line 6079
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6079 (same declaration text).
def OAI.EditApproximation.BinaryFraction.endpointConnectionWithWork line 6086
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6086 (same declaration text).
def OAI.EditApproximation.BinaryFraction.stateGapWithWork line 6091
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6091 (same declaration text).
def OAI.EditApproximation.BinaryFraction.groupScaleSourceWithWork line 6105
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6105 (same declaration text).
def OAI.EditApproximation.BinaryFraction.endpointScoreReadWithWork line 6113
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6113 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialConeWithWork line 6122
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6122 (same declaration text).
def OAI.EditApproximation.BinaryFraction.endpointActionWithWork line 6131
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6131 (same declaration text).
def OAI.EditApproximation.BinaryFraction.endpointScoreReadAllocation line 6137
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6137 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialConeAllocation line 6145
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6145 (same declaration text).
def OAI.EditApproximation.BinaryFraction.groupScaleSourceAllocation line 6154
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6154 (same declaration text).
def OAI.EditApproximation.BinaryFraction.gapGuardAllocation line 6165
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6165 (same declaration text).
def OAI.EditApproximation.BinaryFraction.wideMinimumReadWithWork line 6174
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6174 (same declaration text).
def OAI.EditApproximation.BinaryFraction.groupMemberSourceWithWork line 6182
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6182 (same declaration text).
def OAI.EditApproximation.BinaryFraction.wideActionsFromRepresentativesWithWork line 6191
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6191 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialConeReadWithWork line 6199
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6199 (same declaration text).
def OAI.EditApproximation.BinaryFraction.wideMinimumReadAllocation line 6206
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6206 (same declaration text).
def OAI.EditApproximation.BinaryFraction.groupMemberSourceAllocation line 6216
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6216 (same declaration text).
def OAI.EditApproximation.BinaryFraction.wideActionsFromRepresentativesAllocation line 6225
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6225 (same declaration text).
def OAI.EditApproximation.BinaryFraction.representativeFromActionsReadWithWork line 6235
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6235 (same declaration text).
def OAI.EditApproximation.BinaryFraction.physicalContinuationReadWithWork line 6249
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6249 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialMinimumReadWithWork line 6261
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6261 (same declaration text).
def OAI.EditApproximation.BinaryFraction.localWarmupReadKernelWithWork line 6275
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6275 (same declaration text).
def OAI.EditApproximation.BinaryFraction.representativeFromActionsReadAllocation line 6286
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6286 (same declaration text).
def OAI.EditApproximation.BinaryFraction.physicalContinuationReadAllocation line 6300
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6300 (same declaration text).
def OAI.EditApproximation.BinaryFraction.localWarmupReadAllocation line 6311
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6311 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedRepresentativeReadWithWork line 6322
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6322 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialProgramReadWithWork line 6330
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6330 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedRepresentativeReadAllocation line 6336
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6336 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryRefinementFinishAllocation line 6344
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6344 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryOnlineRangeWithWork line 6358
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6358 (same declaration text).
def OAI.EditApproximation.BinaryFraction.cachedInitialProgramReadWithWork line 6370
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6370 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryOnlineRangeAllocation line 6375
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6375 (same declaration text).
def OAI.EditApproximation.PositionCounts.count line 6398
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6398 (same declaration text).
def OAI.EditApproximation.PositionCounts.left line 6402
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6402 (same declaration text).
def OAI.EditApproximation.PositionCounts.right line 6406
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6406 (same declaration text).
def OAI.EditApproximation.PositionCounts.storageBits line 6410
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6410 (same declaration text).
def OAI.EditApproximation.PositionCounts.add line 6414
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6414 (same declaration text).
def OAI.EditApproximation.PositionCounts.addWithWork line 6421
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6421 (same declaration text).
def OAI.EditApproximation.PositionCounts.prefixWithWork line 6431
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6431 (same declaration text).
def OAI.EditApproximation.BitQuery.Footprint.bind line 6450
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6450 (same declaration text).
def OAI.EditApproximation.BitQuery.Footprint.compute line 6458
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6458 (same declaration text).
def OAI.EditApproximation.BitQuery.Footprint.chargeOf line 6462
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6462 (same declaration text).
def OAI.EditApproximation.BitQuery.Footprint.runCells line 6466
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6466 (same declaration text).
def OAI.EditApproximation.BitQuery.Footprint.computeOf line 6476
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6476 (same declaration text).
def OAI.EditApproximation.BitQuery.Footprint.collect line 6480
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6480 (same declaration text).
def OAI.EditApproximation.BitQuery.Footprint.mapKeysWithWork line 6490
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6490 (same declaration text).
def OAI.EditApproximation.BitQuery.Footprint.restrictWithWork line 6499
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6499 (same declaration text).
def OAI.EditApproximation.BitQuery.Footprint.normalize line 6514
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6514 (same declaration text).
def OAI.EditApproximation.bandActionPredicate line 6529
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6529 (same declaration text).
def OAI.EditApproximation.queryOnlineSourceGather line 6541
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6541 (same declaration text).
def OAI.EditApproximation.coarseLabelChildren line 6553
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6553 (same declaration text).
instance OAI.EditApproximation.bandActionPredicateDecidable line 6561
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6561 (same declaration text).
def OAI.EditApproximation.computedBandActions line 6569
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6569 (same declaration text).
def OAI.EditApproximation.rationalEndpointActionValue line 6587
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6587 (same declaration text).
def OAI.EditApproximation.rationalActualWideActions line 6591
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6591 (same declaration text).
def OAI.EditApproximation.groupQueriedChildLabels line 6597
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6597 (same declaration text).
def OAI.EditApproximation.rationalWideActionMinimum line 6601
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6601 (same declaration text).
def OAI.EditApproximation.groupCurrentInputCover line 6607
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6607 (same declaration text).
def OAI.EditApproximation.representativeBandActions line 6613
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6613 (same declaration text).
structure OAI.EditApproximation.UnskippedBand line 6624
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6624 (same declaration text).
def OAI.EditApproximation.keyedOnlineBandG line 6643
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6643 (same declaration text).
def OAI.EditApproximation.testUnskippedBand line 6649
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6649 (same declaration text).
def OAI.EditApproximation.unskippedBandList line 6668
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6668 (same declaration text).
def OAI.EditApproximation.keyedOnlineCandidate line 6675
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6675 (same declaration text).
def OAI.EditApproximation.cellUnskippedBands line 6720
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6720 (same declaration text).
def OAI.EditApproximation.localOnlineCandidates line 6728
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6728 (same declaration text).
def OAI.EditApproximation.BinaryMemo.value line 6751
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6751 (same declaration text).
def OAI.EditApproximation.BinaryMemo.left line 6755
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6755 (same declaration text).
def OAI.EditApproximation.BinaryMemo.right line 6759
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6759 (same declaration text).
def OAI.EditApproximation.BinaryMemo.lookup line 6763
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6763 (same declaration text).
def OAI.EditApproximation.BinaryMemo.insert line 6768
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6768 (same declaration text).
def OAI.EditApproximation.BinaryMemo.lookupCosted line 6773
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6773 (same declaration text).
def OAI.EditApproximation.BinaryMemo.insertCosted line 6782
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6782 (same declaration text).
def OAI.EditApproximation.rankedMemoEvaluate line 6800
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6800 (same declaration text).
def OAI.EditApproximation.localWarmupStepQuery line 6815
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6815 (same declaration text).
def OAI.EditApproximation.keyedOnlineSourceRange line 6829
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6829 (same declaration text).
def OAI.EditApproximation.occurrenceBuild line 6834
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6834 (same declaration text).
def OAI.EditApproximation.occurrenceBuildWithWork line 6842
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6842 (same declaration text).
def OAI.EditApproximation.occurrenceQueryWithWork line 6853
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6853 (same declaration text).
def OAI.EditApproximation.rankedBitMemoEvaluate line 6862
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6862 (same declaration text).
def OAI.EditApproximation.physicalWarmupStepQuery line 6878
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6878 (same declaration text).
def OAI.EditApproximation.indexedSingletonCostWithWork line 6886
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6886 (same declaration text).
def OAI.EditApproximation.integerOccurrenceIndex line 6892
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6892 (same declaration text).
def OAI.EditApproximation.integerOccurrenceBuildWithWork line 6896
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6896 (same declaration text).
def OAI.EditApproximation.rankedMemoAddressWork line 6900
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6900 (same declaration text).
def OAI.EditApproximation.rankedMemoKernelWork line 6912
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6912 (same declaration text).
def OAI.EditApproximation.physicalWarmupRequestQuery line 6924
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6924 (same declaration text).
abbrev OAI.EditApproximation.PhysicalLocalOnlineKey line 6952
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6952 (same declaration text).
abbrev OAI.EditApproximation.ClampedPhysicalSeed line 6955
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6955 (same declaration text).
def OAI.EditApproximation.finalTargetState line 6957
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6957 (same declaration text).
abbrev OAI.EditApproximation.PhysicalCommonKey line 6959
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6959 (same declaration text).
def OAI.EditApproximation.clampedSeedNat line 6963
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6963 (same declaration text).
def OAI.EditApproximation.triangularChoiceWithWork line 6976
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:6976 (same declaration text).
def OAI.EditApproximation.triangularChoiceAllocation line 7219
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7219 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coordinateVectorWithWork line 7473
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7473 (same declaration text).
def OAI.EditApproximation.BinaryFraction.reduceOnlineIntegerWithWork line 7570
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7570 (same declaration text).
def OAI.EditApproximation.BinaryFraction.countedPreparedActionReadWithWork line 7822
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7822 (same declaration text).
def OAI.EditApproximation.BinaryFraction.countedPreparedActionKernelAllocation line 7833
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7833 (same declaration text).
def OAI.EditApproximation.BinaryFraction.countedBandActionReadWithWork line 7845
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7845 (same declaration text).
def OAI.EditApproximation.BinaryFraction.countedPreparedActionAllocation line 7854
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7854 (same declaration text).
def OAI.EditApproximation.BinaryFraction.countedSampledOnlineReadWithWork line 7860
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7860 (same declaration text).
def OAI.EditApproximation.BinaryFraction.countedBandActionAllocation line 7871
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7871 (same declaration text).
def OAI.EditApproximation.BinaryFraction.countedSampledOnlineAllocation line 7881
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7881 (same declaration text).
def OAI.EditApproximation.SourceRanked.rank line 7901
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7901 (same declaration text).
def OAI.EditApproximation.SourceRanked.keyCode line 7905
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7905 (same declaration text).
def OAI.EditApproximation.SourceRanked.child line 7909
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7909 (same declaration text).
def OAI.EditApproximation.SourceRanked.body line 7915
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7915 (same declaration text).
def OAI.EditApproximation.SourceRanked.bitBody line 7923
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7923 (same declaration text).
def OAI.EditApproximation.ChargedPhysicalRequest.depth line 7940
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7940 (same declaration text).
def OAI.EditApproximation.ChargedPhysicalRequest.index line 7944
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7944 (same declaration text).
def OAI.EditApproximation.ChargedPhysicalRequest.rank line 7948
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7948 (same declaration text).
def OAI.EditApproximation.chargedPreviousRead line 7961
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:7961 (same declaration text).
def OAI.EditApproximation.chargedWarmupChild line 8003
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8003 (same declaration text).
def OAI.EditApproximation.chargedSeedQuery line 8051
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8051 (same declaration text).
def OAI.EditApproximation.chargedWarmupQuery line 8072
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8072 (same declaration text).
abbrev OAI.EditApproximation.coarseEntryWidth line 8100
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8100 (same declaration text).
abbrev OAI.EditApproximation.CoarseGuessIndex line 8102
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8102 (same declaration text).
def OAI.EditApproximation.coarseGuess line 8104
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8104 (same declaration text).
def OAI.EditApproximation.coarseEntryTree line 8106
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8106 (same declaration text).
def OAI.EditApproximation.coarseInitialMeasure line 8109
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8109 (same declaration text).
def OAI.EditApproximation.coarseActiveChildrenWork line 8123
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8123 (same declaration text).
abbrev OAI.EditApproximation.CoarseFullSeedDraws line 8132
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8132 (same declaration text).
def OAI.EditApproximation.coarseFullSeedMeasure line 8135
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8135 (same declaration text).
def OAI.EditApproximation.rejectionAcceptedLaw line 8151
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8151 (same declaration text).
abbrev OAI.EditApproximation.RejectionRuntimeArray line 8154
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8154 (same declaration text).
def OAI.EditApproximation.BinaryMemo.fractionStorage line 8165
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8165 (same declaration text).
def OAI.EditApproximation.BinaryMemo.valueStorage line 8171
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8171 (same declaration text).
def OAI.EditApproximation.indexedLeafWithWork line 8184
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8184 (same declaration text).
def OAI.EditApproximation.integerOccurrenceStorage line 8190
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8190 (same declaration text).
def OAI.EditApproximation.integerStoredDataSpace line 8193
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8193 (same declaration text).
def OAI.EditApproximation.binaryIndexedLeafWithWork line 8207
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8207 (same declaration text).
def OAI.EditApproximation.binaryIndexedLeafAllocation line 8212
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8212 (same declaration text).
def OAI.EditApproximation.queryIndexedSliceWithWork line 8217
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8217 (same declaration text).
def OAI.EditApproximation.queryIndexedSliceAllocation line 8224
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8224 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialGridReadAllocation line 8239
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8239 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialConeReadAllocation line 8247
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8247 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialCentersReadAllocation line 8250
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8250 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialMinimumReadAllocation line 8259
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8259 (same declaration text).
def OAI.EditApproximation.BinaryFraction.initialProgramReadAllocation line 8273
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8273 (same declaration text).
def OAI.EditApproximation.BinaryFraction.cachedInitialProgramReadAllocation line 8277
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8277 (same declaration text).
def OAI.EditApproximation.BinaryFraction.onlineParametersAllocation line 8290
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8290 (same declaration text).
def OAI.EditApproximation.BinaryFraction.refinementDecrementAllocation line 8293
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8293 (same declaration text).
def OAI.EditApproximation.scheduledRefinementAllocation line 8304
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8304 (same declaration text).
def OAI.EditApproximation.refinementBaseAllocation line 8310
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8310 (same declaration text).
def OAI.EditApproximation.refinementParameterAllocation line 8316
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8316 (same declaration text).
def OAI.EditApproximation.computedQueryPassAllocation line 8320
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8320 (same declaration text).
def OAI.EditApproximation.computedQuerySetupAllocation line 8324
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8324 (same declaration text).
def OAI.EditApproximation.UnreducedRational.nat line 8337
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8337 (same declaration text).
def OAI.EditApproximation.BinaryFraction.countedGroupMemberSourceWithWork line 8349
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8349 (same declaration text).
def OAI.EditApproximation.BinaryFraction.roundedBandReadWithWork line 8724
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:8724 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupLabelsWithWork line 9081
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:9081 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupLabelsAllocation line 9451
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:9451 (same declaration text).
def OAI.EditApproximation.BinaryFraction.countedGroupMemberSourceAllocation line 9821
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:9821 (same declaration text).
def OAI.EditApproximation.BinaryFraction.unskippedGuardReadWithWork line 10206
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10206 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupInputsWithWork line 10225
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10225 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseIndexedRootWithWork line 10236
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10236 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupInputsAllocation line 10318
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10318 (same declaration text).
def OAI.EditApproximation.BinaryFraction.unskippedGuardReadAllocation line 10331
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10331 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupInputsTransportWithWork line 10346
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10346 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseIndexedCandidateWithWork line 10353
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10353 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedUnskippedReadAllocation line 10363
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10363 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupInputsTransportAllocation line 10377
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10377 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedUnskippedReadWithWorkRaw line 10385
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10385 (same declaration text).
def OAI.EditApproximation.BinaryFraction.coarseIndexedInitialWithWork line 10399
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10399 (same declaration text).
def OAI.EditApproximation.BinaryFraction.unskippedEstimateSourceWithWorkRaw line 10428
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10428 (same declaration text).
def OAI.EditApproximation.BinaryFraction.unskippedEstimateSourceAllocationRaw line 10436
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10436 (same declaration text).
def OAI.EditApproximation.BinaryFraction.chooseUnskippedSourceWithWorkRaw line 10446
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10446 (same declaration text).
def OAI.EditApproximation.BinaryFraction.chooseUnskippedSourceAllocationRaw line 10450
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10450 (same declaration text).
def OAI.EditApproximation.BinaryFraction.sampledGroupActionSourceWithWorkRaw line 10456
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10456 (same declaration text).
def OAI.EditApproximation.BinaryFraction.sampledGroupActionSourceAllocationRaw line 10463
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10463 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedOnlineReadWithWorkRaw line 10482
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10482 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedOnlineReadAllocationRaw line 10631
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10631 (same declaration text).
inductive OAI.EditDistortion.Step line 10791
Also declared: ComparatorChallenges/EditDistance.lean:10 (same declaration text), OAI/Combinatorics/EditApproximation/Definitions.lean:10791 (same declaration text).
inductive OAI.EditDistortion.Script line 10797
Distinct definitions of this name: ComparatorChallenges/EditDistance.lean:17 (different declaration text), OAI/Combinatorics/EditApproximation/Definitions.lean:10797 (same declaration text). Qualify references as OAI.EditDistortion.Script@path.
def OAI.EditDistortion.edit line 10802
Also declared: ComparatorChallenges/EditDistance.lean:23 (same declaration text), OAI/Combinatorics/EditApproximation/Definitions.lean:10802 (same declaration text).
def OAI.EditDistortion.cost line 10814
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10814 (same declaration text).
def OAI.EditApproximation.CoarseSourceTree.word line 10825
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10825 (same declaration text).
def OAI.EditApproximation.coarseLabelCount line 10838
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10838 (same declaration text).
def OAI.EditApproximation.coarseIndexedEntryBinaryCost line 10848
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10848 (same declaration text).
def OAI.EditApproximation.coarseInitialLabelCount line 10854
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10854 (same declaration text).
def OAI.EditApproximation.coarseChildrenCost line 10871
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10871 (same declaration text).
def OAI.EditApproximation.coarseShiftCost line 10879
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10879 (same declaration text).
instance OAI.EditApproximation.targetIntervalFintype line 10898
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10898 (same declaration text).
def OAI.EditApproximation.UnskippedBand.actions line 10917
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10917 (same declaration text).
def OAI.EditApproximation.UnskippedBand.envelope line 10924
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10924 (same declaration text).
def OAI.EditApproximation.UnskippedBand.rounded line 10930
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10930 (same declaration text).
def OAI.EditApproximation.UnskippedBand.rationalAction line 10937
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10937 (same declaration text).
def OAI.EditApproximation.unskippedGroupEstimate line 10954
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10954 (same declaration text).
def OAI.EditApproximation.groupDyadicScaleAt line 10971
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10971 (same declaration text).
abbrev OAI.EditApproximation.CellGroupDraws line 10983
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10983 (same declaration text).
abbrev OAI.EditApproximation.cellScaleReadDraw line 10987
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10987 (same declaration text).
abbrev OAI.EditApproximation.GroupScalarKey line 10991
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10991 (same declaration text).
abbrev OAI.EditApproximation.CountedCellGroupDraws line 10995
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10995 (same declaration text).
abbrev OAI.EditApproximation.CellGroupSourceAllocations line 10999
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:10999 (same declaration text).
abbrev OAI.EditApproximation.CountedCellGroupAllocations line 11003
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:11003 (same declaration text).
abbrev OAI.EditApproximation.CellGroupReadDraws line 11007
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:11007 (same declaration text).
def OAI.EditApproximation.groupScalarKeys line 11010
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:11010 (same declaration text).
def OAI.EditApproximation.groupDrawFromValues line 11017
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:11017 (same declaration text).
def OAI.EditApproximation.queryGroupKeyEqualWithWork line 11022
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:11022 (same declaration text).
def OAI.EditApproximation.queryGroupKeyEqualAllocation line 11031
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:11031 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupKeySamplesWithWork line 11046
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:11046 (same declaration text).
def OAI.EditApproximation.BinaryFraction.querySharedCellInputsWithWork line 11479
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:11479 (same declaration text).
def OAI.EditApproximation.BinaryFraction.groupKeySampleBlock line 11583
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:11583 (same declaration text).
def OAI.EditApproximation.BinaryFraction.groupKeySampleBlockAllocation line 11960
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:11960 (same declaration text).
def OAI.EditApproximation.BinaryFraction.querySharedCellInputsAllocation line 12336
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12336 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupKeySamplesAllocation line 12446
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12446 (same declaration text).
def OAI.EditApproximation.BinaryFraction.querySharedInputsWithWork line 12543
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12543 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupDrawReadWithWork line 12558
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12558 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupSourceKeysWithWork line 12741
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12741 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupDrawReadAllocation line 12754
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12754 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupSourceKeysAllocation line 12764
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12764 (same declaration text).
def OAI.EditApproximation.BinaryFraction.querySharedInputsAllocation line 12781
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12781 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedCellGroupSourceAllocationRaw line 12805
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12805 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedCellGroupSourceWithWorkRaw line 12843
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12843 (same declaration text).
def OAI.EditApproximation.querySharedInputCover line 12880
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12880 (same declaration text).
def OAI.EditApproximation.coarseThresholdChildrenCost line 12889
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12889 (same declaration text).
def OAI.EditApproximation.coarseThresholdEstimate line 12902
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12902 (same declaration text).
abbrev OAI.EditApproximation.PhysicalScalarIndex line 12923
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12923 (same declaration text).
def OAI.EditApproximation.computedPhysicalCoarseDepth line 12932
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12932 (same declaration text).
abbrev OAI.EditApproximation.PhysicalScalarKey line 12938
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12938 (same declaration text).
instance OAI.EditApproximation.physicalScalarIndexFintype line 12941
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12941 (same declaration text).
def OAI.EditApproximation.physicalScalarRange line 12946
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12946 (same declaration text).
instance OAI.EditApproximation.physicalScalarRangeNeZero line 12952
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12952 (same declaration text).
def OAI.EditApproximation.queryGroupSourceGather line 12967
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12967 (same declaration text).
def OAI.EditApproximation.physicalScalarCodeWithWork line 12977
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12977 (same declaration text).
def OAI.EditApproximation.physicalScalarCodeAllocation line 12996
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:12996 (same declaration text).
abbrev OAI.EditApproximation.PhysicalGroupQueries line 13011
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13011 (same declaration text).
def OAI.EditApproximation.physicalScalarOnlineRead line 13016
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13016 (same declaration text).
def OAI.EditApproximation.physicalScalarGroupQueriesAt line 13025
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13025 (same declaration text).
abbrev OAI.EditApproximation.BitPhysicalGroupQueries line 13038
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13038 (same declaration text).
def OAI.EditApproximation.queryPhysicalScalarRead line 13043
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13043 (same declaration text).
def OAI.EditApproximation.queryPhysicalScalarGroupQueriesAt line 13047
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13047 (same declaration text).
def OAI.EditApproximation.dyadicUnskippedGroupEstimate line 13062
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13062 (same declaration text).
def OAI.EditApproximation.chooseUnskippedGroup line 13070
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13070 (same declaration text).
def OAI.EditApproximation.chooseCellGroupAction line 13088
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13088 (same declaration text).
def OAI.EditApproximation.localCellGroupActions line 13108
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13108 (same declaration text).
def OAI.EditApproximation.localRefinementStepQuery line 13124
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13124 (same declaration text).
def OAI.EditApproximation.localOnlineSourceStepQuery line 13181
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13181 (same declaration text).
def OAI.EditApproximation.queryRefinementGather line 13206
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13206 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryRefinementFinishWithWork line 13228
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13228 (same declaration text).
def OAI.EditApproximation.localRandomSourceStepQuery line 13246
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13246 (same declaration text).
def OAI.EditApproximation.localRandomBandDataQuery line 13261
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13261 (same declaration text).
def OAI.EditApproximation.localRandomDataQuery line 13278
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13278 (same declaration text).
def OAI.EditApproximation.physicalScalarCode line 13294
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13294 (same declaration text).
def OAI.EditApproximation.physicalScalarGroupQueries line 13312
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13312 (same declaration text).
def OAI.EditApproximation.physicalScalarGroupRead line 13337
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13337 (same declaration text).
def OAI.EditApproximation.physicalRandomDataRequestQuery line 13350
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13350 (same declaration text).
def OAI.EditApproximation.physicalInactiveGlobalQuery line 13380
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13380 (same declaration text).
def OAI.EditApproximation.physicalRandomGlobalQuery line 13400
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13400 (same declaration text).
def OAI.EditApproximation.PhysicalTableRequest.entryCapacity line 13433
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13433 (same declaration text).
def OAI.EditApproximation.PhysicalTableRequest.code line 13435
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13435 (same declaration text).
def OAI.EditApproximation.SourceRanked.supportedChild line 13448
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13448 (same declaration text).
def OAI.EditApproximation.SourceRanked.supportedChildMap line 13452
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13452 (same declaration text).
def OAI.EditApproximation.SourceRanked.restrictBody line 13459
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13459 (same declaration text).
def OAI.EditApproximation.physicalRandomBoundedQuery line 13477
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13477 (same declaration text).
def OAI.EditApproximation.chargedRandomGlobalQuery line 13486
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13486 (same declaration text).
abbrev OAI.EditApproximation.PhysicalFamilyScalarKey line 13525
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13525 (same declaration text).
abbrev OAI.EditApproximation.PhysicalFamilyScalarDraw line 13528
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13528 (same declaration text).
def OAI.EditApproximation.physicalFamilyAnswer line 13543
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13543 (same declaration text).
def OAI.EditApproximation.physicalFamilyGroupRead line 13547
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13547 (same declaration text).
def OAI.EditApproximation.physicalFamilyOnlineRead line 13553
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13553 (same declaration text).
abbrev OAI.EditApproximation.QueryFamilyMemoKey line 13569
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13569 (same declaration text).
def OAI.EditApproximation.queryFamilySourceWordWithWork line 13573
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13573 (same declaration text).
def OAI.EditApproximation.queryFamilyMemoRemaining line 13578
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13578 (same declaration text).
abbrev OAI.EditApproximation.ComputedFamilySeed line 13591
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13591 (same declaration text).
abbrev OAI.EditApproximation.ComputedFamilyDraw line 13595
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13595 (same declaration text).
abbrev OAI.EditApproximation.ComputedFamilyInput line 13601
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13601 (same declaration text).
def OAI.EditApproximation.physicalFamilyCode line 13615
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13615 (same declaration text).
def OAI.EditApproximation.ChargedPhysicalRequest.code line 13627
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13627 (same declaration text).
abbrev OAI.EditApproximation.ComputedFamilyScalarKey line 13640
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13640 (same declaration text).
def OAI.EditApproximation.computedFamilyMemoCode line 13646
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13646 (same declaration text).
def OAI.EditApproximation.coarseInitialCandidate line 13662
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13662 (same declaration text).
def OAI.EditApproximation.coarseInitialMinimum line 13670
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13670 (same declaration text).
def OAI.EditApproximation.coarseInitialValue line 13675
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13675 (same declaration text).
def OAI.EditApproximation.coarseActiveArrayWork line 13691
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13691 (same declaration text).
def OAI.EditApproximation.coarseFullSeedTable line 13702
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13702 (same declaration text).
def OAI.EditApproximation.coarseInitialArrayWork line 13707
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13707 (same declaration text).
def OAI.EditApproximation.integerEqualWithWork line 13725
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13725 (same declaration text).
def OAI.EditApproximation.integerPreprocessingWork line 13735
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13735 (same declaration text).
abbrev OAI.EditApproximation.ComputedFamilyMemoKey line 13749
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13749 (same declaration text).
def OAI.EditApproximation.integerPreevaluationWork line 13753
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13753 (same declaration text).
def OAI.EditApproximation.physicalFamilyCodeWithWork line 13766
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13766 (same declaration text).
def OAI.EditApproximation.computedFamilyMemoCodeWithWork line 13783
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13783 (same declaration text).
def OAI.EditApproximation.queryPhysicalScalarGroupQueries line 13804
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13804 (same declaration text).
def OAI.EditApproximation.queryPhysicalScalarGroupRead line 13983
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:13983 (same declaration text).
def OAI.EditApproximation.queryPhysicalScalarOnlineRead line 14000
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14000 (same declaration text).
def OAI.EditApproximation.queryFamilyTagWithWork line 14137
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14137 (same declaration text).
def OAI.EditApproximation.queryFamilyGroupRead line 14146
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14146 (same declaration text).
def OAI.EditApproximation.queryFamilyOnlineRead line 14155
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14155 (same declaration text).
abbrev OAI.EditApproximation.QueryPhysicalChild line 14173
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14173 (same declaration text).
def OAI.EditApproximation.querySupportedChildWithWork line 14176
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14176 (same declaration text).
def OAI.EditApproximation.queryRestrictPhysicalBody line 14181
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14181 (same declaration text).
def OAI.EditApproximation.queryInitialConeProgramAt line 14291
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14291 (same declaration text).
def OAI.EditApproximation.queryChargedRead line 14309
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14309 (same declaration text).
def OAI.EditApproximation.queryChargedPreviousRead line 14316
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14316 (same declaration text).
def OAI.EditApproximation.queryChargedSeedAt line 14366
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14366 (same declaration text).
def OAI.EditApproximation.queryPhysicalInitial line 14436
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14436 (same declaration text).
def OAI.EditApproximation.queryWarmupProgram line 14458
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14458 (same declaration text).
def OAI.EditApproximation.queryChargedWarmupChild line 14477
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14477 (same declaration text).
def OAI.EditApproximation.queryChargedWarmup line 14532
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14532 (same declaration text).
abbrev OAI.EditApproximation.ChargedFamilyQueryKey line 14616
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14616 (same declaration text).
def OAI.EditApproximation.rankedNormalizeBody line 14629
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14629 (same declaration text).
def OAI.EditApproximation.chargedRandomMemoEvaluate line 14643
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14643 (same declaration text).
def OAI.EditApproximation.physicalFamilyProgram line 14661
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14661 (same declaration text).
abbrev OAI.EditApproximation.PhysicalCoarseDraw line 14678
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14678 (same declaration text).
def OAI.EditApproximation.physicalCoarseSeedTable line 14694
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14694 (same declaration text).
def OAI.EditApproximation.localFinalRootRequest line 14773
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14773 (same declaration text).
def OAI.EditApproximation.computedFamilyKernelWork line 14788
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14788 (same declaration text).
def OAI.EditApproximation.computedFamilyAddressWork line 14807
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14807 (same declaration text).
def OAI.EditApproximation.computedFamilyCoarseCopyStorage line 14826
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14826 (same declaration text).
def OAI.EditApproximation.computedFamilyCoarseArrayCapacity line 14832
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14832 (same declaration text).
def OAI.EditApproximation.computedFamilyCoarseScratchCapacity line 14836
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14836 (same declaration text).
def OAI.EditApproximation.computedFamilyCoarseControlCapacity line 14840
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14840 (same declaration text).
def OAI.EditApproximation.physicalFamilyMemoResult line 14867
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14867 (same declaration text).
def OAI.EditApproximation.selectionIndicator line 14887
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14887 (same declaration text).
def OAI.EditApproximation.coarseIndexedEntryCostSum line 14898
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14898 (same declaration text).
def OAI.EditApproximation.querySupportedChildAllocation line 14907
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14907 (same declaration text).
def OAI.EditApproximation.rejectionFailureLaw line 14925
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14925 (same declaration text).
def OAI.EditApproximation.rejectionRuntimeArrayLaw line 14957
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14957 (same declaration text).
def OAI.EditApproximation.rejectionSelectedBits line 14960
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14960 (same declaration text).
abbrev OAI.EditApproximation.physicalFamilyRange line 14975
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14975 (same declaration text).
instance OAI.EditApproximation.physicalFamilyRange_neZero line 14979
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14979 (same declaration text).
abbrev OAI.EditApproximation.ComputedPhysicalCoarseDraw line 14994
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14994 (same declaration text).
abbrev OAI.EditApproximation.ComputedRejectionRuntime line 14998
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:14998 (same declaration text).
def OAI.EditApproximation.computedPhysicalCoarseLaw line 15004
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15004 (same declaration text).
abbrev OAI.EditApproximation.ComputedExecutionOutcome line 15010
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15010 (same declaration text).
def OAI.EditApproximation.computedExecutionLaw line 15013
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15013 (same declaration text).
abbrev OAI.EditApproximation.ComputedFullOutcome line 15021
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15021 (same declaration text).
abbrev OAI.EditApproximation.PhysicalFamilyRuntimeOutcome line 15042
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15042 (same declaration text).
def OAI.EditApproximation.physicalFamilyRuntimeAccepted line 15044
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15044 (same declaration text).
def OAI.EditApproximation.physicalLargeInput line 15057
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15057 (same declaration text).
instance OAI.EditApproximation.physicalLargeInput_decidable line 15063
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15063 (same declaration text).
def OAI.EditApproximation.physicalFamilyMemoBits line 15085
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15085 (same declaration text).
def OAI.EditApproximation.computedFamilyResult line 15101
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15101 (same declaration text).
def OAI.EditApproximation.computedFamilyRejectionWork line 15108
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15108 (same declaration text).
def OAI.EditApproximation.physicalFamilyMemoCoarseWork line 15138
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15138 (same declaration text).
abbrev OAI.EditApproximation.PhysicalCoarseExecution line 15158
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15158 (same declaration text).
def OAI.EditApproximation.physicalCoarseExecutionProjection line 15163
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15163 (same declaration text).
def OAI.EditApproximation.computedExecutionProjection line 15177
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15177 (same declaration text).
def OAI.EditApproximation.computedFullLaw line 15183
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15183 (same declaration text).
def OAI.EditApproximation.computedExecutionAccepted line 15197
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15197 (same declaration text).
def OAI.EditApproximation.computedExecutionRejectionWork line 15202
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15202 (same declaration text).
def OAI.EditApproximation.computedFinalRoot line 15206
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15206 (same declaration text).
def OAI.EditApproximation.computedExecutionKernelWork line 15212
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15212 (same declaration text).
def OAI.EditApproximation.computedExecutionDictionaryWork line 15227
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15227 (same declaration text).
def OAI.EditApproximation.computedExecutionAddressWork line 15231
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15231 (same declaration text).
def OAI.EditApproximation.symbolicComputedCoarseWork line 15249
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15249 (same declaration text).
def OAI.EditApproximation.symbolicComputedExecutionCoarseWork line 15259
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15259 (same declaration text).
def OAI.EditApproximation.computedExecutionCoarseWork line 15273
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15273 (same declaration text).
def OAI.EditApproximation.computedExecutionNonlocalWork line 15288
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15288 (same declaration text).
def OAI.EditApproximation.physicalFamilyIndexedCoarseWork line 15315
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15315 (same declaration text).
def OAI.EditApproximation.symbolicComputedExecutionIndexedCoarseWork line 15338
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15338 (same declaration text).
def OAI.EditApproximation.computedExecutionIndexedCoarseWork line 15359
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15359 (same declaration text).
def OAI.EditApproximation.physicalFamilyCoarseSamplingWork line 15385
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15385 (same declaration text).
def OAI.EditApproximation.symbolicComputedExecutionCoarseSamplingWork line 15409
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15409 (same declaration text).
def OAI.EditApproximation.computedExecutionCoarseSamplingWork line 15430
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15430 (same declaration text).
def OAI.EditApproximation.physicalFamilyCoarsePreparationWork line 15456
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15456 (same declaration text).
def OAI.EditApproximation.computedFamilyCoarsePreparationWork line 15473
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15473 (same declaration text).
def OAI.EditApproximation.computedExecutionCoarsePreparationWork line 15484
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15484 (same declaration text).
def OAI.EditApproximation.computedExecutionReadChargedWork line 15488
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15488 (same declaration text).
def OAI.EditApproximation.computedExecutionTotalWork line 15504
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15504 (same declaration text).
def OAI.EditApproximation.computedFullOutputWork line 15510
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15510 (same declaration text).
def OAI.EditApproximation.queryFamilyTagAllocation line 15528
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15528 (same declaration text).
def OAI.EditApproximation.BitQuery.Footprint.rankedBitMemoCells line 15542
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15542 (same declaration text).
def OAI.EditApproximation.queryInitialGatherFootprint line 15578
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15578 (same declaration text).
def OAI.EditApproximation.queryBandGatherFootprint line 15607
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15607 (same declaration text).
def OAI.EditApproximation.queryGroupSourceGatherFootprint line 15641
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15641 (same declaration text).
def OAI.EditApproximation.queryOnlineSourceGatherFootprint line 15669
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15669 (same declaration text).
def OAI.EditApproximation.queryPhysicalTableReadFootprint line 15713
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15713 (same declaration text).
def OAI.EditApproximation.queryMeanReadFootprint line 15724
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15724 (same declaration text).
def OAI.EditApproximation.queryPhysicalScalarReadFootprint line 15741
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15741 (same declaration text).
def OAI.EditApproximation.queryRestrictPhysicalBodyFootprint line 15748
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15748 (same declaration text).
def OAI.EditApproximation.queryInitialConeProgramAtFootprint line 15850
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15850 (same declaration text).
def OAI.EditApproximation.queryChargedReadFootprint line 15890
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15890 (same declaration text).
def OAI.EditApproximation.queryWarmupProgramFootprint line 15900
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:15900 (same declaration text).
def OAI.EditApproximation.queryPhysicalEarlierReadFootprint line 16004
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:16004 (same declaration text).
def OAI.EditApproximation.queryPhysicalScalarOnlineReadFootprint line 16088
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:16088 (same declaration text).
def OAI.EditApproximation.queryChargedSeedAtFootprint line 16216
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:16216 (same declaration text).
def OAI.EditApproximation.queryFamilyOnlineReadFootprint line 16321
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:16321 (same declaration text).
def OAI.EditApproximation.queryPhysicalInitialFootprint line 16337
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:16337 (same declaration text).
def OAI.EditApproximation.queryPhysicalScalarGroupQueriesFootprint line 16370
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:16370 (same declaration text).
def OAI.EditApproximation.queryPhysicalScalarGroupReadFootprint line 16557
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:16557 (same declaration text).
def OAI.EditApproximation.queryFamilyGroupReadFootprint line 16568
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:16568 (same declaration text).
def OAI.EditApproximation.queryChargedWarmupFootprint line 16593
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:16593 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedComputedCellSourceWithWorkRawBand line 16716
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:16716 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleSourceWithWorkRawBand line 16803
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:16803 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsSourceWithWorkRawBand line 16855
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:16855 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedLocalOnlineScaleSourceWithWorkRawBand line 16879
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:16879 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedLocalOnlineActionsSourceWithWorkRawBand line 17093
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17093 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryOnlineSelectWithWorkRawBand line 17112
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17112 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupSelectWithWorkRawBand line 17119
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17119 (same declaration text).
def OAI.EditApproximation.queryLocalRefinementRawBand line 17134
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17134 (same declaration text).
def OAI.EditApproximation.queryLocalRandomSourcesRawBand line 17154
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17154 (same declaration text).
def OAI.EditApproximation.queryLocalBandRawBand line 17175
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17175 (same declaration text).
def OAI.EditApproximation.queryLocalProgramRawBand line 17255
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17255 (same declaration text).
def OAI.EditApproximation.queryPhysicalRandomDataRequestRawBand line 17270
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17270 (same declaration text).
def OAI.EditApproximation.queryFamilyRefinementRawBand line 17300
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17300 (same declaration text).
def OAI.EditApproximation.queryFamilyActiveRawBand line 17319
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17319 (same declaration text).
def OAI.EditApproximation.queryFamilyBoundedActiveRawBand line 17353
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17353 (same declaration text).
def OAI.EditApproximation.queryChargedFamilyTableRawBand line 17371
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17371 (same declaration text).
def OAI.EditApproximation.queryChargedFamilyGlobalRawBand line 17455
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17455 (same declaration text).
def OAI.EditApproximation.queryFamilyMemoRawRawBand line 17474
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17474 (same declaration text).
def OAI.EditApproximation.computedQueryMemoRawRawBand line 17490
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17490 (same declaration text).
def OAI.EditApproximation.computedQueryMemoNormalizedRawBand line 17515
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17515 (same declaration text).
def OAI.EditApproximation.computedQueryMemoResultRawBand line 17604
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17604 (same declaration text).
def OAI.EditApproximation.computedQueryLocalWorkRawBand line 17613
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17613 (same declaration text).
def OAI.EditApproximation.computedQueryAnswerWithWorkRawBand line 17619
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17619 (same declaration text).
def OAI.EditApproximation.integerQueryLocalWorkRawBand line 17636
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17636 (same declaration text).
def OAI.EditApproximation.integerBinaryOutputRawBand line 17649
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17649 (same declaration text).
def OAI.EditApproximation.integerBinaryAnswerRawBand line 17663
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17663 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedComputedCellSourceAllocationRawBand line 17682
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17682 (same declaration text).
def OAI.EditApproximation.BinaryFraction.castGroupSourceAllocationRawBand line 17779
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17779 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleSourceAllocationRawBand line 17824
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17824 (same declaration text).
def OAI.EditApproximation.BinaryFraction.localGroupSourceScaleBlockRawBand line 17878
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17878 (same declaration text).
def OAI.EditApproximation.BinaryFraction.localGroupSourceScaleBlockAllocationRawBand line 17887
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17887 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsSourceAllocationRawBand line 17895
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17895 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedLocalOnlineScaleSourceAllocationRawBand line 17914
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:17914 (same declaration text).
def OAI.EditApproximation.BinaryFraction.preparedLocalOnlineActionsSourceAllocationRawBand line 18125
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18125 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryOnlineSelectAllocationRawBand line 18144
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18144 (same declaration text).
def OAI.EditApproximation.BinaryFraction.queryGroupSelectAllocationRawBand line 18154
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18154 (same declaration text).
def OAI.EditApproximation.integerBinaryWorkRawBand line 18172
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18172 (same declaration text).
def OAI.EditApproximation.integerFinalAllocationRawBand line 18187
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18187 (same declaration text).
def OAI.EditApproximation.queryLocalRefinementFootprintRawBand line 18205
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18205 (same declaration text).
def OAI.EditApproximation.queryLocalRandomSourcesFootprintRawBand line 18446
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18446 (same declaration text).
def OAI.EditApproximation.queryLocalBandFootprintRawBand line 18524
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18524 (same declaration text).
def OAI.EditApproximation.queryLocalProgramFootprintRawBand line 18644
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18644 (same declaration text).
def OAI.EditApproximation.queryPhysicalRandomDataRequestFootprintRawBand line 18690
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18690 (same declaration text).
def OAI.EditApproximation.queryFamilyRefinementFootprintRawBand line 18755
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18755 (same declaration text).
def OAI.EditApproximation.queryFamilyActiveFootprintRawBand line 18781
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18781 (same declaration text).
def OAI.EditApproximation.queryFamilyBoundedActiveFootprintRawBand line 18808
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18808 (same declaration text).
def OAI.EditApproximation.queryChargedFamilyTableFootprintRawBand line 18829
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18829 (same declaration text).
def OAI.EditApproximation.queryChargedFamilyGlobalFootprintRawBand line 18916
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18916 (same declaration text).
def OAI.EditApproximation.queryFamilyMemoRawFootprintRawBand line 18940
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18940 (same declaration text).
def OAI.EditApproximation.computedQueryMemoRawFootprintRawBand line 18979
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:18979 (same declaration text).
def OAI.EditApproximation.computedQueryMemoFootprintRawBand line 19010
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:19010 (same declaration text).
def OAI.EditApproximation.computedQueryTemporaryCellsFootprintRawBand line 19102
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:19102 (same declaration text).
def OAI.EditApproximation.integerAcceptedSpaceTermsFootprintRawBand line 19113
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:19113 (same declaration text).
def OAI.EditApproximation.integerBinarySpaceFootprintRawBand line 19133
Also declared: OAI/Combinatorics/EditApproximation/Definitions.lean:19133 (same declaration text).
theorem OAI.EditApproximation.almostLinearEditDistanceRawBand Challenge statement: Almost-linear approximation of edit distance sorry line 19146
L4DEL explanation
The formalization gives a randomized $(1+\varepsilon)$-approximation for unit-cost edit distance between explicitly stored integer strings, for every fixed rational $0<\varepsilon<1$. Its estimate is at least the true distance and at most $(1+\varepsilon)$ times it with probability at least $2/3$; equal strings return zero on every execution. For total length at most $N$ and integer symbols bounded by a fixed polynomial in $N$, expected work is at most $(N+2)^{1+\eta}$ for every fixed $\eta>0$ and all sufficiently large $N$. Space is polynomially bounded on every execution.
1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
2. The repository's comparator configuration selects OAI.Combinatorics.EditApproximation.Specification.RawBandMain as the released solution module checked against this declaration.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Specification/RawBandMain.lean:8 (different declaration text). Qualify references as OAI.EditApproximation.almostLinearEditDistanceRawBand@path.
```
theorem almostLinearEditDistanceRawBand (epsilon : OAI.EditApproximation.BinaryFraction)
    (hepsilon : 0 < epsilon.value) (_hepsilonOne : epsilon.value < 1)
    :
    (∀ (source target : List ℤ) (N : ℕ), source.length + target.length ≤ N →
      (2 / 3 : ℝ) ≤ (OAI.EditApproximation.computedFullLaw (source.map OAI.EditApproximation.integerSymbolCode) (target.map OAI.EditApproximation.integerSymbolCode) N epsilon).real
        {outcome | EditDistortion.edit source target ≤ OAI.EditApproximation.integerBinaryAnswerRawBand source target N epsilon outcome ∧
          (OAI.EditApproximation.integerBinaryAnswerRawBand source target N epsilon outcome : ℝ) ≤
            (1 + (epsilon.value : ℝ)) * OAI.EditDistortion.edit source target}) ∧
    (∀ (source target : List ℤ) (N : ℕ), source = target → ∀ outcome,
      OAI.EditApproximation.integerBinaryAnswerRawBand source target N epsilon outcome = 0) ∧
    (∀ (C : ℕ) (eta : ℝ), 0 < eta → ∀ᶠ N : ℕ in atTop,
      ∀ source target : List ℤ, source.length + target.length ≤ N →
…
```
Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.computedFullLaw, OAI.EditApproximation.integerSymbolCode, OAI.EditDistortion.edit, OAI.EditApproximation.integerBinaryAnswerRawBand