fix: make kernel `is_def_eq` caching order-independent (#14806)

This PR fixes a soundness issue in the kernel.

**TL;DR.** The kernel cached successful `is_def_eq` queries in a
union-find structure. Because the implemented `is_def_eq` is sound but
incomplete, and therefore not transitive, the transitive closure
computed by the union-find made a query's result depend on the order of
earlier queries: `is_def_eq(v0, v2)` could return `false` on its own but
`true` after `is_def_eq(v0, v1)` and `is_def_eq(v1, v2)` had succeeded.
A crafted input used this to build a recursor whose type and computation
rule disagreed, and derive `False`. The fix replaces the union-find with
a plain cache keyed on the query pair, so `is_def_eq` is again a
function of its two arguments. **The issue was reported by Daniel Selsam
(OpenAI) using their internal models. An OpenAI agent then produced two
distinct exploits based on it. Both exploits are also caught by nanoda,
and both are caught by the new lean-inductive-models developed by
Joachim Breitner.**

This PR makes the kernel's definitional equality check independent of
the order in which queries are made. The kernel cached successful
`is_def_eq` queries in a union-find structure; because of this, the
result returned by `is_def_eq` could depend on which queries had been
made before. With a carefully constructed input this allowed the kernel
to build a recursor whose type and computation rule were inconsistent,
from which `False` could be derived.

Definitional equality, as specified, is an equivalence relation: it is
reflexive, symmetric, and transitive. That specification is correct. The
kernel's `is_def_eq` is an implementation of this relation, and like any
such implementation it is sound but incomplete: it never reports two
terms as equal unless they really are definitionally equal, but it can
fail to prove a valid equality because it uses a fixed reduction
strategy that may get stuck. As a consequence there exist terms `v0`,
`v1`, `v2` for which `is_def_eq(v0, v1)` and `is_def_eq(v1, v2)` both
succeed while `is_def_eq(v0, v2)`, asked on its own, returns `false`. In
other words, the implemented test is not transitive even though the
relation it approximates is.

To avoid repeated work, the kernel recorded successful queries in a
union-find structure (`equiv_manager`) and consulted it before doing any
real work. Every pair merged into that structure is genuinely
definitionally equal, and since definitional equality is transitive, the
transitive closure the union-find computes contains only true
equalities. The cache is therefore sound in isolation. The problem is
that the implemented `is_def_eq` is incomplete, so exposing this
transitive closure changes its observable result: once `is_def_eq(v0,
v1)` and `is_def_eq(v1, v2)` have been recorded, a later `is_def_eq(v0,
v2)` is answered `true` from the union-find, whereas the same query made
in isolation returns `false`. The value returned by `is_def_eq(v0, v2)`
thus depends on the order of the preceding queries. Any code that
assumes `is_def_eq` is a function of its two arguments can be broken by
this. Recursor construction is one such consumer: it decides which
constructor fields are recursive by calling `is_def_eq` and does so more
than once while building a recursor, and it relies on getting the same
answer each time.

The fix replaces the union-find with a plain cache keyed on the query
pair, matching the `isDefEq` cache used by the elaborator. Kernel
expressions contain no metavariables, so a query's result is a function
of its two arguments; both positive and negative results can be cached
and shared across queries while remaining order-independent. This
restores determinism: `is_def_eq(v0, v2)` now returns the same answer
regardless of history. The elaborator already uses a plain cache with no
union-find, so this does not change which terms elaboration accepts.

The issue was reported by Daniel Selsam (OpenAI) using their internal
models. An OpenAI agent then produced two distinct exploits based on it.
Both exploits are also caught by nanoda, and both are caught by the new
lean-inductive-models developed by Joachim Breitner.

---------

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>