Function reconcile_block_params 

pub fn reconcile_block_params(block: &[MutualInductive]) -> KernelResult<usize>

The ONE parameter-count rule for a MUTUAL block, stated where registration can enforce it.

A mutual block shares a single uniform parameter telescope: Tree A/Forest A are one declaration over one A. Two things are refused, and the second used to be laundered rather than diagnosed:

• a member whose recorded num_params EXCEEDS its own arity — nonsense that derive_mutual_recursor’s .min(arity) silently clamped, so two members could agree on a number while disagreeing about what their parameters mean; and
• members that disagree on the count.

Returns the block’s shared parameter count. An EMPTY block has none and is vacuously fine.

Better than Lean’s diagnostic in one respect: the message lists every member and its own count, so the odd one out is visible without re-reading the declaration.