Reference · Algorithm guarantees

rainbow.algorithms.proofs.triangular

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

AHoF triangular numbers T(n) = 0 + 1 + ... + n -- the arithmetic-series sum that counts pairwise interactions and quantifies the cost of quadratic algorithms (all-pairs comparisons, insertion-sort work, full pivoting). Defined by recursion on n, adding the current index at each step: T 0 = 0 T (succ n) = (succ n) + T n. Exact naturals. Proved native and axiom-free: the step recurrence (Nat.rec computation rule) and worked values (T 0 = 0, T 4 = 10, T 5 = 15). The Gauss closed form n(n+1)/2 is exercised in the executable; what is proved here is the additive recurrence and worked sums. Requires nat and nat addition (algebra/nat-add), carried by the D63 checkpoint. Scope (measured by the kernel): this module has 3 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.triangular` prints this classification.

triangular/number :
  (x₁ : ℕ)
  → ℕ

triangular/step-unfold :
  (n : ℕ)
  → triangular/number (data/succ n) = algebra/nat-add (data/succ n) (triangular/number n)

triangular/number-zero :
  → triangular/number 0 = 0

triangular/number-four :
  → triangular/number 4 = 10

triangular/number-five :
  → triangular/number 5 = 15