eval
plain-language theorem explainer
The unique recursor that interprets a pair of finite traces (subject, ground) in any pointed referring algebra. Citation target for anyone building maps out of referring traces or proving initiality of the free referring structure. Defined by recursion on the subject, then ground evaluation from the algebra basepoint.
Claim. Given a pointed referring algebra $A$ on a carrier $X$ (basepoint $z$, subject step $s_{\mathrm{sub}}$, ground step $s_{\mathrm{grd}}$, with $s_{\mathrm{sub}}\circ s_{\mathrm{grd}}=s_{\mathrm{grd}}\circ s_{\mathrm{sub}}$), there is a map $\mathrm{eval}_A:\mathrm{Trace}\times\mathrm{Trace}\to X$ sending $(\varepsilon,g)$ to the pure ground iteration of $g$ from $z$, and $(\mathrm{extend}(s,\_),g)$ to $s_{\mathrm{sub}}(\mathrm{eval}_A(s,g))$.
background
In the primitive recognition calculus, a finite trace is either empty or one distinction act stacked on a shorter trace. Referring structure treats two such traces as subject and ground coordinates of a self-reference.
A pointed referring algebra on $X$ packages a basepoint $z$ (image of the empty self-reference), a subject-extension map, a ground-extension map, and the law that the two extensions commute. Commutativity is forced: the same pair of steps can be ordered subject-then-ground or ground-then-subject, so any receiving structure must identify both paths. The doc-comment likens this to the product of two natural-number objects among bi-pointed iterations whose steps commute.
Ground-only evaluation is already defined: from a fixed subject base value, iterate the ground step along a ground trace. The present map lifts that to full subject-ground pairs.
proof idea
Definitional recursor, not a proved theorem. Pattern-match on the subject trace: empty subject reduces to ground evaluation from the algebra basepoint $z$; an extended subject applies the subject-step once to the recursive value on the shorter subject with the same ground. The ground coordinate is never matched at the outer level; it is consumed entirely inside the ground evaluator. No tactics or lemmas are invoked in the body.
why it matters
This is the elimination principle for referring traces into any structure that can host commuting subject and ground steps. It is the exact analogue of the recursor for $\mathbb{N}\times\mathbb{N}$ once the two generators are required to commute, and it sits in the SeamClosure.Reference layer that turns free referring data into concrete carriers.
In the broader Recognition forcing chain, self-reference and distinction acts underwrite the path from the recognition composition law through the eight-tick octave and $D=3$. A clean eval map is what lets later modules interpret abstract referring traces inside algebras tied to those forced structures. No downstream theorems are wired yet in the graph, so this declaration is infrastructure awaiting initiality or uniqueness arguments that quote it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.