Float32Model

the exact signed sum of two FINITE values: same signs add the magnitudes, different signs subtract the smaller from the larger and take its sign (equal magnitudes give N = 0, which modelRoundBits makes the signed zero: +0 by the sign chosen below). Until 2026-09-22 the larger-first case took sign 0, so -3.0 + 1.0 gave +2.0 while 1.0 + -3.0 gave -2.0; the known-answer table had no such row. Found by the checked learning step's fused multiply-add, which shares the rule. Exact opposite-sign cancellation must choose +0 even when the first operand is negative. Preserving that operand's sign made -2+2 disagree with native round-to-nearest arithmetic; the singleton normalized- exponential pullback exposed it. Same-sign negative zeros stay negative.

137def modelSumSigned =
138  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
139    (modelSelectSigned (specEqual (modelSign a) (modelSign b))
140      (constructor ModelSigned ModelSignedOf (modelSign a) (nat-add (modelScaledMagnitude a) (modelScaledMagnitude b)))
141      (modelSelectSigned (nat-less-than (modelScaledMagnitude a) (modelScaledMagnitude b))
142        (constructor ModelSigned ModelSignedOf (modelSign b) (nat-subtract (modelScaledMagnitude b) (modelScaledMagnitude a)))
143        (constructor ModelSigned ModelSignedOf
144          (specSelect (nat-less-than (modelScaledMagnitude b) (modelScaledMagnitude a)) (modelSign a) 0)
145          (nat-subtract (modelScaledMagnitude a) (modelScaledMagnitude b)))))))