OAI/Combinatorics/EditApproximation/Geometry/WideEarlierInputs.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Wide enumeration gathers child states before scoring its Cartesian action list. Its recursive input count depends on the coordinate lists, rather than the exponentially larger number of complete actions.

  1. theorem OAI.EditApproximation.wideEarlierChildStateList_length_le line 15
  2. theorem OAI.EditApproximation.wideEarlierInputCover_card line 28
  3. theorem OAI.EditApproximation.wideEarlierInputCover_mem line 59
  4. theorem OAI.EditApproximation.bandCoordinates_earlier_cover line 70
  5. theorem OAI.EditApproximation.localRefinementRepresentatives_length line 85