TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Exact.Zero

Declared zero in exact numerical domains #

Checked arithmetic needs a domain-specific way to recognize every representation that should behave as zero. Structural equality is enough for ordinary exact domains, but a carrier may deliberately retain distinctions that its arithmetic forgets. For example, SignedRat has separate positive and negative zeros.

ExactZero keeps that choice explicit and executable. The class guarantees only that canonical 0 is included; concrete domains provide bridge theorems connecting their declared predicate to the representation's numerical meaning. Generic algorithms branch only on this capability.

source
class FloatLib.Numerics.ExactZero (Exact : Type u) [Zero Exact] :
Type u

A decidable predicate declaring which exact values checked arithmetic treats as zero.

  • isZero : Exact → Prop

    Proposition saying that checked arithmetic should treat an exact value as zero.

  • zero_is_zero : isZero 0

    The domain's canonical 0 is included in the declared zero values.

  • decidableIsZero : DecidablePred isZero

    Executable decision procedure for the declared zero predicate.

Instances
    source
    @[instance_reducible, instance 100]
    instance FloatLib.Numerics.ExactZero.ofLawfulBEq {Exact : Type u} [Zero Exact] [BEq Exact] [LawfulBEq Exact] :
    ExactZero Exact

    Use ordinary equality when the domain's Boolean equality is lawful.

    The low priority lets a domain with several zero representations install its own declared-zero relation.

    source
    @[inline]
    def FloatLib.Numerics.ExactZero.test {Exact : Type u} [Zero Exact] [self : ExactZero Exact] (value : Exact) :
    Bool

    Decide whether an exact value satisfies its domain's declared zero predicate.

    Instances For
      source
      @[simp]
      theorem FloatLib.Numerics.ExactZero.test_eq_true_iff {Exact : Type u} [Zero Exact] [self : ExactZero Exact] (value : Exact) :
      test value = true ↔ isZero value

      The executable zero test decides the exact domain's declared proposition.

      source
      @[simp]
      theorem FloatLib.Numerics.ExactZero.test_eq_false_iff {Exact : Type u} [Zero Exact] [self : ExactZero Exact] (value : Exact) :
      test value = false ↔ ¬isZero value

      A failed executable zero test is the negation of the domain's declared zero proposition.

      source
      @[simp]
      theorem FloatLib.Numerics.ExactZero.test_zero {Exact : Type u} [Zero Exact] [self : ExactZero Exact] :
      test 0 = true

      Every exact domain's canonical zero passes its zero test.