SelfReferenceCost
plain-language theorem explainer
Self-reference cost is the diagonal of a reference structure: the cost of a configuration pointing to itself. Workers in the Algebra of Aboutness cite it when stating that well-behaved reference (especially ratio-induced J-cost) has vanishing self-cost. The definition is a one-line projection of the structure's cost field onto equal arguments.
Claim. Let $R$ be a reference structure on a common configuration space $C$, with non-negative cost $R(s,o)$ of symbol $s$ pointing to object $o$. The self-reference cost of $x \in C$ is $R(x,x)$.
background
The module formalizes the Physics of Reference: aboutness as cost-minimizing compression. A symbol $S$ points to an object $O$ when the ledger link between them minimizes recognition cost. The core object is a reference structure: a non-negative bivariate cost $R : S \to O \to \mathbb{R}$ measuring how expensive it is for $s$ to refer to $o$.
When symbol and object spaces coincide ($S = O = C$), the diagonal $R(x,x)$ is the natural self-reference quantity. The module's thesis is that this diagonal should vanish for well-behaved structures, especially the canonical ratio-induced structure built from the RS cost $J(x) = \tfrac12(x + 1/x) - 1$ (equivalently $\cosh(\log x) - 1$), which is zero at the unit ratio.
Upstream cost notions (observer J-cost on recognition events, multiplicative-recognizer derived cost, PRC quotient J-cost) all feed the same idea: cost is non-negative and vanishes on balanced or unit configurations. Self-reference cost packages that diagonal for the aboutness algebra.
proof idea
Pure definitional abbreviation: evaluate the reference structure's cost field at the pair $(x,x)$. No lemmas, no tactics; the body is the projection $R.\mathrm{cost}, x, x$.
why it matters
Gives a named handle for the diagonal that downstream theorems need. Immediately used by the theorem that ratio-induced reference has vanishing self-cost: for any ratio map $\iota$, $R(x,x) = J(\iota(x)/\iota(x)) = J(1) = 0$. That fact is then packaged into the complete reference summary, which lists self-reference zero among the five pillars of the Algebra of Aboutness (structures, symbols, ratio-induced $J$, mathematical backbone, composition).
In framework terms this is the local expression of balanced recognition: a configuration referring to itself is the unit ratio, where T5's unique $J$ is zero. It ties reference forcing to Law of Existence (defect collapse to zero) and RecognitionForcing (recognition is reference). Without the named diagonal, the summary and the zero-self-cost lemma would restate $R.cost, x, x$ ad hoc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.