Precision Projection for Numeric QUDs

A PrecisionProjection N rounds/approximates values of type N. Composing it with a numeric projection yields a QUD that distinguishes meanings only up to that precision — the formal device behind granularity-coarsened questions ("about a hundred" vs. "exactly 103").

structure PrecisionProjection (N : Type) : Type

Precision projection for numeric meanings (approximate vs exact).

• round : N → N

  Round/approximate the value

• name : String

  Name

def PrecisionProjection.exact {N : Type} : PrecisionProjection N

Exact precision: no rounding

Equations

• PrecisionProjection.exact = { round := id, name := "exact" }

def PrecisionProjection.roundTo (k : ℕ) : PrecisionProjection ℕ

Round down to the enclosing multiple of k — the lower representative ⌊n/k⌋·k of the width-k bucket partition; finer k refines the induced QUD (Nat.ker_div_le_of_dvd).

Equations

• PrecisionProjection.roundTo k = { round := fun (n : ℕ) => n / k * k, name := toString "round" ++ toString k }

@[reducible]

def PrecisionProjection.applyToQUD {M N : Type} [BEq N] [LawfulBEq N] (prec : PrecisionProjection N) (proj : M → N) : QUD M

Compose precision with a QUD. Delegates to QUD.ofProject.

Equations

• prec.applyToQUD proj = QUD.ofProject (prec.round ∘ proj) prec.name