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.Order.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.Order.Rat01 = ↑(Set.Icc 0 1)

@[reducible, inline]

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

The rational value.

Equations

• r.value = ↑r

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

Proof that the value is non-negative.

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

Proof that the value is at most 1.

@[implicit_reducible]

instance Core.Order.Rat01.instRepr : Repr Rat01

Equations

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

def Core.Order.Rat01.zero : Rat01

The endpoint 0.

Equations

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

def Core.Order.Rat01.one : Rat01

The endpoint 1.

Equations

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

def Core.Order.Rat01.half : Rat01

The midpoint ½, the standard default threshold.

Equations

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

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

Does the value strictly exceed a threshold?

Equations

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

@[implicit_reducible]

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

Equations

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

def Core.Order.Rat01.compl (r : Rat01) : Rat01

The complement 1 - r, again in [0, 1].

Models the relationship between a gradient property and its dual on the same scale — e.g. not-at-issueness as the complement of at-issueness.

Equations

• r.compl = ⟨1 - ↑r, ⋯⟩

@[simp]

theorem Core.Order.Rat01.compl_val (r : Rat01) : ↑r.compl = 1 - ↑r

@[simp]

theorem Core.Order.Rat01.compl_compl (r : Rat01) : r.compl.compl = r

theorem Core.Order.Rat01.compl_zero : zero.compl = one

theorem Core.Order.Rat01.compl_one : one.compl = zero

theorem Core.Order.Rat01.compl_antitone : Antitone compl

The complement is order-reversing: a larger value has a smaller complement.