OAI/Combinatorics/UniformKServer/AnchorScalar.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The signed scalar accounting inequalities for the reference, park and hidden-key substeps of the retained-anchor potential.

  1. theorem OAI.UniformKServer.AnchorScalar.reference line 16
  2. theorem OAI.UniformKServer.AnchorScalar.parks line 37
  3. def OAI.UniformKServer.AnchorScalar.value line 46
  4. theorem OAI.UniformKServer.AnchorScalar.value_nonneg line 51
  5. theorem OAI.UniformKServer.AnchorScalar.value_bound line 57
  6. def OAI.UniformKServer.AnchorScalar.near line 64
  7. theorem OAI.UniformKServer.AnchorScalar.near_nonneg line 69
  8. theorem OAI.UniformKServer.AnchorScalar.member line 75