Validate supplied inverse equations without computing the native candidate

[kim-em]

Summary

Adds a checked supplied-inverse equation API for #10378 and the replay interface requested by #10358.

• Packing.Inverse.Equation.readMemo? binds the literal operand, output, selected-root domain, query slice and observed signs without calculating inverseCandidate, gcd or extended gcd.
• Equation.eval_inv and denote_inv prove that the supplied output has the inverse value. Equation.atPoint uses the same selected point as the packing, sign and inverse inventories.
• Public conversion projections and Inverse.Data.toEquation let existing stronger native records supply this semantic contract without opening private constructors.
• Retains the existing Packing.Inverse and InverseFact exact-candidate contract. Their runtime route still computes the native candidate; this PR does not replace that route.
• Controls cover monic and nonmonic reducible heads, a genuinely different valid nonmonic output, changed operands and outputs, genuine incorrect inverse equations, genuine zero equations, changed root domains and out-of-range memo positions.

Verification

• Targeted native controls and companion targets passed (1660 and 4938/4939 jobs).
• Full build, admission audit, structural gates and exact final Opus review are recorded in the final verification comment before merging.
• Every new public theorem has an ordinary-kernel axiom guard; no new proof admissions.

This implements the supplied-equation interface and its semantic laws. The recursive accepted-conjunction exporter and the remaining Phase 4 obligations stay open under #10378. It does not close either owner issue.