Reference · Algorithm guarantees

rainbow.algorithms.proofs.order-statistic

Algorithm guaranteessrc/rainbow/algorithms/proofs/order_statistic.clj1 definitions, 4 theorems

AHoF empirical rank / order statistic: the count of sample values that fall at or below a threshold, count-at-most t xs = |{ x in xs : x <= t }|, the unnormalized empirical CDF at t that underlies quantile estimation, rank statistics, and Monte-Carlo hit counting. It is a fold over the sample list that increments a natural counter exactly when the decidable rational comparison x <= t holds: count-at-most t [] = 0 count-at-most t (x :: rest) = if (x <= t) then succ (count rest) else count rest. Exact naturals and the decidable rational order, so the count is proved data. The threshold sweep that turns counts into a full empirical CDF or quantile is an executable concern; what is proved here is the counting fold, its cons recurrence, and worked counts. Requires nat, decidable nnrat order (audit/decide-nnrat-at-most), logic/if-data, and data/List.rec (all carried by the D63 checkpoint). Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 2 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.order-statistic` prints this classification.

order-statistic/count-at-most :
  (x₁ : ℚ≥0) (x₂ : List ℚ≥0)
  → ℕ

order-statistic/cons-below-increments :
  (xs : List ℚ≥0)
  → order-statistic/count-at-most 5 (data/cons ℚ≥0 3 xs) = data/succ (order-statistic/count-at-most 5 xs)

order-statistic/cons-above-preserves :
  (xs : List ℚ≥0)
  → order-statistic/count-at-most 5 (data/cons ℚ≥0 7 xs) = order-statistic/count-at-most 5 xs

order-statistic/count-example :
  → order-statistic/count-at-most 5 [3, 7, 2] = 2

order-statistic/count-empty :
  → order-statistic/count-at-most 5 [] = 0