[SamuelSchlesinger]

Vertex triples in the Exact Triangle hashing and witness modules were bare Fin n × Fin n × Fin n tuples, read as weightSum … t.1 t.2.1 t.2.2. This PR replaces them with a Triangle n record (fields a b c, deriving DecidableEq and Fintype). That is item 2 of #4823.

Before migrating, I checked whether the counting proofs stay clean with the record, as #4823 asked. They do:

• Triangle.equivProd relates the record to the product.
• Triangle.card : Fintype.card (Triangle n) = n ^ 3 and Triangle.sum_eq (a sum over triangles is an iterated sum over the three parts) replace the repeated Fintype.card_prod/Fintype.sum_prod_type steps in sum_falsePositiveCount_le and falsePositiveCount_add_zeroCount_eq_sum_coeff.
• The test decides still evaluate through the derived instance.

IsSearchAnswer, runScans, card_falsePositive_primes_le and card_le_falsePositiveCount_of_distinct_scans also take or return Triangle n now, so search results and counts use the same type. Only the type of the triple changes; the counted values, step bounds and word layouts are unchanged. The WordRAM readbacks use countZeroMod/falsePositiveCount as opaque numbers and build unchanged. scanOf and signedBitInstances now bind their tuple components by name. Projection chains in these modules go from 15 to 0 (Hashing 10, Lopsided 3, Witnesses 2); the baseline is left to the pruning PR.

There are no compatibility aliases. One test proof changes: simp no longer finds emptiness for Fin 0 triangles on its own, so the zeroCount example at Fin 0 is now decide.

This PR is infrastructure and readability work, not new mathematics. Part of #4823.

Validation:

• lake build --wfail --iofail on the 3 changed modules, all 167 downstream library modules (10 leaves) and the 34 affected tests.
• lake lint on the 3 modules, lake exe lint-style, mk_all --check, check_hygiene --check-simp, both ratchets, check_changed_files --source-only, the manual checker and check_docs --config-only.
• parallel_defs --theorems --no-build-check: no duplicates among the 14 examined (built modules only).
• merge-tree is clean against main and the open PRs that touch these files.

Manuals: Operator's Manual, no edit; the Exact Triangle chapter doesn't name these declarations. Agent Operator's Manual, no edit; no workflow change.

AI disclosure: written by the Jetski worker clients (session 2a1d23e9). Agent review isn't human review.

[SamuelSchlesinger]

Agent review (Jetski alg-layering session b0e92563-9d10-45d2-b8f8-98b2e8157147), head bf501f1: APPROVE.

Reviewed locally before opening, per the CI-throughput rule. I reviewed ec52e7d, then the bf501f1 delta: the baseline edit is reverted, and the Fin 0 zeroCount example is now decide.

• API. Triangle n lives in Hashing, the lowest module that counts triples. Defs/Weights are imported by ThreeSum and all of WordRAM ET, so putting it there would widen their interface. Triangle.card and Triangle.sum_eq replace the Fintype.card_prod×2 and Fintype.sum_prod_type×2 steps in sum_falsePositiveCount_le and falsePositiveCount_add_zeroCount_eq_sum_coeff, so neither proof needs casts or nested sum_congr. HasZeroTriangle stays as the ∃ a b c problem statement, and zeroCount_pos_iff is the bridge.
• Callers. IsSearchAnswer and runScans now use the same type as the counts, which shortens recovery_eq_none_iff's some t case. No product-triple vertex triples remain in ExactTriangle; the other Fin n × Fin n × Fin n uses are DepthFive circuit variables. WordRAM RecordProduct/Detection's simpa only [scanOf, …] still goes through the destructuring let. Counted values, step bounds and word layouts are unchanged. No manual, docs or results file names these declarations, and there's no clash with an existing Triangle.
• Chains. Hashing 10→0, Lopsided 3→0, Witnesses 2→0. The baseline is left to the lower-only pruning PR, so this PR doesn't edit projection_chains_baseline.json (chore(scripts): cap the chain ratchet at the merge-base count so decreases need no baseline edit #5102).
• Manuals. Neither the Operator's Manual nor the Agent Operator's Manual needs an edit. The Exact Triangle chapter doesn't name these declarations, and no workflow changes.
• Optional, not requested: Triangle.sum_eq could get a more descriptive name, e.g. sum_univ_eq.

This is agent review, not human approval.