Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.mean-value-inclusion

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/mean_value_inclusion.clj1 definitions, 3 theorems

AHoF V42 Mean-Value Inclusion: a tighter interval extension than the natural inclusion, using the mean-value form to enclose a function's range in [lo, hi]; a value is certified within the enclosure when it lies between the bounds: encloses? lo hi value = (lo <= value) AND (value <= hi) (boolean AND via logic/if-data over the two order decisions). Proved native and axiom-free (membership + unfold, enclosed value, value below lower bound). Requires audit/decide-nnrat-at-most, logic/if-data (both in the D63 checkpoint). Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 1 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.ahof.mean-value-inclusion` prints this classification.

mean-value/encloses? :
  (x₁ x₂ x₃ : ℚ≥0)
  → data/Bool

mean-value/encloses-unfold :
  (lo hi value : ℚ≥0)
  → mean-value/encloses? lo hi value = logic/if-data data/Bool (audit/decide-nnrat-at-most lo value = audit/decide-nnrat-at-most lo value) (audit/decide-nnrat-at-most lo value) (audit/decide-nnrat-at-most value hi) data/false

mean-value/value-enclosed :
  → mean-value/encloses? 1/2 3/2 1 = data/true

mean-value/value-below-not-enclosed :
  → mean-value/encloses? 1/2 3/2 1/4 = data/false