OAI/Analysis/CircleDomains/Rigidity/CodeFreeTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The residual constraints stored in a base code combine with the open-tag trace theorem to exclude free incidences along the entire path.

  1. theorem OAI.CircleDomainRigidity.ae_code_free_level_incidence_null line 20