evalHom
plain-language theorem explainer
Canonical evaluation map sending each referring trace into any pointed referring algebra on a carrier X. Cited wherever the initial-object property of reference is used: this is the unique structure-preserving arrow out of referring traces. Defined by feeding the subject and ground coordinates into the algebra's two-coordinate recursor.
Claim. Given a pointed referring algebra $A$ on a carrier $X$ (basepoint $z$, commuting subject and ground extensions), the canonical map $\mathrm{eval}_A:\mathrm{ReferringTrace}\to X$ sends a referring pair $(s,g)$ to the value obtained by iterating $A$'s subject and ground steps from $z$ along $s$ and $g$.
background
A referring trace is a pair of ordinary traces: a subject (what is marked) held against a ground (the standing context). Reference is genuine precisely when subject and ground differ; otherwise the pair points at nothing.
A pointed referring algebra on a carrier $X$ packages a basepoint $z$ (image of the empty self-reference), a subject-extension, a ground-extension, and the law that the two extensions commute. Commutativity is forced: a pair $\langle\mathrm{step},s,\mathrm{step},g\rangle$ can be reached by extending subject after ground or ground after subject, so any structure receiving both steps must identify the two orders. This is the exact analogue of a product of two natural-number objects among bi-pointed commuting iterations.
The underlying two-coordinate recursor evaluates an algebra along a subject trace and a ground trace from a chosen base value. The present definition packages that recursor as a single map out of referring traces.
proof idea
One-line definition: on a referring trace $r$, apply the algebra's two-coordinate evaluator to $r$'s subject and ground fields. No tactics; the body is the lambda that projects those two coordinates into the existing recursor.
why it matters
This is the mediating arrow in the initial-object theorem for reference (O1.3, reference_forced_by_distinction): referring traces with empty self-reference as basepoint and the two one-act $\delta$ extensions as steps form the initial pointed referring algebra. Downstream, evalHom_isHom checks that the map preserves basepoint and both steps, and the uniqueness half of O1.3 identifies every homomorphism with this evaluation.
In the Recognition framework the claim is that reference is forced by distinction alone: no second primitive beyond the single act $\delta$ carried by trace stepping, and no law beyond the commutativity already forced by two-dimensional generation. The map is the concrete witness that every commuting pointed referring algebra receives a unique structure-preserving interpretation of aboutness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.