Embeddings between exact domains

ExactMap Source Target converts exact values between the domains used by numerical families. Binary interchange values, including Lean's native Float32 and Float, use SignedRat, which keeps the sign of zero; posit, fixed-point, logarithmic, and quire values use Rat; OCP E8M0 uses Dyadic; codebooks can use another exact type. The integer, rational, dyadic, and signed-rational embeddings are defined below. Conversion lifts these finite maps over NumericalValue observations.

The map from SignedRat to Rat preserves the rational value and forgets the sign of zero. A conversion through Rat therefore cannot carry a source zero sign to its destination.

Instances must preserve value without rounding, overflow, or a context-dependent choice. The class cannot express that law for arbitrary source and target types, so every non-identity instance needs a separate theorem relating their mathematical interpretations. An arbitrary coercion is insufficient to define an instance.

class FloatLib.Floats.ExecFloat.ExactMap (Source : Type u) (Target : Type v) : Type (max u v)

Canonical embedding between executable exact domains.

This class is an interoperability capability, not an implicit numerical-promotion rule. User values remain statically typed, and destination rounding still occurs only in an explicit conversion or destination-driven operation. Installing an instance is a semantic commitment; preservation must be justified in the source or target domain's own mathematical model.

• map : Source → Target

  Preserve the source's numerical value without rounding.

  Representation metadata can be forgotten: signedRatToRat discards the sign of zero. Preservation of numerical value is justified by separate domain-specific theorems.

@[inline]

def FloatLib.Floats.ExecFloat.ExactMap.run {Source : Type u} {Target : Type v} [self : ExactMap Source Target] (value : Source) : Target

Apply the canonical exact-domain embedding selected for these two types.

@[instance_reducible, instance 100]

instance FloatLib.Floats.ExecFloat.ExactMap.identity {Source : Type u} : ExactMap Source Source

Every exact domain embeds into itself without changing a value.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactMap.run_identity {Source : Type u} (value : Source) : run value = value

The identity exact-domain embedding is computationally the identity.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.ExactMap.intToRat : ExactMap ℤ ℚ

Signed integers embed exactly into rational arithmetic.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactMap.run_intToRat (value : ℤ) : run value = Rat.ofInt value

The signed-integer embedding is Mathlib's exact rational constructor.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.ExactMap.natToRat : ExactMap ℕ ℚ

Natural numbers embed exactly into rational arithmetic.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactMap.run_natToRat (value : ℕ) : run value = Rat.ofInt (Int.ofNat value)

The natural-number embedding has denominator one.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.ExactMap.dyadicToRat : ExactMap Numerics.Dyadic ℚ

Exact dyadic values embed into rationals through their mathematical value.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactMap.run_dyadicToRat (value : Numerics.Dyadic) : run value = value.toRat

The dyadic embedding is the executable exact rational denotation.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.ExactMap.ratToSignedRat : ExactMap ℚ Numerics.SignedRat

Rationals embed into the signed-rational domain; zero receives the positive sign.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactMap.run_ratToSignedRat (value : ℚ) : run value = Numerics.SignedRat.ofRat value

The rational embedding keeps the value and derives the sign from it.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.ExactMap.intToSignedRat : ExactMap ℤ Numerics.SignedRat

Signed integers embed into the signed-rational domain.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactMap.run_intToSignedRat (value : ℤ) : run value = Numerics.SignedRat.ofRat (Rat.ofInt value)

The signed-integer embedding is the rational embedding of the integer.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.ExactMap.natToSignedRat : ExactMap ℕ Numerics.SignedRat

Natural numbers embed into the signed-rational domain.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactMap.run_natToSignedRat (value : ℕ) : run value = Numerics.SignedRat.ofRat (Rat.ofInt (Int.ofNat value))

The natural-number embedding is the rational embedding of the number.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.ExactMap.dyadicToSignedRat : ExactMap Numerics.Dyadic Numerics.SignedRat

Exact dyadics embed into the signed-rational domain, keeping the sign of zero.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactMap.run_dyadicToSignedRat (value : Numerics.Dyadic) : run value = Numerics.SignedRat.ofDyadic value

The dyadic embedding is the sign-preserving signed-rational denotation.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.ExactMap.signedRatToRat : ExactMap Numerics.SignedRat ℚ

Signed rationals embed into Rat by forgetting the sign of zero.

The rational value is preserved, but the target exact domain cannot distinguish the two zero signs. A destination that needs the source zero sign must use a sign-preserving exact domain.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactMap.run_signedRatToRat (value : Numerics.SignedRat) : run value = value.value

The signed-rational embedding into Rat is the value projection.