ReferenceQuality
plain-language theorem explainer
Four-level ranking of how well a symbol refers to an object, ordered by reference cost R: perfect (R = 0), optimal (R minimal among symbols), effective (R below a threshold), and weak (R finite). Downstream classifiers and effectiveness arguments cite it as the discrete quality type. As an inductive definition it carries no proof burden beyond decidable equality and printing.
Claim. An inductive type of reference qualities with four constructors: perfect when the reference cost vanishes ($R = 0$); optimal when $R$ attains the infimum over available symbols; effective when $R < \varepsilon$ for a chosen threshold $\varepsilon$; and weak when $R$ is merely finite.
background
The module formalizes reference as cost-minimizing compression: a symbol $S$ is about an object $O$ when the ledger link between them minimizes the RS cost $J$. The core cost is $J(x) = \frac12(x + 1/x) - 1$ (equivalently $\cosh(\log x) - 1$), and reference structures package a cost map $R : S \times O \to \mathbb{R}_{\ge 0}$ together with the axioms that make $R$ a legitimate aboutness measure.
Sibling notions include ReferenceStructure (the costed pair), symbols versus perfect symbols, and mathematical versus near-mathematical configurations (zero or near-zero $J$). The quality ladder sits above those definitions: it does not redefine cost, it grades an already-computed $R$.
Module results such as forced emergence of symbols from positive-$J$ objects, the triangle inequality for chained reference, and the effectiveness principle (near-balanced configurations can refer to any positive-cost object) all presuppose a discrete way to report how good a given link is.
proof idea
No proof body: this is a pure inductive datatype with four nullary constructors, deriving DecidableEq and Repr. The intended semantics of each constructor are fixed by the doc-comment (cost zero, cost-minimal, cost below threshold, cost finite) and are enforced only at use sites such as the classifier that pattern-matches on numerical comparisons of $R$.
why it matters
Gives the discrete vocabulary for the Physics of Reference. The immediate consumer is classifyReference, which turns a concrete cost $R(s,o)$ and threshold $\varepsilon$ into one of these four tags (perfect if cost is zero, else effective if below $\varepsilon$, else weak). That classification supports the effectiveness principle and the mathematical-backbone claim: zero-cost configurations are perfect referents with universal capacity, while near-zero configurations are at least effective.
In the broader RS chain this is scaffolding language for aboutness, not a forcing step (T5–T8). It connects Law of Existence (defect collapse to zero), ledger forcing (reference events as ledger entries), and recognition-as-reference, by making “how good is this pointer” a first-class, decidable value rather than prose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.