ratio_reference_symmetric
plain-language theorem explainer
Ratio-induced reference cost between a symbol configuration and an object equals the RS J-cost of the inverted ratio of their positive embeddings. Cite when swapping symbol/object ratios in the Physics of Reference. Proof is a one-line simp that unfolds the ratio-reference definition and cancels double inversion.
Claim. Let $S,O$ be configuration spaces with ratio maps $\iota_S:S\to\mathbb{R}_{>0}$ and $\iota_O:O\to\mathbb{R}_{>0}$. For any $s\in S$ and $o\in O$, the ratio-reference cost of the pair $(s,o)$ equals $J\bigl((\iota_O(o)/\iota_S(s))^{-1}\bigr)$, where $J(x)=\frac{1}{2}(x+x^{-1})-1$.
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 recognition cost. The canonical cost is the RS functional $J(x)=\frac{x+x^{-1}}{2}-1$ on positive ratios (forced uniquely at T5 of the forcing chain).
A RatioMap embeds a configuration space into $\mathbb{R}_{>0}$, so $J$ applies directly. Ratio-induced reference is the reference structure whose pairwise cost is this $J$ on the ratio of the two embeddings. Because $J(x)=J(x^{-1})$, swapping the two ratios leaves the cost unchanged; the present lemma records one algebraic face of that symmetry.
Upstream, $J$ is the same cost used for recognition events and multiplicative recognizers elsewhere in the foundation stack.
proof idea
One-line tactic proof. Unfold the definition of ratio-induced reference, rewrite division as multiplication by inverse (div_eq_mul_inv), and cancel the double inverse (inv_inv). The right-hand side is then definitionally the cost field of the ratio-reference structure. No external lemmas beyond those simp lemmas are required.
why it matters
Sits in the Algebra of Aboutness stack as a basic identity for ratio-induced reference, the canonical reference structure inherited from $J$. It makes the $J(x)=J(x^{-1})$ symmetry of T5 available at the level of symbol/object pairs, so later results on zero-cost matching, triangle inequalities for chained reference, and representational equivalence can treat the two ratio orientations interchangeably.
The module thesis is that reference is forced by cost minimization rather than postulated. This lemma is a small but necessary algebraic hinge: without it, every argument that swaps symbol and object ratios would re-prove inversion invariance of $J$ in place. No downstream dependents are recorded yet; the immediate sibling is the zero-cost characterization (cost vanishes iff the two ratios agree).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.