A fine scan settles it in favour of 40:
stride 40 +0.454
stride 39 +0.266
stride 41 +0.215
stride 38 +0.214
The peak is sharp and isolated, nearly twice its immediate neighbours, and
the multiples confirm it: 80 scores +0.376, 120 +0.394, 160 +0.340, while the
multiples of 12 (24, 48, 96, 144) all sit at 0.21 to 0.24.
So the record is 40 bytes and the 0x7f/0x47f markers at 12-byte spacing are a
nested structure inside those records, not the record boundary. Their spacing
is irregular -- 12, 24 and larger -- which is what one would expect of a field
present in some records and absent in others.
The previous commit's "they disagree" framing was itself wrong in one
respect: the marker spacing never claimed to be the record size. Read as a
claim about markers inside records rather than about the record itself, the
two measurements were never in conflict, and I had set up a false dichotomy
between them.