| 4767 | // Plan keys (`X.rec`, `all0.rec_N`, …) are shared across every |
| 4768 | // SCC split from one original mutual, and `DashMap::insert` is |
| 4769 | // last-writer-wins. With per-position ownership resolved in |
| 4770 | // aux_gen exactly one block computes each name's plan, so a |
| 4771 | // differing pre-existing entry is a claim collision — fail |
| 4772 | // loudly instead of shipping schedule-dependent rewrites |
| 4773 | // (plans/aux-recursor-alias-collision.md §2.4). |
| 4774 | if plan.head_rewrite.is_none() { |
| 4775 | if let Some(brecon_name) = surgery::rec_name_to_brecon_name(&name) |
| 4776 | && lean_env.get(&brecon_name).is_some() |
| 4777 | { |
| 4778 | let new_plan = surgery::BRecOnCallSitePlan::from_rec_plan(&plan); |
| 4779 | // Type-level brecOn splits into `.go` (the PProd-packed |
| 4780 | // worker) and `.eq` (its unfolding lemma). Lean's |
| 4781 | // auto-generated equation-lemma proofs (`f.eq_def`) reference |
| 4782 | // both DIRECTLY with explicit motive/handler arguments, and |
| 4783 | // their telescopes are identical to `.brecOn`'s (params, |
| 4784 | // motives, indices, major, handlers) — so they need the same |
| 4785 | // call-site permutation. Without these keys, eq_def proofs |
| 4786 | // ship source-order motives against the canonical-order |
| 4787 | // regenerated `.go`/`.eq` (the torchlean |
| 4788 | // `NN.GraphSpec.DAG.*.eq_def` AppTypeMismatch family; fixture |
| 4789 | // `Tests/Ix/Compile/Mutual.lean` `TypeBrecOnEqDef`). |
| 4790 | let mut plan_keys = vec![brecon_name.clone()]; |
| 4791 | for sub in ["go", "eq"] { |
| 4792 | let sub_name = Name::str(brecon_name.clone(), sub.to_string()); |
| 4793 | if lean_env.get(&sub_name).is_some() { |
| 4794 | plan_keys.push(sub_name); |
| 4795 | } |
| 4796 | } |
| 4797 | for key in plan_keys { |
| 4798 | if stt |
| 4799 | .brec_on_call_site_plans |
| 4800 | .get(&key) |
| 4801 | .is_some_and(|existing| *existing != new_plan) |
| 4802 | { |
| 4803 | return Err(CompileError::InvalidMutualBlock { |
| 4804 | reason: format!( |
| 4805 | "conflicting brecOn call-site plans for '{}' — two \ |
| 4806 | blocks claim one source-indexed aux name", |
| 4807 | key.pretty(), |
| 4808 | ), |
| 4809 | }); |
| 4810 | } |
| 4811 | stt.brec_on_call_site_plans.insert(key, new_plan.clone()); |
| 4812 | } |
| 4813 | } |
| 4814 | if let Some(below_name) = surgery::rec_name_to_below_name(&name) |
| 4815 | && let Some(below_ci) = lean_env.get(&below_name) |
| 4816 | { |