Meaning
plain-language theorem explainer
Meaning is the cost-minimizing semantic relation: under a reference structure, symbol s means object o exactly when o attains the least reference cost among all objects. It is the primitive "aboutness" predicate of the Algebra of Aboutness. Anyone proving effectiveness, composition, or referential capacity cites it. The body is a direct universal quantification comparing costs.
Claim. Let $R$ be a reference structure on symbol type $S$ and object type $O$, with nonnegative cost $c_R:S\times O\to\mathbb{R}$. Then $s$ means $o$ under $R$ if and only if $c_R(s,o)\le c_R(s,o')$ for every $o'\in O$ (i.e., $o$ is a global cost minimizer for $s$).
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 cost. The core object is a reference structure: a map $c:S\to O\to\mathbb{R}$ with $c(s,o)\ge 0$ for all pairs.
Meaning is the induced semantic relation on that structure. It does not invent a new cost; it packages the argmin condition. Upstream cost notions (observer J-cost on recognition events, multiplicative-recognizer derived cost, rung-coarsen summed ratio weights, PRC quotient J-cost) all supply concrete instances of such nonnegative costs once lifted into a reference structure.
Local setting: reference is forced from asymmetry whenever complex ($J>0$) objects exist; zero-cost (mathematical) configurations have universal referential reach. Meaning is the predicate those theorems quantify over.
proof idea
Definitional, not a proof. The body is the Prop $\forall o',; R.\mathrm{cost}, s, o \le R.\mathrm{cost}, s, o'$. No tactics, no lemmas: it is the least-cost target condition written as a universal inequality over the object type.
why it matters
This is the core semantic relation of the Algebra of Aboutness. Downstream, the effectiveness principle states that near-balanced symbols ($J\approx 0$) can mean any positive-cost object; its conclusion is existence of $s$ with Meaning. Indicator reference proves Meaning at the designated target. Product composition preserves Meaning componentwise. Referential capacity is defined as the set of objects for which some cheaper symbol satisfies Meaning, and mathematical universal capacity upgrades that to all positive-cost objects when the symbol space is mathematical.
UniqueMeaning, Symbol, and PerfectSymbol refine the same predicate (strict minimizer, symbolic status). In the broader RS chain, reference events are ledger entries and recognition is reference; Meaning is where that identification becomes a usable Prop. It sits under the J-cost uniqueness (T5) and the Recognition Composition Law once concrete ratio costs are plugged into the reference structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.