OAI/Analysis/CircleDomains/Topology/SubarcGates.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The original endpoint law's prescribed closed gates survive measurable subarc selection and compact conditioning. In particular the localized arc starts satisfy the very same collar gate used by the positive-law construction.

  1. theorem OAI.CircleDomainRigidity.GateRule.of_range_subset line 18
  2. theorem OAI.CircleDomainRigidity.IsSubarcLawReduction.gates line 27
  3. theorem OAI.CircleDomainRigidity.codePathLaw_gates line 43
  4. theorem OAI.CircleDomainRigidity.IsSubarcLawReduction.code_gates line 54
  5. theorem OAI.CircleDomainRigidity.IsSubarcLawReduction.terminal_start_gate line 65