IxVM: handle wrapped recursor telescopes and theorem-headed iota majors

[arthurpaulino]

Summary

Fix two WHNF gaps that caused IxVM to reject valid Lean constants involving recursors:

• Whnf index telescopes while reconstructing canonical recursors, so index binders hidden behind definitional wrappers are discovered.
• Unfold theorem-headed recursor majors at the iota site, while keeping theorem bodies stuck in general WHNF.
• Run K-recursor synthesis on the raw major before major WHNF, matching the reference kernel and avoiding expensive evaluation of proof-producing decision procedures.
• Guard the hoisted K path against partially applied recursors before reading the major from the spine.

Together these changes fix all 34 previously reported mathlib failures, including Rat.instEncodable and the family of failures involving wrapped inductive types.

Details

Canonical recursor reconstruction previously peeled an inductive's declared type structurally. For declarations whose index telescope is hidden behind an abbrev, this encountered an application instead of a Forall and aborted. collect_index_doms now preserves the cheap structural fast path, falls back to WHNF when necessary, and stops tolerantly in the same way as the reference implementation. The earlier validation of the complete parameter and index telescope remains strict, so this does not weaken the kernel check.

Separately, a recursor major may legitimately be headed by an auto-generated theorem after Lean's abstractNestedProofs pass. General IxVM WHNF intentionally leaves theorem heads stuck, preventing iota reduction in this case. The new whnf_iota_major unfolds theorem heads only while reducing an iota major. This gives the required reduction without globally expanding every proof term.

For K-like recursors, synthesis now runs against the raw major before attempting major WHNF, as in the reference kernel. This avoids evaluating potentially large decision procedures merely to reduce proof-valued majors. Because this moves the K gate ahead of try_iota, it now checks that the spine actually contains the major before calling list_lookup; partially applied recursors simply decline the iota step.

Tests and cost

• Added HiddenIdx/PredOver coverage for index binders hidden by a definitional wrapper.
• Added thmMajorUse coverage for theorem-headed iota majors.
• Added partialKRec coverage for partially applied K recursors.
• Both IxVM test suites pass.
• All 34 previously failing mathlib constants pass; Rat.instEncodable completes in 119 seconds.
• Performance guards remain flat: Std.Time...ofDays._proof_1 5.1s, bitblast goCache equality 41s, goCache_Inv_of_Inv 112s, and UInt8.ofBitVec_not 2.3s.
• FFT pins were re-harvested. The index-telescope change moves affected pins by at most 0.0002%; the iota/K change has a largest shift of +0.03%, with some recursor-heavy cases improving by avoiding major WHNF.