OAI/Analysis/CircleDomains/Selection/CodeResidualAvoidance.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The stored rational-interval constraints give null residual-incidence envelopes under the actual square bounds on visits.

  1. def OAI.CircleDomainRigidity.rationalStart line 18
  2. def OAI.CircleDomainRigidity.rationalEnd line 19
  3. theorem OAI.CircleDomainRigidity.rationalStart_eq line 21
  4. theorem OAI.CircleDomainRigidity.rationalEnd_eq line 25
  5. theorem OAI.CircleDomainRigidity.baseCode_prior_bound line 29
  6. theorem OAI.CircleDomainRigidity.baseCode_level_bound line 35
  7. theorem OAI.CircleDomainRigidity.ae_code_boundaryToll_finite line 43
  8. theorem OAI.CircleDomainRigidity.ae_code_prior_envelope_null line 54
  9. theorem OAI.CircleDomainRigidity.ae_code_level_envelope_null line 70