OAI/Analysis/CircleDomains/Selection/RealBandPaidValues.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

On a common branch range shorter than one, the paid circle threshold is exactly the real threshold. Domain hits contribute a coordinate value; flagged hits contribute a member of the actual real band.

  1. theorem OAI.CircleDomainRigidity.real_band_paid_values line 16