OAI/Analysis/CircleDomains/Topology/RecursiveCompactReduction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The recursive positive law gives an actual compactly supported terminal-arc law at sufficiently deep collars. Its physical density and punctured hit norm are arbitrarily small, and the original prescribed gates survive the reduction.

  1. structure OAI.CircleDomainRigidity.CompactRecursiveReduction line 19
  2. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.eventually_compact_reduction line 40
  3. theorem OAI.CircleDomainRigidity.CompactRecursiveReduction.start_gate line 90