OAI/Analysis/CircleDomains/Selection/ZeroRealCoordinate.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A zero coordinate occupies unused selection slots. Its new-level failure event is contained in the single zero circle level, hence has zero measure.

  1. def OAI.CircleDomainRigidity.PhysicalRealCoordinate.zero line 19
  2. theorem OAI.CircleDomainRigidity.circleBandGraph_zero_subset line 36
  3. theorem OAI.CircleDomainRigidity.zero_coordinate_compatibility line 48
  4. def OAI.CircleDomainRigidity.UngatedRealTest.zeroTest line 57