Tentai Show: one mirror map is the whole puzzle, and every deduction happens twice or not at all

Tentai Show (Spiral Galaxies) in the browser with four rule sets
inside. Divide the grid into regions, one per dot, so that every region
contains its dot, is connected, and maps onto itself under a 180° turn
about that dot. Dots sit on cell centres, edge midpoints, or lattice
points. Puzzle #33 in the solver series.

Demo: https://sen.ltd/portfolio/tentai-show/
Repo: https://github.com/sen-ltd/tentai-show

I picked this one because the whole puzzle folds into a single map. The rules
say three things — contains its dot, connected, 180°-symmetric — and once you
start implementing, two and a half of those turn out to be sentences about one
one-line function.

Doubled coordinates and the three kinds of dot

A dot can sit on a cell centre, an edge midpoint, or a lattice point. That
looks like a case analysis until you double the coordinates. Put the centre of
cell (r, c) at (2r+1, 2c+1); a dot position (cy, cx) with integers in
[1, 2n−1] is a cell centre when both are odd, an edge when exactly one is
even, a lattice point when both are even. And the mirror of cell k through dot
g is:

export function mirrorOf(k: number, g: Galaxy, n: number): number {
  const r = g.cy - rowOf(k, n) - 1;
  const c = g.cx - colOf(k, n) - 1;
  return r >= 0 && r < n && c >= 0 && c < n ? r * n + c : -1;
}

2·cy − (2r+1) is odd whatever the parity of cy, so the mirror of a cell is
always exactly one cell, for every kind of dot. The case analysis only ever
resurfaces when enumerating the 1, 2 or 4 cells a dot physically touches.

The four-rule ladder

The solver prunes a candidate array cand[g][k] — "galaxy g can still own
cell k".

level	rule
mirror	a cell and its twin stand or fall together — in both directions: a dead twin kills the cell, and a pinned cell pins its twin
reach	a region is connected and contains its dot, so g dies wherever a cell cannot walk home to the dot through surviving candidates
bridge	a cell pinned to g must stay connected to its dot; a cell on the only remaining corridor is taken
probe	assume one pairing, run the rules below to a fixpoint, drop the pairing if that alone is a contradiction

The pair theorem — every deduction happens twice

One invariant falls out of the construction: each galaxy's candidate set
stays 180°-symmetric about its dot through the entire ladder.

Each rule commutes with the rotation. The mirror closure is symmetric by
definition. The reach BFS walks a symmetric set from symmetric sources (the
cells the dot touches), so the reached set is symmetric. If a corridor cell
forced by bridge is an articulation point, so is its twin. A probe
contradiction replays verbatim on the mirrored side. So prune a candidate on
one side of a dot and the twin falls in the same round. Deductions happen
twice or not at all.

This is measurable: 3 sizes × 300 boards × 4 levels = 3,600 fixpoints,
zero asymmetric candidate sets.

A corollary comes free. A galaxy whose dot sits on an edge or corner covers an
even number of cells; a centre dot covers an odd number. That parity rule
looks worth implementing — and it can never fire. Under the symmetric
closure, undecided cells arrive in twins, and a twin contributes zero or two
cells: every parity the rule could check is already correct. A rule that
cannot fire is a theorem of the rules below it.

The trap I stepped in — writing half of the mirror rule

My first mirror said: "if g is dead at the twin, kill it here". That
transfers candidate death. But the definition of symmetry is stronger — if
a cell is in g's region, so is its twin. The information "this cell's
candidates collapsed to g" never reaches the twin through death-transfer
alone.

// Ownership transfers too: a cell pinned to g pins its twin through g.
for (let k = 0; k < nc; k++) {
  const g = assignedAt(model, cand, k);
  if (g === -1) continue;
  const m = model.mirror[g * nc + k];
  for (let h = 0; h < model.galaxies.length; h++) {
    if (h !== g && cand[h * nc + m]) cand[h * nc + m] = 0;
  }
}

