OAI/Analysis/CircleDomains/Rigidity/RankedCodeTraces.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Generic prior-level intersections for a code whose natural labels carry an independent inherited order. Physical coarea and local trace estimates are unchanged; only the finite-tuple comparison uses the rank.

  1. theorem OAI.CircleDomainRigidity.ranked_ae_code_level_singleton_on_tags line 18
  2. theorem OAI.CircleDomainRigidity.ranked_ae_code_local_band_tag_trace_null line 40
  3. theorem OAI.CircleDomainRigidity.ranked_ae_code_branch_free_level_incidence_null line 104
  4. theorem OAI.CircleDomainRigidity.ranked_ae_code_period_free_level_incidence_null line 174
  5. theorem OAI.CircleDomainRigidity.ranked_code_period_generic_levels line 276