A normal circuit with a reducible term: non-left-linearity in convergent gate elimination

R_B terminates: the single-integer weight W (the constant 0 weighted 3, every other symbol 1) strictly decreases on each of the 16 rules and hence at every rewrite step at every position; consequently WellFounded and no infinite reduction sequence

R_B is confluent and has unique normal forms, via the bottom-up smart-constructor normalizer nf: nf t is irreducible, one step never changes nf, and t reaches nf t – so neither the Critical Pair Lemma nor Newman's lemma is used

Every rule of R_B is a Boolean identity, so rewriting preserves the function computed; and a closed term normalizes to 1 or!1 exactly matching its truth value – the source's 'rewriting a circuit with bits substituted just evaluates it'

Controls on the rule set: 0 ->!1 strictly increases the plain symbol count; the weight with w(0) = 2 ties on that rule while w(0) = 3 decreases; R_B extended with commutativity of AND is not terminating (x / y is not even accessible) although W cannot see it; and nf does not collapse every term

An explicit legal input to Algorithm 2 of arXiv:2602.17942v1 – four inputs, all read, four binary gates against the bound 3(n-1) = 9, n = 4 > 3 – that is S'-normal (checked at all ten nodes against all sixteen rules) while its unfolded term (((!x1 /!x1) / x2) / x3) / x4 is R_B-reducible. Every input variable carries exactly ONE hyperedge; the duplication is two distinct free NOT gates. A second, smaller variant duplicates an input hyperedge instead

ERRATUM. On that circuit the line-8 Assert of Algorithm 2 of arXiv:2602.17942v1 – 'h has inputs (!)xₚ, (!)x_q for p, q in V and p!= q', justified in the source by 'the assertion holds because Cᵢ is in normal form' – fails: the unique topologically minimal costly gate (first in EVERY topological order, since every other costly gate has it below) reads two distinct nodes both representing!x₁, so any p, q witnessing the assertion's shape satisfy p = q, and the algorithm as printed has no next move

The repair, machine-checked: one pass of hash-consing (merge edges with equal label and equal already-merged arguments) restores the g / g redex at the blocked gate, leaves the unfolded term and the binary-gate count unchanged, and removes one free negation edge. The witness does collapse in the source's own sense – an explicit non-injective root-preserving hypergraph morphism is exhibited – so it is S-abnormal and S'-normal, which locates the defect exactly at the omission of collapse

Controls for the term-graph half: a LEFT-LINEAR rule does lift on the same shape (two distinct edges both labelled by the constant 1 feeding one AND is NOT S'-normal, because 1 / g -> g does not repeat a variable); a four-input circuit on which the line-8 assertion holds (p = 1, q = 2); and the two negative controls refuting both 'S'-normal implies R_B-normal' and 'the correspondence always fails'

CC_D(XOR₂) = 3: an explicit three-gate DeMorgan circuit computes XOR₂, and NO circuit with two or fewer binary gates computes XOR₂ or its negation – by complete enumeration of all 18,628 well-formed circuits on two inputs with at most two gates, with the COMPLETENESS of the enumeration proved in Lean (memₑnumLe2), so this is a lower bound and not a search report

Controls for the enumeration: it has exactly 18,628 members and does contain circuits computing AND₂ with one gate (so the exhaustive negative is not vacuous); three gates are NOT impossible, refuting any strengthening of the lower bound to size <= 3

The bound 3(n-1) is attained: an explicit DeMorgan circuit family for XORₙ built from XOR(u,v) = (u / v) /!(u / v), with exactly 3(n-1) binary gates and well-formedness proved for EVERY n, and its functional correctness checked exhaustively for n = 1..6