Names and columns: the Leibniz congruence of a diagonal name-algebra

A name-algebra in the sense of the Coordinatal Gödel locale is a set of names generated from a base by unary operations, each name reading a column of a fixed coordinate system. Designating the names that represent the diagonal turns it into a logical matrix. We study the Leibniz congruence of that matrix (the diagonal name-algebra, for short) inside the locale, with every definition and every numbered theorem checked in Isabelle/HOL (no axioms, no sorry). Three things are shown. (i) The relation of indiscernibility under term functions is defined for an arbitrary generated-path structure and proved to be the largest congruence compatible with the designated set, i.e. the Leibniz congruence. (ii) If the designated set is a single name that is the value of a constant term function, then every filter of the resulting logic is the Leibniz class of that name in its own Leibniz congruence; the single equation x ≈ p(x) defines truth in every filter. The logic is assertional in Raftery's sense (its designated name is the value of a term constant on the algebra), hence truth-equational; the theorem is the single-algebra instance of that fact, now machine-checked. (iii) The column map, which sends a name to the column it reads, has a kernel ≈, the extensional kernel. We call a congruence of the name-algebra column-level if it is the pull-back of its push-forward along the column map; equivalently, if it contains ≈. When the operations are extensional, the column map is a surjective homomorphism and the textbook lemma puts ≈ below the Leibniz congruence. When an operation is not extensional, the quotient by ≈ is not an algebra; the lemma still applies to every congruence below ≈ and puts it below the Leibniz congruence, but it says nothing about the rest of ≈, and the two relations can become incomparable. Two five-element name-algebras witness this: in one the two relations are incomparable, in the other the Leibniz congruence is the identity and lies strictly below ≈; in both the only congruence below ≈ is the identity. The exact minima are settled: with a single designated name a strict position needs three names and incomparability four, and both bounds are attained. The diagonal name-logics of all six examples are assertional, hence truth-equational, and none is protoalgebraic (an artefact of the unary signature). Four of them are not selfextensional (two formulas that say the same thing stop saying the same thing after one operation); the two three-element witnesses are selfextensional, one of them without being extensional, so the designation side and the column side are independent in both directions. None of this is general: when the diagonal is not marked on the path the designated set is empty and the logic is protoalgebraic and selfextensional.