core: strict unitality is pinned only where the two pushout numberings coincide — id;g on a non-monotone left leg is unguarded

[tsondru]

Found at #289 (G2-T3) r4 decision review, 2026-08-22. Not found by reading the tests — found by proposing a wrong change to perform_pushout and discovering the suite could not see it.

The gap

compose_with_quotient (catgraph/src/cospan.rs) passes self.right/self.is_right_id as perform_pushout's left leg, so the left_leg_id fast path is exactly strict left unitality: id ; g returns g's apex numbering verbatim. The general union-find path numbers the apex by left-leg discovery order instead, so it returns g with its apex permuted. The two paths therefore disagree, and only one of them satisfies id ; g = g on the nose.

Nothing in the suite pins that. The two candidate guards both miss it, for different reasons:

• catgraph/tests/property_laws.rs:376 — cospan_left_identity asserts assert_connectivity_eq(&result, &f, ...), i.e. up to connectivity equivalence. Apex renumbering is invisible to it by construction. Same for cospan_right_identity at :383.
• catgraph/tests/pushout_correctness.rs:29 — compose_with_left_identity_preserves_structure does assert strict structure (left_to_middle, right_to_middle, middle), but its fixture is f = cospan(&[0, 1], &[1, 2], &['a', 'b', 'c']). With f.left = [0, 1] the fast path and the union-find path produce identical output, so the assertions cannot separate them. Sound, and narrow in exactly the way its name does not admit.

Measured

Probe fixture — a left leg that is not monotone-injective-from-0:

let f = Cospan::new(vec![1, 0], vec![0, 1], vec!['a', 'b']).unwrap();
let id = Cospan::identity(&f.domain());
let result = id.compose(&f).unwrap();
assert_eq!(result.middle(), f.middle());

tree	result.middle()	probe
68d49d2 (fast path as-is)	['a', 'b']	passes
candidate: left_leg_id arm renumbered to match union-find	['b', 'a']	fails

The candidate change's own cargo test --workspace was green, and its diff touched none of property_laws.rs, pushout_correctness.rs, frobenius_axioms.rs, compact_closed.rs or braiding_core_pins.rs. So a change that silently breaks id ; g = g passes the full gate set today.

The right_leg_id arm is not affected — it returns exactly what the union-find path returns for the same input (derived by hand twice, on both the fast-path and union-find branches). The divergence is one arm only. But the right-hand law is pinned no more strictly than the left one, so it is unguarded for the same reason.

Work

Part of this lands in #289: that PR promotes the probe above to a permanent test, since the r4 work touches perform_pushout directly. The residual for this issue:

1. Mirror it on the right — f ; id asserted strictly with a right leg that is not monotone-injective-from-0. Low risk today (the arms agree) but unpinned for the same reason the left one was.
2. pushout_correctness.rs:29 — either widen the fixture so the assertions can separate the two numberings, or state the narrowness in the docstring. A test named ..._preserves_structure that only ever sees the degenerate case is the tell CLAUDE.md's second vacuity check is looking for.
3. Decide whether the identity laws deserve strict-equality proptest arms. General composition is defined only up to isomorphism, so assert_connectivity_eq is the right comparison there — but identity composition is the one case where strict equality is a legitimate law, and asserting it up-to-iso throws away the property that actually distinguishes a correct implementation.

Falsify: with the widened fixtures in place, renumbering the left_leg_id arm to representative = (0..R).map(Right) → union-find order must redden them; record the measured apex before and after.

Severity

Important, not minor. Most sound-but-narrow rows in this sweep are theoretical — this one is measured to have let a real regression through a full green suite and a /code-review high pass. Group: G2 (core), after #289.

[tsondru]

Folded into #392 (coverage backlog, 2026-09-01 triage: test-only row, prod diff 0 expected). Reopen if a production defect surfaces here.

[tsondru]

Discharged by PR #410 (squash ef99d94, G18-T1): catgraph/tests/canonical.rs::strict_unitality_over_the_cospan_corpus and strict_unitality_on_every_braiding_of_at_most_four_wires pin strict left/right unitality on Cospan<char> under derived PartialEq; the perform_pushout fast-path mutant reddens 21 of 118 corpus checks.