repr_equiv_symm
plain-language theorem explainer
Mutual zero reference cost is a symmetric relation on configurations. Anyone treating representation equivalence as a semantic equivalence in the Algebra of Aboutness cites this. The proof is a one-line term that swaps the two conjuncts of the mutual-cost definition.
Claim. Let $R$ be a reference structure on a configuration space $C$ (a nonnegative cost $R:C\times C\to\mathbb{R}$). If $x,y\in C$ satisfy $R(x,y)=0$ and $R(y,x)=0$, then $R(y,x)=0$ and $R(x,y)=0$.
background
The module formalizes the Physics of Reference: aboutness is cost-minimizing compression. A reference structure on symbol and object types is a map $\mathrm{cost}:S\to O\to\mathbb{R}$ with $\mathrm{cost}\ge 0$. When $S=O=C$, it scores how one configuration points to another.
Representation equivalence is the induced semantic relation: $x$ and $y$ are equivalent when mutual reference is perfect, i.e. both directed costs vanish. The module pairs this with reflexivity (when self-reference costs zero) and a triangle-inequality form of transitivity.
Local setting is the Algebra of Aboutness, tied to the RS cost $J$ via ratio-induced reference and to ledger/recognition forcing elsewhere in Foundation.
proof idea
Purely definitional. Representation equivalence is the conjunction of the two directed zero-cost statements. The term proof is the pair constructor that swaps those conjuncts: from $\langle h_1,h_2\rangle$ build $\langle h_2,h_1\rangle$. No lemmas, no arithmetic, no appeal to nonnegativity.
why it matters
Closes the symmetry leg of representation equivalence as an equivalence relation on configurations under a self-reference structure. The module lists representation equivalence among its main results: two configurations are representationally equivalent when mutual reference cost is zero. The next sibling targets transitivity under the triangle inequality for reference costs.
In the broader RS picture this is bookkeeping for the Algebra of Aboutness, not a forcing-chain step (T5–T8). It supports treating perfect mutual reference as a genuine equivalence when building composition and effectiveness arguments. No downstream dependents are recorded yet; the lemma is infrastructure for later equivalence-class or quotient reasoning about symbols and objects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.