Reference · Signed rationals

rainbow.math.rational.signed.deviation-rows

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

The two-row encoding of a magnitude bound says exactly what it looks like. A contract model says "the deviation must stay within t". A linear model cannot write a magnitude, so it writes two rows, d <= t and -d <= t, and the question a verified reformulation has to answer is whether that pair is the same constraint. Unlike the indicator row, this one admits a full EQUIVALENCE rather than a pair of one-way guarantees: optimization/deviation-rows-sound d <= t -> -d <= t -> max(d, -d) <= t the two rows are enough: nothing outside the magnitude bound survives them; optimization/deviation-rows-complete max(d, -d) <= t -> (d <= t) AND (-d <= t) the two rows are not too many: everything the magnitude bound allowed still satisfies both. Together they say the encoding is neither too tight nor too loose, which is the strongest form of reformulation guarantee and the one a buyer should ask for before trusting a model they did not write. `signed/max` and its bound laws come from the signed lattice; this module only adds the `optimization/` statements that connect them to the modelling question. `signed/negate-reverses-order` is proved here because the order cone is where it belongs: negating both sides of a comparison swaps the two Grothendieck cross sums, so it is additive commutativity transported through the nnrat order. Native and axiom-free on D63.

Depends onmath.rational.nnrat.add-monotonemath.rational.signed.order-transitivitymath.rational.signed.minmax

signed/negate-reverses-order :
  (a b : ℚ)
  (ordered : a ≤ b)
  → signed/negate b ≤ signed/negate a

optimization/deviation-rows-sound :
  (d t : ℚ)
  (above : d ≤ t)
  (below : signed/negate d ≤ t)
  → signed/max d (signed/negate d) ≤ t

optimization/deviation-rows-complete :
  (d t : ℚ)
  (bounded : signed/max d (signed/negate d) ≤ t)
  → proposition/conjunction (d ≤ t) (signed/negate d ≤ t)