IsHom
plain-language theorem explainer
A map from referring traces into a pointed referring algebra is a homomorphism when it sends the empty self-reference to the basepoint and intertwines subject and ground one-step extensions with the algebra's two operators. Anyone proving uniqueness or existence of structure-preserving maps out of the referring-trace carrier cites this predicate. It is a pure three-conjunct Prop definition, not a proved statement.
Claim. Let $A$ be a pointed referring algebra 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}}$). A map $h$ from referring traces to $X$ is a homomorphism when $h(\langle\emptyset,\emptyset\rangle)=z$, $h(\langle\mathrm{step}\,s,\,g\rangle)=s_{\mathrm{Sub}}(h(\langle s,g\rangle))$ for all traces $s,g$, and $h(\langle s,\,\mathrm{step}\,g\rangle)=s_{\mathrm{Grd}}(h(\langle s,g\rangle))$ for all $s,g$.
background
In the seam-closure reference module, a referring trace is a pair of ordinary traces: a subject (what is marked) and a ground (the standing context). Reference is genuine only when subject and ground differ; the empty self-reference is the pair of empty traces and is the basepoint of the free structure.
A pointed referring algebra on a carrier $X$ supplies a basepoint $z$ (image of that empty self-reference), a subject-extension operator, a ground-extension operator, and the commutativity law forcing the two orders of double extension to agree. The doc-comment stresses the analogy with the product of two natural-number objects: bi-pointed iterations whose steps commute.
Traces themselves come from the primitive recognition calculus: finite sequences built from the empty trace by one-act extension under the single distinction act $\delta$. The one-step map is exactly that extension. Homomorphisms are the structure-preserving maps that receive both extensions while fixing the basepoint.
proof idea
Definitional, not a proof. The predicate is the conjunction of three equations: basepoint preservation on the empty self-reference; naturality of $h$ under subject extension via $\mathrm{Trace.step}$ against the algebra's subject operator; and naturality under ground extension against the ground operator. No lemmas are invoked; the body is the Prop that later uniqueness and existence theorems instantiate.
why it matters
This predicate is the morphism clause in the initial-object statement that reference is forced by distinction. Downstream, evalHom_isHom shows the recursor-induced evaluation map satisfies it, and reference_forced_by_distinction (O1.3) uses that fact to prove there is a unique homomorphism out of referring traces into any pointed referring algebra.
The parent theorem's doc-comment is explicit: referring traces with empty self-reference as basepoint and the two one-act $\delta$ extensions as steps are the initial pointed referring algebra. No second primitive is introduced; the only act is $\delta$, and the only extra law is the commutativity already forced by two-dimensional generation. That is the exact analogue of the free trace orbit being initial among pointed iterations, now lifted to aboutness.
In the broader Recognition forcing chain this sits in foundation seam-closure work that turns distinction into reference without new generators, feeding the arithmetic and calibration layers that later pin $\varphi$ and the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.