Left-quotient result review

Run the independent review check from the repository root:

python3 public/research-artifacts/result-review-2026-09-01-batch-15/audit_left_quotient_review.py

The construction side evaluates the quotienting expression as a relation on the Antimirov partial derivatives of the target expression. The oracle side builds epsilon-free Glushkov position automata and searches their synchronized state-pair graph. They share the parser, fixed expression corpus, alphabet, and case ordering; they do not share derivative transitions, automaton states, or the quotient acceptance algorithm.

The audit covers 405 expression pairs and all 31 binary suffixes of length at most four, giving 12,555 membership comparisons. It also checks the unary bounded-unfolding obstruction for every integer k from 0 through 64. The saved certificate reports zero failures and the same semantic transcript hash as both earlier published audits.

The computation corroborates the structural proof; it does not replace the all-expression theorem or formalize the separate constructor-only compiler discipline.