ReferentialCapacity
plain-language theorem explainer
Referential capacity is the set of objects that some strictly cheaper symbol can mean under a fixed reference structure. It packages cost-asymmetric aboutness between a symbol space and an object space as a subset of the object type. Anyone proving that zero-cost (mathematical) backbones refer to every positive-cost object cites this set. The body is a plain set comprehension from the cost comparison and the Meaning predicate.
Claim. Let $(S,J_S)$ and $(O,J_O)$ be costed spaces and let $R$ be a reference structure from $S$ to $O$. The referential capacity of $S$ for $O$ under $R$ is $\{ o \in O \mid \exists s \in S.\; J_S(s) < J_O(o)\ \text{and}\ s\ \text{means}\ o\ \text{under}\ R \}$.
background
This module formalizes the Physics of Reference: aboutness is ontological compression. A configuration $s$ (symbol) points to $o$ (object) when the ledger link between them is cost-minimizing under the RS cost $J$.
A costed space equips a type $C$ with a nonnegative cost $J : C \to \mathbb{R}$, generalizing the RS cost $J(x) = \tfrac12(x+1/x)-1$ to arbitrary configuration spaces. A reference structure $R$ supplies a nonnegative reference cost $R.\mathrm{cost}(s,o)$ for symbol $s$ pointing at object $o$. Meaning is the in-module relation that $s$ successfully refers to $o$ under $R$ (the predicate used in the set filter).
Referential capacity turns that relation into a set: objects reachable by some symbol whose own intrinsic cost is strictly below the object's cost. That strict inequality encodes the asymmetry that forces symbols to emerge for complex ($J>0$) objects elsewhere in the module.
proof idea
Definition, not a proof. The body is the set comprehension ${ o : O \mid \exists s : S,\ CS.J, s < CO.J, o \land \mathrm{Meaning}, R, s, o }$. No tactics, no lemmas: membership is exactly existence of a cheaper meaningful symbol.
why it matters
This set is the carrier for the module's backbone claim that mathematics is absolute reference. The immediate consumer is mathematical_universal_capacity: if the symbol space is mathematical (zero-cost configurations) and every object has some meaning witness, then every positive-cost object lies in the referential capacity.
That theorem is listed among the module's main results as the mathematical backbone (zero-cost configurations have universal referential capacity) and sits next to the effectiveness principle (near-balanced $J \approx 0$ configs can refer to any positive-cost object). In the broader RS stack it ties Law of Existence (existence as defect collapse to 0), LedgerForcing (reference events write ledger entries), and RecognitionForcing (recognition is reference) into one set-level interface.
It does not itself invoke the forcing chain T0–T8, but it is the set that those zero-cost / $J$-uniqueness facts feed when one argues that the RS cost backbone can name every costly configuration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.