Add the third opinion: an independent model, exhaustive, on 33.7M inputs

[gHashTag]

#2199 shipped exhaustive cross-target checking and printed a limitation on every run: it compared C against Rust only, so a fault shared by both backends — a spec bug, or shared front-end lowering — was invisible. "The backends agree" and "the backends both match the specification" are different claims, and the first is easy to mistake for the second.

This closes that gap.

tools/ternary_model.py is an independent transcription of the primitives, read from specs/ternary/ternary_ripple_adder.t27 and re-expressed in Python. It was not derived from the generated C or Rust — had it been, it would agree by construction and prove nothing.

Transcribed faithfully, including the parts that look wrong: pack2 does not mask its arguments to two bits, so a value above 3 spills into the neighbouring trit lane. A model that "fixed" that would report a divergence which is really the model disagreeing with the specification it exists to encode.

Result — three-way agreement, exhaustive:

primitive	inputs	result
full_adder(u8,u8,u8)	16,777,216	model == C == Rust
maj3(u8,u8,u8)	16,777,216	model == C == Rust
tmul(u8,u8)	65,536	model == C == Rust
pack2(u8,u8)	65,536	model == C == Rust
negate(u8)	256	model == C == Rust

33.7 million inputs, three independent implementations, ~8 seconds total.

Two negative controls, because the model arm needed its own. Perturbing C proves the C/Rust comparison has resolution; it says nothing about whether a model disagreeing with both backends would be noticed — which is the entire reason the model exists. So there are now two:

one-input perturbation of C     changes the digest   91a68892 -> b7b51485
one-input perturbation of MODEL is visible          91a68892 -> cea51633, backends 91a68892

A measurement that changed the approach. Pure Python over full_adder's 16.7M inputs did not finish in 600 s — it calls dot27 nine times per input, 27 lanes each, about 4 billion operations. Memoising dot27 (a pure function, so semantics are untouched) takes it to under a second. Measured rather than guessed: 179k calls/s uncached, 2.2M/s cached.

Anything added to TARGETS without a model entry is still checked two-way and labelled [2-way: no model entry], so the weaker case cannot pass itself off as the stronger one.

Refs #2198