repr_equiv_trans
plain-language theorem explainer
Mutual zero reference cost (representational equivalence) is transitive whenever the reference cost obeys the triangle inequality. Cite this when treating semantic equivalence of configurations as an equivalence relation in the Algebra of Aboutness. The argument is a two-sided squeeze: triangle plus vanishing summands, then nonnegativity forces both directed costs to zero via antisymmetry of ≤.
Claim. Let $R$ be a reference structure on a type $C$: a map $R:C\times C\to\mathbb{R}$ with $R(s,o)\ge 0$. Assume the triangle inequality $R(a,c)\le R(a,b)+R(b,c)$ for all $a,b,c\in C$. If $R(x,y)=R(y,x)=0$ and $R(y,z)=R(z,y)=0$, then $R(x,z)=R(z,x)=0$.
background
The module formalizes the Physics of Reference: aboutness is ontological compression, one configuration pointing to another by minimizing ledger cost. A reference structure on symbol and object types is a real-valued cost of pointing, required to be nonnegative. Here the two types coincide, so the structure is an endocost on configurations.
Representational equivalence means mutual perfect reference: both directed costs vanish. The module lists the triangle inequality for reference costs among its main results (chained reference bounds direct reference) and treats representational equivalence as the induced semantic relation. Nonnegativity of cost is part of the structure package and is the lower bound used to pin equality once an upper bound of zero is obtained.
proof idea
Split the conjunction with constructor. For the forward cost: instantiate the triangle hypothesis at $(x,y,z)$ to get $R(x,z)\le R(x,y)+R(y,z)$; rewrite both summands to $0$ from the two equivalence hypotheses; simplify to $R(x,z)\le 0$; conclude $R(x,z)=0$ by le_antisymm against structural nonnegativity. Repeat with the reversed triple $(z,y,x)$ for the backward cost, rewriting the reverse legs of the two equivalences.
why it matters
This is the transitivity leg of representational equivalence in the Algebra of Aboutness. Together with the sibling reflexivity statement (self-reference cost zero), it makes mutual zero-cost reference an equivalence relation once triangle holds, so configuration spaces can be quotiented by perfect mutual reference. The module thesis ties reference to J-cost minimization and ledger entries; the triangle hypothesis is the same shape as the listed reference_triangle result. No downstream consumers are wired yet in the graph, so the lemma presently closes the local equivalence-relation package rather than feeding a named parent theorem. It sits under Foundation, adjacent to Law of Existence (existence as defect collapse to zero) and RecognitionForcing (recognition as reference).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.