OAI/Combinatorics/EditApproximation/Binary/BinaryCountedGroup.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Group evaluation reads the exact finite sampler indexed by the count computed from the stored rational scale. Casting indices below is proof transport only; the emitted natural count is used by the executed loop.

  1. def OAI.EditApproximation.BinaryFraction.countedGroupMemberWithWork line 13
  2. theorem OAI.EditApproximation.BinaryFraction.groupMemberWithWork_transport line 25
  3. theorem OAI.EditApproximation.BinaryFraction.countedGroupMemberWithWork_value line 35
  4. theorem OAI.EditApproximation.BinaryFraction.countedGroupMemberWithWork_cost line 46