CraftCosts.lean

import Std

/- An integer accounting identity. The definitions are assumptions about a
   chosen horizon and common cost unit, not laws of organizational behaviour. -/
namespace CraftCosts

def separate (n d : Int) : Int := n * d

def shared (n a f q w l : Int) : Int := f + n * a + q + w + l

theorem sharing_threshold (n d a f q w l : Int) :
    shared n a f q w l < separate n d ↔
    f + q + w + l < n * (d - a) := by
  unfold shared separate
  rw [Int.mul_sub]
  omega

theorem cost_tie (n d a f q w l : Int) :
    shared n a f q w l = separate n d ↔
    f + q + w + l = n * (d - a) := by
  unfold shared separate
  rw [Int.mul_sub]
  omega

theorem overhead_reverses_saving (n d a f q w l : Int)
    (h : n * (d - a) < f + q + w + l) :
    separate n d < shared n a f q w l := by
  unfold separate shared
  rw [Int.mul_sub] at h
  omega

-- Constructed witnesses prove neither architecture universally minimizes cost.
theorem shared_saving_example : shared 4 10 30 5 5 0 < separate 4 50 := by decide
theorem waiting_reversal_example : separate 4 50 < shared 4 10 30 5 200 0 := by decide

#print axioms sharing_threshold
#print axioms cost_tie
#print axioms overhead_reverses_saving
end CraftCosts