Reference · Algorithm guarantees

rainbow.algorithms.proofs.net-flow

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

AHoF net flow / net present value: the signed balance of inflows against outflows, net inflow outflow = inflow - outflow, the exact-rational primitive behind net-reward MDPs, cash-flow / NPV accounting, and constraint residuals. Signed subtraction stores the balance as a Grothendieck pair (positive, negative) that is not canonical, so worked net values are proved on the signed cross-product equivalence signed/equivalent (discharged by reflexivity on the reduced nat cross-product), and a surplus (inflow >= outflow) is certified nonnegative via the decidable rational order. Discounting a cash-flow stream is an executable concern; what is proved here is the net computation, worked balances, and the surplus-nonnegativity guarantee. Requires signed/subtract, signed/equivalent, signed/nonnegative, nnrat/at-most, and the decidable nnrat order (all 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.net-flow` prints this classification.

net-flow/net :
  (x₁ x₂ : ℚ)
  → ℚ

net-flow/net-unfold :
  (inflow outflow : ℚ)
  → net-flow/net inflow outflow = inflow - outflow

net-flow/net-surplus-example :
  → net-flow/net (signed/from-nnrat 5) (signed/from-nnrat 3) = signed/from-nnrat 2

net-flow/net-larger-surplus-example :
  → net-flow/net (signed/from-nnrat 7) (signed/from-nnrat 2) = signed/from-nnrat 5

net-flow/net-surplus-nonnegative :
  → signed/nonnegative (net-flow/net (signed/from-nnrat 5) (signed/from-nnrat 3))