OAI/Analysis/CircleDomains/Selection/BlockCodeInvariants.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Domain-endpoint and disk-origin invariants for normalization of mixed paid chains into grouped jump codes.

  1. def OAI.CircleDomainRigidity.BlockPathsInDomain line 20
  2. def OAI.CircleDomainRigidity.BlockDisksFrom line 24
  3. theorem OAI.CircleDomainRigidity.jumpBlockCode_initial_eq line 27
  4. theorem OAI.CircleDomainRigidity.jumpBlockCode_terminal_eq line 35
  5. theorem OAI.CircleDomainRigidity.singlePieceBlock_inDomain line 45
  6. theorem OAI.CircleDomainRigidity.singlePieceBlock_disksFrom line 50
  7. theorem OAI.CircleDomainRigidity.replaceInitialTruePiece_inDomain line 54
  8. theorem OAI.CircleDomainRigidity.replaceInitialTruePiece_disksFrom line 64
  9. theorem OAI.CircleDomainRigidity.prependNewBlockJump_inDomain line 69
  10. theorem OAI.CircleDomainRigidity.prependNewBlockJump_disksFrom line 79
  11. theorem OAI.CircleDomainRigidity.prependOldBlockJump_inDomain line 89
  12. theorem OAI.CircleDomainRigidity.prependOldBlockJump_disksFrom line 97