OAI/Analysis/CircleDomains/Topology/GraphBoundaryBranches.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The graph avoidance supplied by the subordinate contour construction implies exactly the inactive lattice avoidance of its local real lifts. This applies equally to real coordinates and genuine period coordinates.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.graph_branch_avoids_lattice_on_real_boundary line 17
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_masked_graph_boundary_active line 37
  3. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.physical_mem_graph line 67