Explicit projective views of posit quires

These adapters apply Option.toOnePoint to the exact optional semantics. They map the unique quire NaR word to the added point and then to mathlib's projective line, preserving the distinction between NaR and finite values. This geometric interpretation supplies no signed or ordered infinity semantics for quire arithmetic.

References

• Mathlib, OnePoint.equivProjectivization.

@[inline]

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

One-point view of quire meanings over Rat.

The added point represents quire NaR in this view.

@[simp]

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

The zero quire embeds as finite zero in projective rational semantics.

@[simp]

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

The NaR quire embeds as the projective rational point at infinity.

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

Finite one-point coordinates agree exactly with the primary rational semantics.

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

The rational one-point view reaches its added point exactly for quire NaR.

@[inline]

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

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

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

Rational projective-line point representing quire NaR.

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

The rational projective line reaches its distinguished NaR point exactly for quire NaR.

@[inline]

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

Real one-point view of quire meanings.

@[simp]

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

The zero quire embeds as finite zero in projective real semantics.

@[simp]

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

The NaR quire embeds as the projective real point at infinity.

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

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

@[inline]

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

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

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

Real projective-line point representing quire NaR.

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

The real projective line reaches its distinguished NaR point exactly for quire NaR.