OAI/Analysis/CircleDomains/Probability/CodeRealBandTagNull.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The real-coordinate tag conclusion for the actual base-code law. The independent-level condition comes from the stored tag tuples; the countable chart cover and all local payment measures are constructed.

  1. theorem OAI.CircleDomainRigidity.ae_code_real_level_singleton_on_tags line 25
  2. theorem OAI.CircleDomainRigidity.ae_code_real_band_tag_trace_null line 56