OAI/Combinatorics/EditApproximation/Queries/QuerySharedGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Boolean endpoint enumeration for the whole-cell shared-read cover. The inner interval is centered at each computed left endpoint plus the child length, exactly as in the published query's gap guard.

  1. theorem OAI.EditApproximation.queryGapStatesWithWork_value line 16
  2. theorem OAI.EditApproximation.BinaryFraction.queryGroupRoundedStatesWithWork_value line 28