reference_triangle
plain-language theorem explainer
Direct reference cost between configurations is always bounded by a two-step chain: either the ordinary triangle holds for a chosen intermediate, or some witness makes the chain bound work. Anyone formalizing cost-minimizing aboutness or reference geometries cites this. The proof is immediate: the second disjunct is always true by taking the witness to be the target, since self-cost vanishes.
Claim. Let $R$ be a reference structure on a type $X$ (a nonnegative cost of one configuration pointing to another). Assume self-reference has zero cost: $R(x,x)=0$ for all $x$. Then for all $a,b,c\in X$, either $R(a,c)\le R(a,b)+R(b,c)$, or there exists a witness $w$ such that $R(a,c)\le R(a,w)+R(w,c)$.
background
The module develops the Algebra of Aboutness: reference as ontological compression. A configuration $S$ points to an object $O$ when the connecting ledger entry minimizes recognition cost. The core object is a reference structure: a map $\mathrm{cost}:S\to O\to\mathbb{R}$ that is pointwise nonnegative.
In Recognition Science the canonical cost on positive ratios is the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$), forced unique by the Recognition Composition Law and landmark T5. Self-cost zero is the natural normalization when a configuration refers to itself. Cost symmetry is hypothesized in the signature but not used in the argument.
The surrounding development ties to Law of Existence (existence as defect collapse to zero), ledger forcing (reference events write ledger entries), and recognition forcing (recognition is reference).
proof idea
The argument never opens the first disjunct. It takes the right branch and supplies the existential witness $w:=c$. After rewriting with the self-cost hypothesis $R(c,c)=0$, the goal reduces to $R(a,c)\le R(a,c)+0$, discharged by linear arithmetic. Symmetry is carried only for interface uniformity with sibling reference lemmas; it plays no role.
why it matters
Module main result 4: chained reference bounds direct reference. It underwrites treating reference structures as cost geometries for later composition and effectiveness results, even though the RS J-cost itself is not a metric. A nearby note records the correct direction $J(r^2)\ge 2J(r)$ (equality only at $r=1$), so the ordinary metric triangle fails for $J$; this theorem therefore uses a disjunctive weakening that always holds under zero self-cost.
No downstream dependents are wired in the current graph (zero used-by edges). The module still places it beside ratio-induced reference, representation equivalence (mutual cost zero), and the effectiveness principle (near-balanced configurations can refer to any positive-cost object). It lives in Foundation, feeding recognition and ledger layers rather than the T0–T8 uniqueness chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.