This is the transcript of a Fable latent space search grounded with my SMT theory for combinatorial species. I don't want to give your project any "slop", but if any of these solvers are of interest I would be happy to properly implement them with tests.
All checks pass — benchmarks/winding_smt.py is in the refreshed zip. Here's what the two experiments established.
How the solver compares on winding numbers: strong on both directions, with one lesson that matters more than the timings. On the Zₖ clock discretization (odd k, so wrapped differences are unambiguous), z3 proved the per-plaquette bound |w| ≤ 1 as UNSAT in 18 ms, proved the topology theorem — total vortex charge on a torus is zero — as UNSAT in 19 ms, constructed a vortex/antivortex pair at prescribed plaquettes in 28 ms, and built a charge-1 vortex on an open grid (where the boundary carries the charge) in 16 ms. Existence and impossibility both land in milliseconds.
But the road there is the real finding. My first encoding created fresh wrapped-difference variables per plaquette, and the L=3 torus UNSAT timed out at 15 seconds — the solver had to rediscover, edge by edge, that shared differences cancel. Encoding each edge's difference once, reused with opposite signs by its two adjacent plaquettes, makes the telescoping identity Σwₚ = 0 syntactic, and the same proof collapses to 19 ms of pure propagation. The moral, which generalizes well beyond this toy: the solver doesn't find topology; the encoding carries it. Discrete topological invariants are exact-sequence facts, and if the variable-sharing structure mirrors the boundary operator, impossibility proofs are free; if it doesn't, they're exponential. That's also the honest framing for any OpenWave use: SMT is credible for certified discrete initial conditions and impossibility checks on small lattices (e.g., "no configuration with this charge profile exists under these boundary conditions"), not as a competitor to their PDE solvers.
Does the cycle-index machinery help? Yes, and quantifiably, in both of its roles. As a counter: Burnside over C₄ × Z₅ (plaquette rotations × global phase, order 20) says the 100 raw w=+1 plaquette states fall into exactly 5 orbits, verified against direct orbit partitioning — a 20× compression, meaning the group acts freely on this stratum (every vortex state has trivial stabilizer, itself a small structural fact the count reveals). As a solver accelerant: fixing the global phase cut the allSAT enumeration from 100 models in 98 ms to 20 models in 24 ms — a reduction of exactly ×5, predicted by Burnside before the solver ran and confirmed by it after. That's the useful division of labor in miniature: the cycle-index machinery predicts the size of the symmetry-reduced space, the symmetry-breaking constraints realize the reduction, and agreement between the two is a correctness check on both.
For OpenWave specifically, the composite picture from this plus last turn: the deliverable-grade contributions are the layout certificate (8× SoA miss advantage on their voxel records), Pólya orbit-reduction for their parameter sweeps, and now this pattern — boundary-respecting SMT encodings for certified defect initial conditions, with Burnside-predicted symmetry breaking when enumerating configuration families. The species theory proper stays home, as before; the machinery around it travels well.
This is the transcript of a Fable latent space search grounded with my SMT theory for combinatorial species. I don't want to give your project any "slop", but if any of these solvers are of interest I would be happy to properly implement them with tests.
All checks pass — benchmarks/winding_smt.py is in the refreshed zip. Here's what the two experiments established.
How the solver compares on winding numbers: strong on both directions, with one lesson that matters more than the timings. On the Zₖ clock discretization (odd k, so wrapped differences are unambiguous), z3 proved the per-plaquette bound |w| ≤ 1 as UNSAT in 18 ms, proved the topology theorem — total vortex charge on a torus is zero — as UNSAT in 19 ms, constructed a vortex/antivortex pair at prescribed plaquettes in 28 ms, and built a charge-1 vortex on an open grid (where the boundary carries the charge) in 16 ms. Existence and impossibility both land in milliseconds.
But the road there is the real finding. My first encoding created fresh wrapped-difference variables per plaquette, and the L=3 torus UNSAT timed out at 15 seconds — the solver had to rediscover, edge by edge, that shared differences cancel. Encoding each edge's difference once, reused with opposite signs by its two adjacent plaquettes, makes the telescoping identity Σwₚ = 0 syntactic, and the same proof collapses to 19 ms of pure propagation. The moral, which generalizes well beyond this toy: the solver doesn't find topology; the encoding carries it. Discrete topological invariants are exact-sequence facts, and if the variable-sharing structure mirrors the boundary operator, impossibility proofs are free; if it doesn't, they're exponential. That's also the honest framing for any OpenWave use: SMT is credible for certified discrete initial conditions and impossibility checks on small lattices (e.g., "no configuration with this charge profile exists under these boundary conditions"), not as a competitor to their PDE solvers.
Does the cycle-index machinery help? Yes, and quantifiably, in both of its roles. As a counter: Burnside over C₄ × Z₅ (plaquette rotations × global phase, order 20) says the 100 raw w=+1 plaquette states fall into exactly 5 orbits, verified against direct orbit partitioning — a 20× compression, meaning the group acts freely on this stratum (every vortex state has trivial stabilizer, itself a small structural fact the count reveals). As a solver accelerant: fixing the global phase cut the allSAT enumeration from 100 models in 98 ms to 20 models in 24 ms — a reduction of exactly ×5, predicted by Burnside before the solver ran and confirmed by it after. That's the useful division of labor in miniature: the cycle-index machinery predicts the size of the symmetry-reduced space, the symmetry-breaking constraints realize the reduction, and agreement between the two is a correctness check on both.
For OpenWave specifically, the composite picture from this plus last turn: the deliverable-grade contributions are the layout certificate (8× SoA miss advantage on their voxel records), Pólya orbit-reduction for their parameter sweeps, and now this pattern — boundary-respecting SMT encodings for certified defect initial conditions, with Burnside-predicted symmetry breaking when enumerating configuration families. The species theory proper stays home, as before; the machinery around it travels well.