Reference · Algorithm guarantees

rainbow.algorithms.proofs.interval-membership

Algorithm guaranteessrc/rainbow/algorithms/proofs/interval_membership.clj2 definitions, 2 theorems

Interval membership over exact rationals (AHoF V40, decision layer). A value x lies in the closed interval [lo, hi] exactly when lo <= x AND x <= hi: interval-contains? lo hi x = if (decide lo<=x) then (decide x<=hi) else false (boolean AND via logic/if-data over Bool). The endpoint operation for interval addition [a,b]+[c,d] = [a+c, b+d] is exact-rational addition of the corresponding endpoints: interval-add-endpoint p q = p + q. This is the membership/decision companion to `rainbow.algorithms.proofs.interval-arithmetic` (which proves the interval constructor and the additive enclosure over signed rationals); here membership composes the exact-rational order decision with the boolean AND, and endpoint addition composes exact-rational addition -- the two reusable pieces the worked V40 milestone instance specializes, each with an unfold theorem. Proved native and axiom-free. Requires audit/decide-nnrat-at-most, logic/if-data, nnrat/add (all present in the D63 checkpoint). Scope (measured by the kernel): this module has 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.interval-membership` prints this classification.

validation/interval-contains? :
  (x₁ x₂ x₃ : ℚ≥0)
  → data/Bool

validation/interval-add-endpoint :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

validation/interval-contains-unfold :
  (lo hi x : ℚ≥0)
  → validation/interval-contains? lo hi x = logic/if-data data/Bool (audit/decide-nnrat-at-most lo x = audit/decide-nnrat-at-most lo x) (audit/decide-nnrat-at-most lo x) (audit/decide-nnrat-at-most x hi) data/false

validation/interval-add-endpoint-unfold :
  (p q : ℚ≥0)
  → estimation/total-weight p q = p + q