TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Configured.Projective

Optional projective views of configured posits #

These adapters intentionally map NaR to the added point of mathlib's one-point completion and projective line. They are proof-side views, not executable posit semantics, and are kept outside the basic configured API to avoid imposing topology and projective-geometry dependencies on ordinary programs.

source
@[inline]
def FloatLib.Floats.ExecFloat.Posit.toProjectiveRat {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
OnePoint ℚ

Explicit one-point view of a configured posit.

This view maps NaR to OnePoint.infty, reinterpreting its meaning as the added projective point. The primary denotation returned by decode keeps NaR as ExceptionalValue.notAReal.

Instances For
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.Posit.toProjectiveRatLine {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
    Projectivization ℚ (Fin 2 → ℚ)

    Canonical mathlib rational projective-line view of a configured posit.

    Instances For
      source
      @[inline]
      noncomputable def FloatLib.Floats.ExecFloat.Posit.toProjectiveReal {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
      OnePoint ℝ

      Explicit real one-point view, obtained by embedding exact rational finite values.

      Instances For
        source
        @[inline]
        noncomputable def FloatLib.Floats.ExecFloat.Posit.toProjectiveRealLine {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
        Projectivization ℝ (Fin 2 → ℝ)

        Canonical mathlib real projective-line view of a configured posit.

        Instances For
          source
          @[simp]
          theorem FloatLib.Floats.ExecFloat.Posit.toProjectiveRat_eq_infty_iff {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
          toProjectiveRat value = OnePoint.infty ↔ isNaR value = true

          A configured posit maps to the rational point at infinity exactly when it is NaR.

          source
          @[simp]
          theorem FloatLib.Floats.ExecFloat.Posit.toProjectiveRat_eq_coe_iff {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (rational : ℚ) :
          toProjectiveRat value = ↑rational ↔ toRat? value = some rational

          Equality with a finite rational point is equivalent to the exact optional rational view.

          source
          theorem FloatLib.Floats.ExecFloat.Posit.toProjectiveRatLine_eq_finite_iff {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (rational : ℚ) :
          toProjectiveRatLine value = (OnePoint.equivProjectivization ℚ) ↑rational ↔ toRat? value = some rational

          The rational projective-line view represents precisely the same finite rational values.

          source
          @[simp]
          theorem FloatLib.Floats.ExecFloat.Posit.toProjectiveRatLine_eq_nar_iff {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
          toProjectiveRatLine value = Formats.Posit.Model.projectiveRatNaR ↔ isNaR value = true

          The distinguished rational projective point is attained exactly by posit NaR.

          source
          @[simp]
          theorem FloatLib.Floats.ExecFloat.Posit.toProjectiveReal_eq_infty_iff {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
          toProjectiveReal value = OnePoint.infty ↔ isNaR value = true

          A configured posit maps to the real point at infinity exactly when it is NaR.

          source
          @[simp]
          theorem FloatLib.Floats.ExecFloat.Posit.toProjectiveReal_eq_coe_iff {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (rational : ℚ) :
          toProjectiveReal value = ↑↑rational ↔ toRat? value = some rational

          Equality with an embedded rational real point agrees with the exact rational view.

          source
          theorem FloatLib.Floats.ExecFloat.Posit.toProjectiveRealLine_eq_finite_iff {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (rational : ℚ) :
          toProjectiveRealLine value = (OnePoint.equivProjectivization ℝ) ↑↑rational ↔ toRat? value = some rational

          The real projective-line view represents precisely the embedded finite rational values.

          source
          @[simp]
          theorem FloatLib.Floats.ExecFloat.Posit.toProjectiveRealLine_eq_nar_iff {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
          toProjectiveRealLine value = Formats.Posit.Model.projectiveRealNaR ↔ isNaR value = true

          The distinguished real projective point is attained exactly by posit NaR.