OAI/Analysis/CircleDomains/Probability/CodeLocalBandTagNull.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The local branch payment theorem for the actual code law. The global level's singleton contacts follow from stored tag tuples and ordered compatibility, including when the coordinate has nonzero period.

  1. theorem OAI.CircleDomainRigidity.ae_code_level_singleton_on_tags line 22
  2. theorem OAI.CircleDomainRigidity.ae_code_local_band_tag_trace_null line 43