indicatorReference
plain-language theorem explainer
Canonical indicator reference: a single symbol points uniquely to one chosen target object, with cost 0 on the target and 1 elsewhere. Anyone proving uniqueness of meaning, forced symbols, or the effectiveness principle cites this construction. The body is a direct structure instance; nonnegativity is a two-branch numeric check.
Claim. For any type $O$ with decidable equality and any target $t\in O$, there is a reference structure with symbol space a singleton and object space $O$ whose reference cost is $0$ when the object equals $t$ and $1$ otherwise (hence nonnegative).
background
The module formalizes the Physics of Reference: aboutness is cost-minimizing compression. A configuration $S$ (symbol) points to $O$ (object) when the ledger link between them minimizes cost. The core object is a reference structure: a map $\mathrm{cost}:S\to O\to\mathbb{R}$ together with a proof that every value is nonnegative.
Indicator reference is the discrete extreme case. Symbol space is a unit type (one symbol). Object space is arbitrary with decidable equality. Cost collapses to the classical indicator of equality with a fixed target. This sits beside ratio-induced reference (from the RS $J$-cost) as the simplest structure that still exhibits unique pointing.
Upstream cost notions (observer $J$-cost, multiplicative recognizer cost, rung-coarsened sums) motivate why nonnegative real costs are the right currency; here the cost is hardcoded rather than derived from $J$.
proof idea
Definitional construction, not a deep proof. Fill the reference-structure fields: cost is if o = target then 0 else 1 (independent of the unique symbol). Nonnegativity is discharged by split_ifs on that equality, then norm_num on the constants $0$ and $1$. No external lemmas are required beyond the structure type.
why it matters
Supplies the working example of unique reference used throughout the Algebra of Aboutness. Immediately yields indicator_meaning: the singleton symbol achieves meaning at the target (zero cost there, strictly positive elsewhere).
It is the witness construction inside the existence theorems reference_is_forced (complex objects force cheap symbols) and mathematics_is_absolute_backbone (zero-cost math space as universal compressor), and it seeds the effectiveness principle that near-balanced configurations can refer to any positive-cost object. In framework terms it is the discrete skeleton of reference before the continuous $J$-cost and RCL enter via ratio reference; it makes the "symbol points to object" claim fully concrete for later composition and triangle inequalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.