OAI/Analysis/CircleDomains/Selection/JumpBlockCodes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Concrete finite chains grouped into true-path blocks separated by old jumps. The finite code records old disk labels and new-jump counts.

  1. abbrev OAI.CircleDomainRigidity.BoundedBlockPattern line 17
  2. def OAI.CircleDomainRigidity.blockAnchors line 20
  3. theorem OAI.CircleDomainRigidity.blockAnchors_zero line 24
  4. theorem OAI.CircleDomainRigidity.blockAnchors_last line 28
  5. theorem OAI.CircleDomainRigidity.blockAnchors_internal line 33
  6. theorem OAI.CircleDomainRigidity.blockAnchors_frontier line 38
  7. structure OAI.CircleDomainRigidity.JumpBlockCode line 51
  8. structure OAI.CircleDomainRigidity.IsJumpBlockCode line 55
  9. def OAI.CircleDomainRigidity.jumpBlockCost line 66