reference_is_forced
plain-language theorem explainer
Any costed object space that contains at least one positive-cost configuration forces a nonempty symbol: some cheaper configuration that means that object under a reference structure. Cite this for the Algebra of Aboutness existence claim and for the T5-to-reference bridge in the unified forcing chain. The proof is a classical constructive witness: the unit type with zero cost and the indicator reference at the expensive object.
Claim. Let $O$ be a type equipped with a cost $J_O : O \to \mathbb{R}_{\ge 0}$. If there exists $o \in O$ with $J_O(o) > 0$, then there exist a symbol space $S$ with cost $J_S$, a reference structure $R : S \times O \to \mathbb{R}_{\ge 0}$, and a pair $(s,o)$ such that $s$ means $o$ under $R$ and $J_S(s) < J_O(o)$.
background
The module formalizes the Physics of Reference: aboutness is ontological compression. A configuration $S$ points to $O$ when the ledger cost of that link is minimal. A CostedSpace equips a type with a nonnegative intrinsic cost $J$, generalizing the RS cost $J(x)=\frac12(x+1/x)-1$. A ReferenceStructure supplies a nonnegative cost of one configuration referring to another.
A Symbol is the ontological core of that story: a pair $(s,o)$ where $s$ means $o$ (minimizes reference cost) and $s$ is strictly cheaper than $o$ (compression). The module thesis is that such symbols are not primitives; they are forced whenever the object side has positive cost.
Upstream, the indicator reference structure on the unit type sends the unique symbol to cost $0$ at a chosen target and cost $1$ elsewhere. The lemma indicator_meaning records that this map achieves meaning at that target. The unit costed space is the zero-cost backbone used throughout the forcing bridges.
proof idea
Classical choice extracts a complex object $o_c$ with $J(o_c)>0$ from the hypothesis. The witness is then explicit: symbol space $\mathbf{1}$ (Unit), the unit costed space (uniformly zero $J$), and the indicator reference pinned at $o_c$.
The Symbol record is filled by the unique unit element as $s$, $o_c$ as the object, indicator_meaning for the meaning field, and the strict inequality $0 < J(o_c)$ for compression. No further lemmas are needed; the construction is the proof.
why it matters
This is Main Result 1 of the Algebra of Aboutness: reference from asymmetry. Downstream, reference_in_forcing_chain is a one-line re-export that places the same existence claim inside the T0–T8 narrative. The unified forcing chain uses it in the T5-to-canonical-reference bridge (t5_to_canonical_reference_bridge_holds), where the legacy existential is derived alongside the mathematical-backbone theorem and the unit costed space as canonical zero-cost reference.
In framework terms it sits after T5 J-uniqueness: once a genuine cost asymmetry exists, cheap symbols must appear. That is the existence half of why mathematics (zero-cost configurations) can serve as universal compressor, and why recognition events create ledger entries about something. It does not yet force uniqueness of the symbol system; uniqueness and effectiveness are handled by sibling results such as the absolute-backbone theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.