Reference · Algorithm guarantees

rainbow.algorithms.proofs.golden-section-search

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

Golden Section Search interval reduction over exact rationals (AHoF O9). A unimodal minimum is bracketed in [a, b]; two interior probe points c < d are evaluated, and the sub-interval on the side of the SMALLER interior value is kept, shrinking the bracket each iteration. The reduction decision compares the two interior values, and the retained interior value is their minimum: keep-left? fc fd = decide (fc <= fd) (keep [a, d] when fc <= fd) retained-min fc fd = if (fc <= fd) then fc else fd (min via if-data / nnrat) over exact rationals. Golden Section and Fibonacci Search share this skeleton; only the probe-point placement differs. Proved native and axiom-free: the reduction decision and the retained-minimum selection, each with an unfold theorem. Requires audit/decide-nnrat-at-most, logic/if-data (both 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.golden-section-search` prints this classification.

linesearch/keep-left? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

linesearch/retained-min :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

linesearch/keep-left-unfold :
  (fc fd : ℚ≥0)
  → failmon/safe? fc fd = audit/decide-nnrat-at-most fc fd

linesearch/retained-min-unfold :
  (fc fd : ℚ≥0)
  → linesearch/retained-min fc fd = logic/if-data ℚ≥0 (audit/decide-nnrat-at-most fc fd = audit/decide-nnrat-at-most fc fd) (audit/decide-nnrat-at-most fc fd) fc fd