TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Codebook.Catalog.Proof

Denotation theorems for named tiny codebooks #

These lemmas expose the exact meaning of each catalog word without adding runtime code.

source
@[simp]
theorem FloatLib.Floats.Formats.Codebook.Catalog.bipolar1_denote_zero :
bipolar1.denote 0#1 = Numerics.NumericalValue.finite (-1)

The zero bit pattern of bipolar1 denotes negative one.

source
@[simp]
theorem FloatLib.Floats.Formats.Codebook.Catalog.bipolar1_denote_one :
bipolar1.denote 1#1 = Numerics.NumericalValue.finite 1

The one bit pattern of bipolar1 denotes positive one.

source
@[simp]
theorem FloatLib.Floats.Formats.Codebook.Catalog.ternary2_denote_zero :
ternary2.denote 0#2 = Numerics.NumericalValue.finite 0

The 00 ternary code denotes zero.

source
@[simp]
theorem FloatLib.Floats.Formats.Codebook.Catalog.ternary2_denote_positive :
ternary2.denote 1#2 = Numerics.NumericalValue.finite 1

The 01 ternary code denotes positive one.

source
@[simp]
theorem FloatLib.Floats.Formats.Codebook.Catalog.ternary2_denote_negative :
ternary2.denote 2#2 = Numerics.NumericalValue.finite (-1)

The 10 ternary code denotes negative one.

source
@[simp]
theorem FloatLib.Floats.Formats.Codebook.Catalog.ternary2_denote_reserved :
ternary2.denote 3#2 = Numerics.NumericalValue.exceptional (Numerics.ExceptionalValue.reserved (some 3))

The 11 ternary code is the reserved exceptional word.