indicator_meaning
plain-language theorem explainer
The indicator reference structure aimed at a fixed target makes the unit symbol mean that target: reference cost is minimized exactly there. Anyone proving forced emergence of symbols, mathematical backbone, or the effectiveness principle cites this as the elementary witness that a pure pointer achieves meaning. The proof unfolds the indicator cost and splits on equality, reducing both branches by arithmetic.
Claim. Let $O$ be a type with decidable equality and let $t \in O$. Under the indicator reference structure aimed at $t$, the unique unit symbol means $t$: for every $o' \in O$, the reference cost from the unit to $t$ is at most the reference cost from the unit to $o'$.
background
The module formalizes the Physics of Reference: aboutness is ontological compression. A configuration $S$ (symbol) points to $O$ (object) when the ledger link between them minimizes $J$-cost. A ReferenceStructure packages a cost map $R.cost : S \to O \to \mathbb{R}$; meaning is the semantic relation that $s$ means $o$ when $o$ is a global minimizer of $R.cost, s,(-)$.
The indicator construction is the purest pointer: its symbol space is the unit type, and its cost is the classical $0/1$ indicator of equality with a fixed target. It sits beside the ratio-induced reference structure, whose cost is $J(\mathrm{ratio}(s)/\mathrm{ratio}(o))$ with the RS cost $J(x)=\tfrac12(x+1/x)-1$. Upstream cost notions (observer $J$-cost on recognition events, multiplicative-recognizer derived cost, rung-coarsened total cost) all feed the same minimization language used here.
Local setting: existence equals defect collapse to zero; recognition is reference; ledger entries record reference events. This lemma is the elementary sanity check that a perfect pointer really does mean its target.
proof idea
Term-mode proof by unfolding. Introduce an arbitrary competitor $o'$. Simplify the indicator reference cost definition. Rewrite with the positive branch of the equality test at the target (reflexivity), so the left-hand cost is the zero branch. Case-split on whether $o'$ equals the target; both branches close by norm_num (costs are $0$ or $1$, and $0 \le 0$, $0 \le 1$). No external lemmas beyond the definition of the indicator structure and decidable equality.
why it matters
This is the seed witness for the Algebra of Aboutness. Downstream, reference_is_forced uses such cheap symbols to show that any world with positive-$J$ objects forces the emergence of symbols; mathematics_is_absolute_backbone lifts the zero-cost case to Wigner's effectiveness (mathematics as maximal compressor); effectiveness_principle generalizes to near-balanced symbols that can mean any expensive object.
In framework terms it is the discrete, unit-symbol instance of cost-minimizing reference that the ratio-induced construction later inherits from $J$. It does not itself invoke the forcing chain T5–T8 or the RCL identity, but it supplies the semantic relation those later structures must satisfy when they claim to mean something. Closes no open scaffold; it is a fully proved elementary step inside Foundation.Reference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.