Correctness of catalog-codebook arithmetic

For the one-bit bipolar and two-bit ternary catalog tables, negation and multiplication agree with the corresponding integer operations on finite inputs. The proofs enumerate these tables' stored words. The ternary refinement statements assume finite operands; separate rejection theorems cover multiplication with a reserved operand.

theorem FloatLib.Floats.Formats.Codebook.Catalog.bipolar1.neg_refines : Numerics.Operation.Finite1 bipolar1.numericalSystem bipolar1.numericalSystem neg fun (x : ℤ) => -x

Bipolar negation exactly refines integer negation.

theorem FloatLib.Floats.Formats.Codebook.Catalog.bipolar1.mul_refines : Numerics.Operation.Finite2 bipolar1.numericalSystem bipolar1.numericalSystem bipolar1.numericalSystem mul fun (x y : ℤ) => x * y

Bipolar multiplication exactly refines integer multiplication.

@[simp]

theorem FloatLib.Floats.Formats.Codebook.Catalog.ternary2.mul_reserved_left (x : ternary2.Code) : mul? (3#2) x = none

A reserved left operand is rejected, including when the right operand is zero.

@[simp]

theorem FloatLib.Floats.Formats.Codebook.Catalog.ternary2.mul_reserved_right (x : ternary2.Code) : mul? x 3#2 = none

A reserved right operand is rejected, including when the left operand is zero.

theorem FloatLib.Floats.Formats.Codebook.Catalog.ternary2.neg_refines : Numerics.Operation.Checked1 ternary2.numericalSystem ternary2.numericalSystem neg? fun (x : ℤ) => Numerics.NumericalValue.finite (-x)

Checked ternary negation exactly refines integer negation on finite inputs.

theorem FloatLib.Floats.Formats.Codebook.Catalog.ternary2.mul_refines : Numerics.Operation.Checked2 ternary2.numericalSystem ternary2.numericalSystem ternary2.numericalSystem mul? fun (x y : ℤ) => Numerics.NumericalValue.finite (x * y)

Checked ternary multiplication exactly refines integer multiplication on finite inputs.