Encoded numerical systems

NumericalSystem is the family-independent interface of FloatLib. It says only what code type is stored, what mathematical scalar domain finite codes denote, and how every code is interpreted. It does not assume a radix, exponent field, NaN convention, or rounding rule.

This small interface is broad enough for binary and decimal floats, fixed point, posits, logarithmic number systems, block-scaled values, and exact integers. Concrete arithmetic and its proofs remain in the corresponding implementation modules.

structure FloatLib.Numerics.NumericalSystem : Type (max (u + 1) (v + 1))

A representation together with its complete mathematical interpretation.

• Code : Type u

  Stored or executable values of the system.

• Scalar : Type v

  Exact mathematical domain used to interpret ordinary codes.

• denote : self.Code → NumericalValue self.Scalar

  Meaning of every code, including infinities and exceptional words.

@[reducible]

def FloatLib.Numerics.NumericalSystem.ofFinite {Code : Type u} {Scalar : Type v} (decode : Code → Scalar) : NumericalSystem

Build a numerical system whose every code has an ordinary finite interpretation.

This is the common representation shape for exact integers, fixed-point values, logarithmic codes, and other formats without infinities or exceptional words.

@[reducible]

def FloatLib.Numerics.NumericalSystem.exact (α : Type u) : NumericalSystem

A scalar type viewed as an exact numerical system with no exceptional codes.

Reducibility lets Lean reuse structures such as orders and rings on α through the projected Code and Scalar types without introducing forwarding instances.

def FloatLib.Numerics.NumericalSystem.Represents (S : NumericalSystem) (code : S.Code) (x : S.Scalar) : Prop

code represents the ordinary scalar x.

@[simp]

theorem FloatLib.Numerics.NumericalSystem.ofFinite_represents_iff {Code : Type u} {Scalar : Type v} (decode : Code → Scalar) (code : Code) (value : Scalar) : (ofFinite decode).Represents code value ↔ decode code = value

In an ofFinite system, representation is equality after decoding.

theorem FloatLib.Numerics.NumericalSystem.exact_represents_iff {α : Type u} (code value : α) : (exact α).Represents code value ↔ code = value

Exact-system representation is ordinary equality.

def FloatLib.Numerics.NumericalSystem.Representable (S : NumericalSystem) (x : S.Scalar) : Prop

An exact scalar is representable when some code denotes it.

def FloatLib.Numerics.NumericalSystem.Equivalent (S : NumericalSystem) (x y : S.Code) : Prop

Two codes are semantically equivalent, even if their bit patterns differ.

def FloatLib.Numerics.NumericalSystem.IsFinite (S : NumericalSystem) (code : S.Code) : Prop

A code has an ordinary finite meaning.

def FloatLib.Numerics.NumericalSystem.mapScalar {β : Type w} (S : NumericalSystem) (f : S.Scalar → β) : NumericalSystem

Change only the mathematical codomain of a numerical system.

@[simp]

theorem FloatLib.Numerics.NumericalSystem.represents_mapScalar {β : Type w} (S : NumericalSystem) (f : S.Scalar → β) (code : S.Code) (x : S.Scalar) (h : S.Represents code x) : (S.mapScalar f).Represents code (f x)

A represented scalar remains represented after mapping the system's scalar codomain.