Optional projective semantics of posits

The primary posit semantics remains NumericalValue Rat: every ordinary word denotes an exact dyadic rational, while the single NaR word denotes ExceptionalValue.notAReal.

For applications that intentionally want a one-point completion, Model.toProjectiveRat is Option.toOnePoint applied to the exact optional semantics: it maps all finite values to their canonical rational point and NaR to the added point. The theorem toProjectiveRat_eq_infty_iff identifies NaR exactly; it remains distinct from every finite point. Mathlib supplies the canonical equivalence from OnePoint Rat to the projective line over Rat.

Finite rational values map canonically into OnePoint Real and the real projective line. This adapter provides coordinates for topology and projective proofs. It does not change the arithmetic interpretation of NaR.

References

• Posit Working Group, Standard for Posit Arithmetic (2022), March 2, 2022, Sections 3--5, https://posithub.org/docs/posit_standard-2.pdf.
• Mathlib, OnePoint.equivProjectivization, https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.toProjectiveRat {format : Format} (value : Model format) : OnePoint ℚ

Intentional one-point projection of posit meanings.

It sends NaR to the added point called ∞ by OnePoint, distinct from all finite values. The name of that point does not give NaR an ordered or signed-infinity interpretation.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toProjectiveRat_zero (format : Format) : (zero format).toProjectiveRat = ↑0

The rational one-point projection sends the canonical zero word to zero.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toProjectiveRat_nar (format : Format) : (nar format).toProjectiveRat = OnePoint.infty

The rational one-point projection sends the unique NaR word to its added point.

theorem FloatLib.Floats.Formats.Posit.Model.toProjectiveRat_eq_coe_iff {format : Format} (value : Model format) (rational : ℚ) : value.toProjectiveRat = ↑rational ↔ value.toRat? = some rational

The one-point projection agrees with the exact rational view on every ordinary posit.

Together with toProjectiveRat_eq_infty_iff, this characterizes the complete projection: finite points correspond exactly to some rational, and the added point corresponds exactly to NaR.

theorem FloatLib.Floats.Formats.Posit.Model.toProjectiveRat_eq_infty_iff {format : Format} (value : Model format) : value.toProjectiveRat = OnePoint.infty ↔ value.isNaR = true

The projective view reaches its added point exactly for the NaR encoding.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.toProjectiveRatLine {format : Format} (value : Model format) : Projectivization ℚ (Fin 2 → ℚ)

Canonical rational projective-line point associated with the rational one-point view.

def FloatLib.Floats.Formats.Posit.Model.projectiveRatNaR : Projectivization ℚ (Fin 2 → ℚ)

Rational projective-line point chosen for NaR by the one-point view.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toProjectiveRatLine_zero (format : Format) : (zero format).toProjectiveRatLine = (OnePoint.equivProjectivization ℚ) ↑0

The rational projective-line projection sends the canonical zero word to zero.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toProjectiveRatLine_nar (format : Format) : (nar format).toProjectiveRatLine = projectiveRatNaR

The rational projective-line projection sends NaR to its distinguished added point.

theorem FloatLib.Floats.Formats.Posit.Model.toProjectiveRatLine_eq_finite_iff {format : Format} (value : Model format) (rational : ℚ) : value.toProjectiveRatLine = (OnePoint.equivProjectivization ℚ) ↑rational ↔ value.toRat? = some rational

Equality of finite projective-line points is exactly equality of their rational coordinates.

The equivalence is inherited from mathlib's OnePoint.equivProjectivization; no separate posit notion of projective equality is introduced.

theorem FloatLib.Floats.Formats.Posit.Model.toProjectiveRatLine_eq_nar_iff {format : Format} (value : Model format) : value.toProjectiveRatLine = projectiveRatNaR ↔ value.isNaR = true

The rational projective-line view is its NaR point exactly for the NaR encoding.

Mathlib real and real-projective views

@[inline]

noncomputable def FloatLib.Floats.Formats.Posit.Model.toProjectiveReal {format : Format} (value : Model format) : OnePoint ℝ

Intentional real one-point projection of posit meanings.

The finite branch is the canonical injection Rat → Real; NaR alone maps to the added point. This view is useful for topology and analysis. Its type distinguishes this geometric interpretation from the notAReal exception used by decodeReal.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toProjectiveReal_zero (format : Format) : (zero format).toProjectiveReal = ↑0

The real one-point projection sends the canonical zero word to zero.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toProjectiveReal_nar (format : Format) : (nar format).toProjectiveReal = OnePoint.infty

The real one-point projection sends the unique NaR word to its added point.

theorem FloatLib.Floats.Formats.Posit.Model.toProjectiveReal_eq_coe_iff {format : Format} (value : Model format) (rational : ℚ) : value.toProjectiveReal = ↑↑rational ↔ value.toRat? = some rational

A finite rational coordinate is preserved exactly by the real one-point projection.

theorem FloatLib.Floats.Formats.Posit.Model.toProjectiveReal_eq_infty_iff {format : Format} (value : Model format) : value.toProjectiveReal = OnePoint.infty ↔ value.isNaR = true

The real one-point projection reaches its added point exactly for NaR.

@[inline]

noncomputable def FloatLib.Floats.Formats.Posit.Model.toProjectiveRealLine {format : Format} (value : Model format) : Projectivization ℝ (Fin 2 → ℝ)

Canonical real projective-line point associated with the real one-point view.

noncomputable def FloatLib.Floats.Formats.Posit.Model.projectiveRealNaR : Projectivization ℝ (Fin 2 → ℝ)

Real projective-line point chosen for NaR by the one-point view.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toProjectiveRealLine_zero (format : Format) : (zero format).toProjectiveRealLine = (OnePoint.equivProjectivization ℝ) ↑0

The real projective-line projection sends the canonical zero word to zero.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toProjectiveRealLine_nar (format : Format) : (nar format).toProjectiveRealLine = projectiveRealNaR

The real projective-line projection sends NaR to its distinguished added point.

theorem FloatLib.Floats.Formats.Posit.Model.toProjectiveRealLine_eq_finite_iff {format : Format} (value : Model format) (rational : ℚ) : value.toProjectiveRealLine = (OnePoint.equivProjectivization ℝ) ↑↑rational ↔ value.toRat? = some rational

Finite real projective coordinates agree exactly with the embedded rational semantics.

theorem FloatLib.Floats.Formats.Posit.Model.toProjectiveRealLine_eq_nar_iff {format : Format} (value : Model format) : value.toProjectiveRealLine = projectiveRealNaR ↔ value.isNaR = true

The real projective-line view is its NaR point exactly for the NaR encoding.