evalHom_isHom
plain-language theorem explainer
The canonical evaluation map from referring traces into any pointed referring algebra is a structure-preserving homomorphism. Anyone citing the initial-object forcing of reference by distinction (O1.3) needs this fact. The proof is a short term construction: basepoint by reflexivity, subject step by definitional equality, ground step by the ground-coordinate recursor lemma.
Claim. For any pointed referring algebra $A$ on a carrier $X$ (basepoint $z$, subject extension $s_{\mathrm{Sub}}$, ground extension $s_{\mathrm{Grd}}$, with $s_{\mathrm{Sub}}\circ s_{\mathrm{Grd}}=s_{\mathrm{Grd}}\circ s_{\mathrm{Sub}}$), the canonical evaluation map $h$ induced by recursion on referring traces is a homomorphism: $h$ sends the empty self-reference to $z$, intertwines subject one-step extension with $s_{\mathrm{Sub}}$, and intertwines ground one-step extension with $s_{\mathrm{Grd}}$.
background
In the SeamClosure reference module, a referring trace is a pair of ordinary recognition traces (subject and ground coordinates). The empty self-reference is the basepoint; the only generative act is the one-step distinction extension $\delta$, written Trace.step, applied independently on either coordinate.
A pointed referring algebra on a carrier $X$ packages a basepoint $z$ together with two endomorphisms $s_{\mathrm{Sub}}$ and $s_{\mathrm{Grd}}$ that commute. Commutativity is forced: a two-step referring trace can be reached by extending subject then ground or ground then subject, so any receiving structure must identify the two orders. This is the exact analogue of a product of two natural-number objects among bi-pointed commuting iterations.
The predicate IsHom says a map $h$ from referring traces into $X$ preserves the basepoint and intertwines both one-act extensions. The canonical candidate is the evaluation homomorphism built by recursion on the two coordinates; the present theorem asserts that candidate really is a homomorphism.
proof idea
Term-mode proof via refine ⟨rfl, ?_, ?_⟩ on the three conjuncts of the homomorphism predicate.
Basepoint: evaluation at the empty self-reference equals $A.z$ by definitional reflexivity.
Subject step: for arbitrary subject and ground traces, the intertwining identity holds by rfl (definitional unfolding of the recursor on a subject extension).
Ground step: reduce the goal to the ground-coordinate identity eval A s (Trace.step g) = A.sGrd (eval A s g) and discharge it by the upstream lemma eval_ground_step.
why it matters
This is the structure half of O1.3 in the SeamClosure reference development. Downstream, reference_forced_by_distinction packages existence and uniqueness: referring traces with empty self-reference as basepoint and the two $\delta$-extensions as steps are the initial pointed referring algebra. That theorem opens with refine ⟨evalHom A, evalHom_isHom A, ?_⟩, so the present result supplies the existence witness.
Framework role: reference is forced by distinction alone. No second primitive is introduced; the only act is $\delta$ carried by Trace.step, and the only extra law is the commutativity already forced by two-dimensional generation. This is the precise analogue of the ordinary trace orbit being initial among pointed iterations, and it closes the seam that reference is not an independent ontological ingredient beyond distinction in the Recognition foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.