evalGround
plain-language theorem explainer
Recursive evaluation of a finite distinction trace along the ground-extension of a pointed referring algebra, starting from a chosen subject base value. Empty traces return the base; each extension applies the algebra's ground step. Downstream evaluation of referring pairs and the initial-object forcing theorem both rest on this one-coordinate recursor. The definition is plain structural recursion on Trace.
Claim. Fix a pointed referring algebra $A$ on a carrier $X$ (basepoint, subject step, ground step, and the two steps commute) and a base value $b \in X$. Define $\mathrm{evalGround}_A(b,-):\mathrm{Trace}\to X$ by $\mathrm{evalGround}_A(b,\emptyset)=b$ and $\mathrm{evalGround}_A(b,\mathrm{extend}(g,\delta))=A.s_{\mathrm{grd}}(\mathrm{evalGround}_A(b,g))$.
background
In the seam-closure reference module, a finite trace is the free iteration of a single distinction act: empty, or one extension by a distinction. A pointed referring algebra on a carrier $X$ packages a basepoint $z$ (image of empty self-reference), a subject-extension $s_{\mathrm{sub}}$, a ground-extension $s_{\mathrm{grd}}$, and the law $s_{\mathrm{sub}}\circ s_{\mathrm{grd}}=s_{\mathrm{grd}}\circ s_{\mathrm{sub}}$. Commutativity is forced because a two-coordinate referring pair can be built in either order.
This definition isolates the ground coordinate: it walks a single trace by iterating only $s_{\mathrm{grd}}$, from an arbitrary subject base rather than from $z$. It is the ground half of the two-argument recursor that later evaluates a referring pair into $X$. The pattern matches the LogicNat-style primitive recursion used elsewhere in the foundation (base case plus one step), specialized to Trace and the ground arrow.
proof idea
No proof obligation: the declaration is a definition by pattern matching on Trace. The empty constructor returns the supplied base; the extend constructor applies the algebra's ground map $s_{\mathrm{grd}}$ to the recursive value on the predecessor trace. The DistinctionAct payload is ignored, as only the length of the ground iteration matters for this coordinate.
why it matters
This is the ground leg of the referring-trace recursor. The full evaluator eval calls it on the empty-subject case with basepoint $A.z$, then recurses on the subject with $s_{\mathrm{sub}}$. The non-definitional ground computation rule for eval is proved by induction on the subject using algebra commutativity, and that rule is what makes the unique homomorphism out of referring traces well-defined.
Downstream, the forcing theorem (O1.3) states that referring traces with empty self-reference and the two one-act extensions are the initial pointed referring algebra: for every commuting pointed referring algebra there is a unique structure-preserving map. That is the precise sense in which reference is forced by distinction alone, with no second primitive beyond $\delta$. This ground evaluator is the piece that implements the ground half of that unique map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.