Function norm_add_node

crates/kernel/src/level.rs:341–343

Insert `(idx, k)` into the var list at `path`, taking the max of offsets when `idx` is already present. Mirrors Lean4Lean's `NormLevel.addNode v k path'` (`refs/lean4lean/Lean4Lean/Level.lean:92`); `k` must be the current succ-accumulator from `normalize_aux`. An earlier port of this function dropped `k` and always inserted `(idx, 0)`, which silently mis-normalized `Succ^n(imax(u, Param v))` shap

(s: &mut NormLevel, idx: u64, k: u64, path: &[u64])

      Err(pos) => self.var.insert(pos, VarNode { idx, offset: k }),
    }
  }
}

/// Canonical form: a map from imax-paths (sorted param indices representing
/// the conditioning chain) to nodes tracking constant offsets and variable
/// contributions.