OAI/Analysis/CircleDomains/Modulus/MixedChainNormalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Normalize an arbitrary mixed paid chain into grouped old-jump blocks. Consecutive true pieces are joined; a jump receives a zero-cost constant true piece when needed. Total cost and all new disk labels are preserved.

  1. theorem OAI.CircleDomainRigidity.exists_grouped_code_of_paid_chain line 21