Compute — projective plane of order 12

Replay:

python3 replay_identities.py
python3 classify_types.py
python3 macneish_pair.py certs/macneish_involution_2mols.json
python3 verify_involution_mols.py --json certs/macneish_involution_2mols.json
python3 verify_involution_mols.py --json certs/t2_squares.json
./drat-trim certs/mate_t2.cnf certs/mate_t2.drat
./drat-trim certs/mate_macneish.cnf certs/mate_macneish.drat

The last two CNFs are regenerated by encode_mate.py from the family JSON; the checked DRAT files match the CNFs written tonight.

artifact	claim
`certs/identities.json`	$v=157$ , pair count, $\lvert\det B\rvert=13\cdot12^{78}$ , Bruck–Ryser silent
`certs/type_classification.json`	remaining Aut-element types after divisibility
`certs/macneish_involution_2mols.json`	explicit involution 2-MOLS (MacNeish product)
`certs/t1_squares.json`, `certs/t2_squares.json`	SAT witnesses for $t=1,2$
`certs/mate_t2.drat`, `certs/mate_macneish.drat`	verified UNSAT: those two 2-families have no third involution-mate
`certs/t3b.cnf` / `certs/t3c.out`	$t=3$ cell-symbol; kissat `UNKNOWN` at 2396s / 45M conflicts
`certs/sd3.cnf` / `certs/sd3.out`	$t=3$ $\sigma,\delta$ ; kissat `UNKNOWN` at 2396s / 21M conflicts

kissat 4.0.4 and drat-trim are local copies. Do not treat a SAT timeout as an exclusion.