reference_in_forcing_chain
plain-language theorem explainer
In any costed configuration space that contains at least one positive-cost object, a symbol space, a cost on it, and a reference structure exist so that some configuration is a genuine symbol for that object. Anyone citing the Physics of Reference or the T0–T8 forcing chain uses this as the bridge that puts reference inside the chain. The proof is a one-line term applying the already-proved forcing theorem for reference.
Claim. Let $P$ be a type equipped with a costed space $(P,J_P)$ (a nonnegative cost $J_P:P\to\mathbb{R}$). If there exists $o\in P$ with $J_P(o)>0$, then there exist a type $S$, a costed space $(S,J_S)$, and a reference structure $R:S\times P\to\mathbb{R}_{\ge 0}$ such that some pair $(s,o)$ is a symbol: $s$ means $o$ under $R$ and $J_S(s)<J_P(o)$.
background
The module formalizes the Physics of Reference: aboutness is ontological compression. A configuration $s$ refers to an object $o$ when the ledger cost of that pointing is minimal and $s$ is strictly cheaper than $o$.
A CostedSpace equips a type $C$ with $J:C\to\mathbb{R}$ and $J\ge 0$, generalizing the RS cost $J(x)=\frac12(x+1/x)-1$. A ReferenceStructure $R:S\to O\to\mathbb{R}$ assigns nonnegative reference costs. A Symbol is a pair $(s,o)$ with meaning (cost-minimizing reference) and compression $J_S(s)<J_O(o)$.
The main prior result is reference_is_forced: any world with a complex ($J>0$) object forces symbols to exist. The Recognition Composition Law (d'Alembert form on $\mathbb{R}_+$) and the broader T0–T8 chain supply the cost axioms that make $J$ unique and nonnegative, so the asymmetry hypothesis is well-posed.
proof idea
One-line term proof: the goal is definitionally the conclusion of reference_is_forced, so the proof is just reference_is_forced P CO h. No extra reconstruction of the symbol space or reference structure is done here; that work lives in the upstream forcing theorem.
why it matters
Places reference inside the T0–T8 forcing chain rather than treating aboutness as an extra primitive. The doc-comment states the link explicitly: in any world with cost asymmetry, reference structures are forced. That matches the module thesis that Recognition IS reference and that ledger entries arise from reference events.
Upstream, uniqueness of $J$ (T5) and the Recognition Composition Law underwrite the cost axioms used by CostedSpace. Downstream the declaration currently has no recorded dependents; it is the named chain-entry point for the Algebra of Aboutness, sitting beside ratio-induced reference, the reference triangle inequality, and the effectiveness principle for near-zero-cost backbones. It does not itself derive $\varphi$, the eight-tick octave, or $D=3$; it only registers reference as a forced consequence once positive cost exists.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.