OAI/Combinatorics/MatrixRemoval/CanonicalCopyBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Unconditional copy bound for the canonical host

Concrete anchor rigidity and six-mode body localization imply the integer copy bound and its normalized form.

  1. theorem OAI.Problem348.OrderedHost.anchor64Pinned line 17
  2. theorem OAI.Problem348.OrderedHost.matching_copy_leaf line 21
  3. theorem OAI.Problem348.OrderedHost.canonical_copyCount_le line 28
  4. theorem OAI.Problem348.OrderedHost.canonical_copyDensity_le line 33