RepresentationEquiv
plain-language theorem explainer
Two configurations are representationally equivalent when each refers to the other at zero cost (mutual perfect reference). Workers on the Algebra of Aboutness, semantic identity, or zero-cost backbone results cite this predicate. It is a bare definition: the Prop is the conjunction of the two vanishing directed costs.
Claim. Fix a self-referential reference structure $R$ on a configuration space $C$ (a nonnegative cost $R:C\times C\to\mathbb{R}$). Configurations $x,y\in C$ are representationally equivalent when $R(x,y)=0$ and $R(y,x)=0$.
background
The module formalizes the Physics of Reference: aboutness is cost-minimizing compression. A symbol $S$ points to an object $O$ when the ledger link between them minimizes reference cost. The core object is a reference structure: a map $\mathrm{cost}:S\to O\to\mathbb{R}$ that is pointwise nonnegative.
Here the structure is self-referential ($S=O=C$), so cost measures how one configuration refers to another inside the same space. Zero mutual cost is perfect reference in both directions. Upstream cost notions in RS (J-cost on ratios, recognizer-derived costs, event costs) supply concrete instances; the definition itself is agnostic and only needs the abstract nonnegative bifield.
The module thesis ties this to Law of Existence (existence as defect collapse to zero) and RecognitionForcing (recognition is reference). Representation equivalence is the induced semantic sameness relation once perfect mutual reference is available.
proof idea
Definitional, not a proved theorem. The predicate is introduced as the conjunction $R.\mathrm{cost},x,y=0\land R.\mathrm{cost},y,x=0$. No tactics, no lemmas: the body is the Prop itself. Downstream lemmas unpack or reassemble this pair of equalities.
why it matters
Listed as main result 6 in the Algebra of Aboutness module: the semantic equivalence relation induced by reference. It is the target of perfect_implies_representational_equivalence (perfect mutual reference is exactly this predicate) and the carrier for the equivalence-relation package: reflexivity when self-cost vanishes, symmetry by swapping conjuncts, and transitivity once a triangle inequality on cost is assumed.
In the broader RS picture this sits next to the mathematical backbone (zero-cost configurations as universal referents) and the effectiveness principle (near-balanced $J\approx 0$ symbols can refer widely). It does not itself invoke T5 J-uniqueness or the RCL, but any RS-native instance will typically take cost from $J(x)=\frac12(x+x^{-1})-1$ on ratio space, so zero mutual cost means both directed ratios sit at the J-minimum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.