Reference · Algorithm guarantees

rainbow.algorithms.proofs.interior-point

Algorithm guaranteessrc/rainbow/algorithms/proofs/interior_point.clj1 definitions, 3 theorems

AHoF O50 Interior Point / Barrier Method: the transform that keeps iterates strictly feasible by adding a barrier term that grows as a constraint slack approaches zero: barrier-objective = objective + mu * (1 / slack) where `slack` is the (positive) distance to a constraint boundary and `mu` is the barrier parameter, shrunk toward zero across outer iterations. The textbook log barrier -mu*sum(log slack) is not exact-rational, so this uses the rational inverse barrier mu/slack (both keep iterates interior and diverge at the boundary); the log form stays an executable concern. What is proved is the barrier-objective recurrence and worked instances via exact division. 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.interior-point` prints this classification.

barrier/objective :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

barrier/objective-unfold :
  (objective mu slack : ℚ≥0)
  → barrier/objective objective mu slack = objective + nnrat/divide mu slack

barrier/unit-slack-example :
  → barrier/objective 1 2 1 = 3

barrier/wide-slack-example :
  → barrier/objective 1 2 2 = 2