Effective Protocol Action Monoid

Abstract

Protocol words modulo equality of their state actions form a faithful effective monoid.

Theorem 1.1 (The protocol action-kernel quotient is faithful).

$$\begin{array}{r}\forall A,Q:\mathrm{Type},\\ \mathrm{MonoidAction}(\mathrm{FreeMonoid}(A),Q),\\ rhoAct(u,v):=\forall z:Q,u(z)=v(z),\\ Mact:=\mathrm{ConQuotient}(\ker (\mathrm{ActionEnd}(\mathrm{FreeMonoid}(A),Q))),\\ alphaAct:=\mathrm{MulActionOfEndHom}(\mathrm{kerLift}(\mathrm{ActionEnd}(\mathrm{FreeMonoid}(A),Q))),\\ \mathrm{Equivalence}(rhoAct)\wedge \\ (\forall p:\mathrm{FreeMonoid}(A),u:\mathrm{FreeMonoid}(A),v:\mathrm{FreeMonoid}(A),rhoAct(u,v)\Rightarrow rhoAct(p\cdot u,p\cdot v))\wedge \\ (\forall s:\mathrm{FreeMonoid}(A),u:\mathrm{FreeMonoid}(A),v:\mathrm{FreeMonoid}(A),rhoAct(u,v)\Rightarrow rhoAct(u\cdot s,v\cdot s))\wedge \\ \mathrm{FaithfulAction}(Mact,Q,alphaAct).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Control/EffectiveProtocolActionMonoid.effective_protocol_action_monoid (✓ std3). ∎

Source. Repository-derived.

Commentary.

The protocol carrier is the free monoid on the action alphabet. Two words are related exactly when their given action agrees on every state; this relation is therefore constructed from the source action rather than declared independently.

The public conclusion records equivalence and compatibility with multiplication on both sides. The effective carrier is the canonical quotient by the kernel of the action representation, and its action is induced by the canonical injective kernel lift, which proves faithfulness.

References

• Truth anchor: D5/S3/ConceptDynamics/Control/EffectiveProtocolActionMonoid.effective_protocol_action_monoid