Core/Scales/Rat01.lean — rational unit interval

A rational number in [0, 1] for gradient linguistic properties (at-issueness, projectivity) and their contextual thresholds.

This file is part of the Phase A decomposition of the legacy Core/Scales/Scale.lean dumping ground (master plan v4).

@[reducible, inline]

abbrev Core.Scale.Rat01 : Type

A rational number in the unit interval [0, 1].

Wraps Mathlib's Set.Icc subtype for gradient linguistic properties (at-issueness, projectivity, etc.) and their contextual thresholds. Using Set.Icc gives us standard interval infrastructure from Mathlib (order, membership, etc.) without custom boilerplate.

Access: r.val for the rational value, r.prop.1 for 0 ≤ r, r.prop.2 for r ≤ 1.

Equations

• Core.Scale.Rat01 = ↑(Set.Icc 0 1)

@[reducible, inline]

abbrev Core.Scale.Rat01.value (r : Rat01) : ℚ

The rational value.

Equations

• r.value = ↑r

theorem Core.Scale.Rat01.nonneg (r : Rat01) : 0 ≤ ↑r

Proof that the value is non-negative.

theorem Core.Scale.Rat01.le_one (r : Rat01) : ↑r ≤ 1

Proof that the value is at most 1.

@[implicit_reducible]

instance Core.Scale.Rat01.instRepr : Repr Rat01

Equations

• Core.Scale.Rat01.instRepr = { reprPrec := fun (r : Core.Scale.Rat01) (x : ℕ) => repr ↑r }

def Core.Scale.Rat01.zero : Rat01

The endpoint 0.

Equations

• Core.Scale.Rat01.zero = ⟨0, Core.Scale.Rat01.zero._proof_1⟩

def Core.Scale.Rat01.one : Rat01

The endpoint 1.

Equations

• Core.Scale.Rat01.one = ⟨1, Core.Scale.Rat01.one._proof_1⟩

def Core.Scale.Rat01.half : Rat01

The midpoint ½, the standard default threshold.

Equations

• Core.Scale.Rat01.half = ⟨1 / 2, Core.Scale.Rat01.half._proof_1⟩

def Core.Scale.Rat01.exceeds (d θ : Rat01) : Prop

Does the value strictly exceed a threshold?

Equations

• d.exceeds θ = (↑θ < ↑d)

@[implicit_reducible]

instance Core.Scale.Rat01.instDecidableExceeds (d θ : Rat01) : Decidable (d.exceeds θ)

Equations

• d.instDecidableExceeds θ = Core.Scale.Rat01.instDecidableExceeds._aux_1 d θ