Release preparation for v4.0.0

[fariedabuzaid]

Release preparation for v4.0.0. The theme is that queries stop being
strings and structures start declaring their own vocabulary — and that the
package stops pretending some of its structures are more "built in" than
others.

The two proposals, checked first

The precompiled .autstr artifacts are gone. Load vs build from scratch was
0.017s/0.049s (Büchi ℕ), 0.023s/0.252s (Büchi ℤ), 0.022s/0.458s (MSO0), and the
built presentations are equivalent to the loaded ones relation by relation
with identical state counts. They bought 0.03–0.44s while being a second source
of truth that could silently drift.

The "arithmetic interface" was already gone — deleted a release earlier by
the symbolic rewrite. What looked like a live second interface was the README's
quick start, which still imported VariableETerm and had been broken code ever
since. The 85 lines that remained were the symbolic interface applied to ℤ.

Asking why it existed at all found the real asymmetry: nine structures
declared a default_signature; the three in buildin could not, because they
were plain functions returning a bare presentation with nowhere to hang one. So
the signature moved onto the presentations and the module became redundant.

autstr.buildin is dissolved

Every structure the library ships is built in, so the name carved nothing:

was	now
buildin.presentations	autstr.arithmetic (Büchi ℕ/ℤ) + autstr.powerset (MSO0)
buildin.tree_presentations	autstr.tree_arithmetic
buildin.automata	autstr.utils.automata_tools (which already imported one from it)

All three presentations gained a codec, each verified against the automata
rather than assumed: ℕ is LSB-first binary (checked against A(x,y,z)), and
MSO0 is a bitmask in canonical form — the universe rejects trailing zeros, so
{0} is 1 and ∅ is the empty word (checked against Subset over all subsets
of {0,1,2}). MSO0 thereby gains an interface it never had: union, intersection
and difference as +, *, -, with solutions returned as Python sets.

Three latent bugs, all found by writing examples

None of these had a failing test; each was exposed by a notebook cell.

1. Enumeration was broken for every interpreted structure of dimension > 1,
   including the shipped Ordinal(2). iterate_language built each tape by
   string-concatenating letters, which holds only while a letter is one
   character; over a product alphabet a letter is a tuple, and str() flattened
   ('0','1') into text no codec could read. Membership worked throughout,
   which is why it went unseen.
2. Such a presentation could not be reloaded after serialization. JSON has
   no tuples, so the alphabet came back as a set of lists (unhashable) and the
   padding symbol as a list.
3. The v2 back-compat loader lost its only test when the artifacts went
   away: test_the_legacy_flat_payload_still_loads was left building a
   presentation and querying it, touching no legacy payload at all. It now
   constructs a v2 payload by hand.

Plus a groups.ipynb cell labelled "has an element of order 4" that asked for
order 2 — Z/2 alone satisfied it.

Serialization for the tree engine

The expensive constructions are the tree ones, so this was on the wrong side of
the line. A tree automaton's compiled form is a sorted table of child pairs with
one diagram root each, and STORE.export/import_nodes are generic over roots,
so the diagram half needed no new code. The collapsible Reach presentation is
22709 bytes, reloads in 0.01s against 0.5s to rebuild, and the reloaded relation
is still reflexive, contains E, and is transitive.

Notebooks and documentation

Six notebooks, not five. infinite_structures is new — the integer grid, the
regular tree, Turing configuration graphs, and level 2 collapsible pushdown
graphs, where the contrast is the point: both present computation as a graph and
both have a decidable first-order theory, but reachability is halting for one
and a relation of the other. composition gained interpretations, built around
the construction of ℤ from ℕ as a 2-dimensional quotient interpretation, with
the codec as the step that makes it legible.

The changelog moved to CHANGELOG.md (and a docs page), leaving the README with
what only it can say. References went the other way: four in the README, the
full annotated bibliography in the docs, cited at the point of use — which
exposed that the overview had no section on any v4 material. It now has two.

Checks

• 855 passed, 5 skipped.
• Docs build clean under -W --keep-going, every notebook executed, all
  cross-references resolving.
• The history animation is regenerated through this release.

Every bibliography entry carries a DOI, checked against the publisher or the
journal rather than supplied from memory. One annotation was wrong and is
fixed: a publisher's abstract page claims rank-width is not defined in Oum &
Seymour 2006, which would have made it the wrong citation for RankWidthClass
— Oum's own survey settles it ("Rank-width was introduced by Oum and Seymour
[71]", where [71] is that paper). Kartzow's issue was also off, 9(1:12) rather
than 9(1).

Generated with Claude Code