ReferringAlgebra
plain-language theorem explainer
A pointed referring algebra is a carrier with basepoint z, subject step sSub, ground step sGrd, and the law that the two steps commute. Anyone building the recursor from referring traces into a semantic carrier cites this structure. It is pure data: four fields, no proof obligation beyond the commutativity equation.
Claim. A pointed referring algebra on a type $X$ consists of a basepoint $z \in X$, two endomorphisms $s_{\mathrm{sub}}, s_{\mathrm{grd}} : X \to X$, and the identity $s_{\mathrm{sub}} \circ s_{\mathrm{grd}} = s_{\mathrm{grd}} \circ s_{\mathrm{sub}}$. The basepoint is the image of the empty self-reference; the two maps are the one-act subject and ground extensions.
background
In the SeamClosure.Reference module, a referring trace is a pair of finite traces (subject and ground), generated from the empty self-reference by one-act extensions on either coordinate. The empty pair is the pure self-reference; stepping the subject or the ground records which side of the distinction was extended.
Any structure that receives both extensions must treat the two orders as the same point: extending subject then ground equals extending ground then subject. That is exactly the product of two natural-number objects being initial among bi-pointed iterations whose steps commute. The algebra packages that data on an arbitrary carrier $X$.
Upstream, the PrimitiveDistinction and PrimitiveRecognitionCalculus layers supply the distinction and certified real-valued protocols that later evaluations land in; this structure is the intermediate semantic interface between free referring traces and those concrete carriers.
proof idea
No proof: this is a structure declaration. The four fields are the basepoint, the two extension maps, and the single equational axiom that the extensions commute. Downstream lemmas (especially the ground-step rule for the recursor) invoke that axiom by induction on the subject coordinate.
why it matters
This is the semantic target for the referring-trace recursor. Downstream, eval and evalGround interpret a pair of traces by iterating $s_{\mathrm{sub}}$ and $s_{\mathrm{grd}}$ from $z$; eval_ground_step is the one non-definitional computation rule and uses commutativity by induction on the subject. IsHom and evalHom_isHom package the universal property: the free referring trace maps uniquely into any such algebra.
In the Recognition framework this sits in the foundation seam-closure layer: reference is reduced to distinction plus commuting bi-iteration, so later forcing (T0–T8 bridge, ledger floor) can treat reference as generated structure rather than a primitive. The parent result reference_forced_by_distinction uses the algebra to close that reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.