We introduce a many-sorted first-order kernel theory TKer whose models are categorylike structures equipped with a distinguished predicate of segments labeled by increments, an odds map on objects, and a multiplier map on increments valued in an abelian group. A transfer axiom propagates odds along segments. A witness-only scheme P is a set of existential axioms asserting the existence of finite segmentlabeled diagrams. From TKer + P we extract a reduced semantics for multiplier equalities that is guarded by diagram membership: multiplier constraints are asserted only for tuples of increments that occur together as labels in an instance of a witness template. For each template (θ; a¯) ∈ P we construct a presented diagram Mθ, extract from it a subgroup of Z n generated by endpoint-matched segment-walk relations, and define an induced reduced theory diag(P). Assuming TKer + P is satisfiable, we prove the Theorem of m-Completeness for m-Equations: for every diagram-guarded mequation φ, (TKer + P) |=m,P φ ⇐⇒ diag(P) |= φ. We also record that the coarser fragment of universal m-equations guarded only by the predicate Real collapses to the identities of abelian groups (together with m(0) = 1). In this way, existential pattern assumptions are compiled into a complete, explicit equational theory for the guarded fragment, rather than handled only by general-purpose saturation or by equational reasoning that presupposes an equational axiom basis.
William Kofski (Tue,) studied this question.