Reference · Signed rationals

rainbow.math.rational.signed.upper-bound-program

Signed rationalssrc/rainbow/math/rational/signed/upper_bound_program.clj0 definitions, 3 theorems

A worked constrained program, certified end-to-end by the general duality theorem -- the non-vacuity witness for the signed Lagrangian stack. For an ARBITRARY signed bound c, take the one-constraint program minimize f y = -y (equivalently: maximize y) subject to g y = y - c <= 0 (equivalently: y <= c) and relax it with the single multiplier lambda = 1. The Lagrangian collapses to a constant: L y = -y + 1*(y - c) ~ -c so the dual value -c bounds L everywhere, which is exactly the `bound` hypothesis of `optimization/signed-constrained-weak-duality`. The remaining hypotheses are the new unit laws: 0 <= 1 gives multiplier nonnegativity, c - c <= 0 gives feasibility of the candidate x0 = c, and the zero gap is reflexivity because f c is literally -c. Feeding all of that to `optimization/signed-constrained-zero-gap-optimal` yields, for every c and every x in the feasible set, optimization/signed-upper-bound-program-optimal : x - c <= 0 -> -c <= -x i.e. c maximizes the objective subject to x <= c. The conclusion is elementary on its own; the point is that it is DERIVED, for a whole parameterized family, through the abstract weak-duality / zero-gap machinery rather than proved directly -- so that machinery is inhabited, not vacuous. The one piece of real work is the Lagrangian collapse: over Grothendieck pairs it is the nnrat reassociation `Nc + (Py + (Ny + Pc)) ~ (Ny + (Py + Nc)) + Pc`, both sides being the same four-element multiset -- one `rainbow.math.rational.nnrat.ring` call. Native and axiom-free; chains the concrete constrained-duality module, the signed unit laws, the KKT congruence and the nnrat-ring tactic on D63.

Depends onmath.rational.signed.constrained-dualitymath.rational.signed.kkt-sufficiencymath.rational.signed.unit-lawsmath.rational.nnrat.ring

optimization/signed-upper-bound-lagrangian-collapse :
  (c y : ℚ)
  → signed/negate c = signed/negate y + (y - c)

optimization/signed-upper-bound-dual-bound :
  (c y : ℚ)
  → signed/negate c ≤ signed/negate y + (1 · (y - c) + 0)

optimization/signed-upper-bound-program-optimal :
  (c x : ℚ)
  (member : x - c ≤ 0)
  → signed/negate c ≤ signed/negate x