eval_ground_step
plain-language theorem explainer
Extending the ground coordinate of a referring trace by one step, then evaluating into a pointed referring algebra, equals applying that algebra's ground-extension after evaluation. Anyone proving that the canonical evaluation map is a referring-algebra homomorphism cites this identity. The proof is induction on the subject trace, with the algebra commutativity law discharging the inductive step; it is the sole non-definitional computation rule for evaluation.
Claim. Let $A$ be a pointed referring algebra on a carrier $X$, with ground-extension operator $s_{\mathrm{Grd}}$. For any finite traces $s$ and $g$, evaluation of $A$ at subject $s$ on the one-step extension of $g$ equals $s_{\mathrm{Grd}}$ applied to the evaluation at $s$ on $g$: $\mathrm{eval}_A(s,\,\mathrm{step}(g)) = s_{\mathrm{Grd}}(\mathrm{eval}_A(s,g))$.
background
A finite trace is either empty or obtained by extending a prior trace by one distinction act. The one-step operator appends the primitive distinction $\delta$. Referring traces pair a subject coordinate with a ground coordinate; both are traces.
A pointed referring algebra on a carrier $X$ supplies a basepoint $z$ (image of the empty self-reference), a subject-extension $s_{\mathrm{Sub}}$, a ground-extension $s_{\mathrm{Grd}}$, and the commutativity law $s_{\mathrm{Sub}}\circ s_{\mathrm{Grd}}=s_{\mathrm{Grd}}\circ s_{\mathrm{Sub}}$. 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 extensions must identify the two orders. The doc-comment calls this "the exact analogue of the product of two natural-number objects being initial among bi-pointed iterations whose two steps commute."
Evaluation folds a referring algebra along a subject/ground pair. Subject-extension steps are definitional in that fold; the ground-extension interaction is not, and is isolated here.
proof idea
Term-mode proof by induction on the subject trace $s$.
Empty subject: both sides reduce by unfolding evaluation, the ground-only evaluator, and the one-step constructor; simp closes the goal.
Inductive step ($s$ extended by one act): the goal rewrites to $s_{\mathrm{Sub}}(\mathrm{eval}(s',\mathrm{step},g))=s_{\mathrm{Grd}}(s_{\mathrm{Sub}}(\mathrm{eval}(s',g)))$. Apply the inductive hypothesis inside, then the algebra commutativity law $s_{\mathrm{Sub}}\circ s_{\mathrm{Grd}}=s_{\mathrm{Grd}}\circ s_{\mathrm{Sub}}$ to swap the two operators.
why it matters
This is the non-definitional half of the claim that canonical evaluation is a structure-preserving map from referring traces into any pointed referring algebra. The sole downstream consumer is the homomorphism theorem for that evaluation map, whose ground-intertwining obligation is exactly this identity (subject-intertwining is rfl).
In the SeamClosure.Reference development, referring algebras package how self-reference and ground distinction compose. Closing the evaluation-as-homomorphism fact pins the initiality analogy stated in the algebra doc-comment: referring traces freely generate the bi-pointed commuting iteration. That sits in the foundation layer feeding Primitive Recognition Calculus structure, upstream of the forcing chain landmarks (J-uniqueness, $\varphi$, eight-tick octave), rather than deriving those landmarks itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.