With that half missing, grading boards by the weakest level that finishes them
collapsed to {mirror, probe}: all sixteen 7×7 bank boards graded probe.
Pinned cells never propagated, so every deduction the middle rules should have
made was swallowed by probe. With both directions in, the same generator and
seeds spread the 7×7 bank to mirror 9 / reach 6 / bridge 1. Before measuring
how strong your rule sets are, check that each rule uses all of its own
definition.

The connectivity cliff

300 raw boards per size, unfiltered — filtering the population by the
property you measure makes the column meaningless. Fraction finished by the
fixpoint alone:

board	mirror	+reach	+bridge	+probe	unique answers in the raw stream
5×5	94.3%	97.7%	98.0%	98.0%	98.0%
7×7	63.3%	93.3%	95.3%	95.3%	95.3%
10×10	2.7%	87.3%	92.3%	93.0%	93.0%

mirror falls off a cliff, from 94.3% on 5×5 to 2.7% on 10×10. Mirrors
preserve distance, so "the twin is off the board" prunes less and less as
boards grow — and mirror never once asks whether a cell can still walk
home. reach asks exactly that and lifts 10×10 back to 87.3%. Connectivity
is the rule that pays.

Ablation measured "value relative to the bench", again

Same boards, all four rules minus one:

board	full	−mirror	−reach	−bridge	−probe
5×5	98.0%	5.3%	95.0%	98.0%	98.0%
7×7	95.3%	0.0%	74.0%	95.3%	95.3%
10×10	93.0%	0.0%	31.0%	92.7%	92.3%

Incrementally (the +bridge column of the ladder), bridge looks like
+5.0 points on 10×10. In the ablation it is worth −0.3 points — take
it out and probe picks up nearly every ball it drops. This is the same lesson
the previous puzzle in this series taught: a propagator has no intrinsic
contribution, only a contribution relative to a particular bench. Publish the
incremental ladder and the ablation, because either one alone will lie.

The solve rate is capped by uniqueness — and the ladder hits the cap

Look at the table again: the solve rate at probe equals the unique-answer
rate of the raw stream, to the decimal, at all three sizes (98.0 / 95.3 /
93.0%). Not a coincidence. Sound propagation can never kill a true solution,
so a fixpoint can never finish a board that has two answers. "Solved by
rules" is bounded above by "unique", and this ladder reaches the bound
exactly. Every unsolved board in those columns is a multi-solution board,
where no sound rule could ever help.

That 93–98% of the raw stream is unique at all is this puzzle's own
personality: the mirror constraint is brutal on its own. Even a brute force
with no candidate arrays — walk cells row-major, assign twin pairs in one
stroke, never look at connectivity until a leaf hands the finished division to
an independent flood-fill validator — enumerates all solutions of a 5×5 in a
median of 5 nodes. The uniqueness check on a 10×10 needs a median of 142.5
guesses at mirror, and 0 once reach is in.

Verification

• Count agreement: the propagating search at all four levels and the brute force above count the same number of solutions on random small boards. A sound rule set cannot change the count, so one level disagreeing would convict that rule.
• Independent validator: shares no code with the model or the rules; flood-fills every region at every leaf and every solver exit.
• Soundness: the generator's own division survives the probe-level fixpoint with zero candidates lost, on random boards.
• The pair theorem: symmetry of every candidate set audited after every fixpoint (the 3,600-run version of the same check).

27 tests.

Takeaways

• Doubled coordinates collapse three kinds of dot into one one-line mirror map
• Candidate sets stay 180°-symmetric through the whole ladder (3,600 fixpoints, zero violations): deductions happen twice or not at all
• The parity rule cannot fire — it is a theorem of the mirror closure. Knowing which rules you don't have to write is also a payoff
• The mirror rule has two directions, death and ownership; write half of it and your difficulty grades quietly collapse
• mirror drops to 2.7% on 10×10; connectivity brings back 87.3%
• bridge: +5.0pt incremental, −0.3pt in ablation — publish both numbers
• A sound fixpoint's solve rate is capped by the uniqueness rate, and this ladder hits the cap at every size

---

SEN LLC builds small, well-measured software and writes up what it learns.
More at sen.ltd/portfolio.