classifyReference
plain-language theorem explainer
Given a reference structure, a symbol, an object, and a threshold ε, this classifier returns perfect when the reference cost is zero, effective when the cost is positive but below ε, and weak otherwise. Anyone working the Algebra of Aboutness uses it to grade how well a configuration points to another. The body is a three-way case split on the cost value; optimal is not assigned here.
Claim. For a reference structure $R$ on symbol type $S$ and object type $O$, a symbol $s\in S$, an object $o\in O$, and a threshold $\varepsilon\in\mathbb{R}$, return the reference quality of $(s,o)$: perfect if $R(s,o)=0$, effective if $0<R(s,o)<\varepsilon$, and weak otherwise.
background
The module formalizes reference as cost-minimizing compression: a symbol $S$ points to an object $O$ when the ledger link between them minimizes cost. A ReferenceStructure is the core object: a nonnegative cost map $S\to O\to\mathbb{R}$. The RS cost $J(x)=\frac12(x+1/x)-1$ (equivalently $\cosh(\log x)-1$) is the canonical engine behind ratio-induced reference elsewhere in the file.
ReferenceQuality orders reference types by cost: perfect ($R=0$, direct identity), optimal ($R$ minimal among symbols), effective ($R$ below a practical threshold), and weak (finite but not useful). Related modules treat existence as defect collapse to zero and recognition events as J-costed ledger entries; the identity event sits at state $1$ with zero cost.
This classifier is the operational readout of that quality scale for a fixed pair $(s,o)$ and threshold $\varepsilon$.
proof idea
Pure definition by nested conditionals on $R.\mathrm{cost},s,o$. First branch: equality with zero yields perfect. Second: strict inequality below $\varepsilon$ yields effective. Residual case yields weak. No lemmas are applied; optimal is never emitted by this map.
why it matters
It turns the qualitative ladder in the Physics of Reference into a concrete grading function used when stating effectiveness and backbone results. The module thesis is that aboutness is forced by cost minimization: zero-cost configurations have universal referential capacity, and near-balanced ones ($J\approx 0$) can refer to any positive-cost object (effectiveness principle). Perfect quality lines up with identity and representation equivalence (mutual cost zero). The definition sits downstream of the J-cost and recognition-event cost conventions and upstream of any prose or theorem that needs a discrete quality label rather than a raw real cost. No used_by edges are recorded yet; it is infrastructure for the Algebra of Aboutness rather than a forcing-chain step (T5–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.